From e95feba878c0ad4ee3f15a07429b901761142f5d Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 09:13:53 -0400 Subject: [PATCH 1/3] Audit #6097's five-call diagonal-pair refutation and extend it to F3 Independent stdlib engine (F_p restatement) and a local SAT encoding agree with #6097 over F2 (zero survivors at lengths <= 5). Over F3 at width two the stdlib engine refutes lengths <= 4 and the local SAT run refutes length five, so the six-call minimum also holds over F3. No new kappa. Co-Authored-By: Claude Opus 5.5 --- .../diagonal-pair-collision-audit/README.md | 146 ++++++++ .../SOURCES.json | 18 + .../diagonal-pair-collision-audit/TASK.json | 57 +++ .../diagonal-pair-collision-audit/VERIFY.json | 19 + .../sat_crosscheck.py | 101 +++++ .../diagonal-pair-collision-audit/verify.py | 347 ++++++++++++++++++ 6 files changed, 688 insertions(+) create mode 100644 research/diagonal-pair-collision-audit/README.md create mode 100644 research/diagonal-pair-collision-audit/SOURCES.json create mode 100644 research/diagonal-pair-collision-audit/TASK.json create mode 100644 research/diagonal-pair-collision-audit/VERIFY.json create mode 100644 research/diagonal-pair-collision-audit/sat_crosscheck.py create mode 100644 research/diagonal-pair-collision-audit/verify.py diff --git a/research/diagonal-pair-collision-audit/README.md b/research/diagonal-pair-collision-audit/README.md new file mode 100644 index 0000000000..7590f2b384 --- /dev/null +++ b/research/diagonal-pair-collision-audit/README.md @@ -0,0 +1,146 @@ +# Audit of #6097's five-call diagonal-pair refutation, and the same floor over F3 + +**Independent audit and a scoped extension. No new κ.** The selected record is +unchanged. + +[#6097](https://github.com/CrocSwap/integer-mult-bounds/pull/6097) (JoyboyBrian, +head `0a24101a977a652a306dd252b009d54840e4fdc9`) proves a computer-assisted +floor in the rank-one-idempotent register model of #4089. Over `F2` at width +two, for every group `G` and label set `L`, no product of at most five calls +`D_N(g) = (I−N) + [g]N` equals `diag([a],[b])`. This needs `a ≠ b` and that +neither is a product of at most two labels. For `diag([xyx],[yxy])` the +direct six-call word shows the bound is exact. + +## Results + +1. **#6097's PROOF.md: no error found.** I checked each step against the model. + This covers the free basis-change normalization, dropping identity-labelled + calls, prefix/suffix cancellation, the forbidden equalities, the parity step, + and the completeness of partner branching. There are three remarks, and none + affects the result. + * PROOF.md says "every common-prefix or common-suffix rule". #6097's + `cancellation_rules` emits only the *maximal* common prefix and suffix of + each pair. The two closures are equal. Say `U = p·r·u` and `V = p·r·v`, where + `p·r` is the maximal prefix. The shorter-prefix law `U ~ V ⇔ r·u ~ r·v` then + follows from the maximal laws `U ~ V ⇔ u ~ v` and `r·u ~ r·v ⇔ u ~ v`. My + engine emits every prefix and suffix length and reaches the same verdicts. + * Its node counts are exactly those of my engine (1,392 at length four and + 10,634 at length five). The codes are different, but both branch on the + first class of a shortest residual equation. So the search order is not an + independent check. The SAT encoding below is a different method. + * The node cap (200,000) is shared by all tuples of one length. It fails + closed, so it cannot produce a false rejection. +2. **An independent stdlib engine agrees** ([verify.py](verify.py)). It was + written before I read #6097's verifier. It restates the relaxation over `F_p` + and imports no repository code. Over `F2` it finds zero survivors at lengths + 0–5 (all 9,331 tuples), and it accepts #6097's controls. Without + cancellation it gives exactly 20 survivors at length four and 938 at length + five. These are the counts of #6048's support-only relaxation. +3. **A local SAT cross-check also agrees** ([sat_crosscheck.py](sat_crosscheck.py), + python-sat 1.9.dev15 / CaDiCaL 1.5.3, Python 3.12.14, macOS arm64). This + method is independent of the branching search. Over `F2` it finds zero + survivors at lengths 1–5. Without cancellation it finds 20 and 938, matching + the stdlib engine. +4. **New: the same six-call floor holds over F3 at width two.** Over `F3` there + are 12 rank-one idempotents (`p(p+1)`). The stdlib engine refutes all tuples + of length 0–4: 22,621 of them, registered. The local SAT run refutes all + 248,832 tuples of length five, in 555 s on 8 cores. The direct six-call word + works over every field. So under #6097's hypotheses the minimum over `F3` is + also **exactly six**. This answers #6097 open question 2 for `F3` at width + two. The length-five row is **local SAT evidence**, not a stdlib replay. + The stdlib search is far too slow there: single tuples starting and ending + with the projectors `[[2,1],[1,2]]` and `[[2,2],[2,2]]` need up to ~1.4·10⁵ + nodes. Without cancellation, both engines find exactly 84 survivors at `F3` + length four. So the F3 refutation does depend on cancellation, as it does + over `F2`. + +## Soundness over F_p + +The argument is #6097's, with parity replaced by class weights mod `p`. Drop +identity-labelled calls. Expand the product as `Σ_U [g_U] P_U`, with +`P_U = Π_i (N_i if i ∈ U else I − N_i)` in chronological order. Subtract +`[a]` in entry 00 and `[b]` in entry 11. Each of the four entry equations is +zero in `F_p[G]`. The elements `[g]` form a basis, so every actual group-value +class has total coefficient 0 mod `p` in every equation. This follows the +known partition argument: + +* **Closure.** Common-prefix and common-suffix cancellation hold in every group. + The forbidden equalities `g_i ≠ e`, `a ≠ b`, and `a, b ∉ {g_U : |U| ≤ 2}` + are the hypotheses. +* **Forcing.** Merges only add the class totals of an equation. Suppose a + current class has a nonzero total. Its final class must then contain another + current class whose total is nonzero. With one such class there is a + contradiction. With exactly two, they must merge, and their totals must sum + to 0. +* **Branching.** Otherwise, take a class with a nonzero total in a shortest + residual equation. Branch over every other class with a nonzero total in that + equation. One branch keeps the actual realization. + +The SAT encoding states the same relaxation directly. It has one variable per +node pair, transitivity clauses, and each cancellation rule as an equivalence. +Forbidden pairs are negative units. For every equation `E` and node `u ∈ E`, a +mod-`p` one-hot counter forces `Σ_{v∈E} w_v [v ~ u] ≡ 0`. A model is exactly +a surviving partition. Free scalar changes of basis reduce to conjugated +projectors over `GL₂(F_p)`, exactly as in #6097. `S D_N(g) S⁻¹ = D_{SNS⁻¹}(g)`, +and the augmentation `F_p[G] → F_p` forces the trailing scalar to be `I`. + +## Reproduce + +```sh +python3 -I -W error -B research/diagonal-pair-collision-audit/verify.py # ~30 s +python3 -I -O -W error -B research/diagonal-pair-collision-audit/verify.py +# local only, needs python-sat: +python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 2 5 +python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 3 5 --jobs 8 # ~10 min +python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 3 4 --no-cancel # 84 +``` + +Expected marker: `PASS_DIAGONAL_PAIR_COLLISION_AUDIT`. The run must also show +zero survivors in every row: `F2` lengths 0–5 and `F3` lengths 0–4. The +controls check several things: + +* both projector inventories, against an independent `u vᵀ` (`v·u = 1`) + enumeration; +* #6097's bit encoding; +* every generated cancellation rule, as a single common-context law; +* the subset expansion, against a free-monoid expansion; +* the exact six-call endpoint over `F2` and `F3`; +* that the solver accepts the six-call word and #6038's four-call `xy/yx` + word; +* that #6097's tuple `(1,5,1,10)` survives without cancellation and dies with + it; +* the short-target reopening of `(E00,E11)`, and the rejection of #6097's + written five-call example; +* the exact no-cancellation counts 20, 938 and 84, and the 30 `F2` length-five + survivors left when only prefix cancellation is used. + +## What this does not cover + +* Width at least three, `F4` and other prime-power fields, and `F_p` for + `p ≥ 5` at length five. I did not finish a local stdlib run of `F5` at length + four, and I claim nothing from it. +* A stdlib or proof-checked replay of the `F3` length-five row. A DRAT proof + per tuple, or a symmetry-reduced faster search, would close this. +* Native conversion, restoration, tariffs, suppliers and the selected + frontier. No independent human or proof-kernel review is claimed. + +## Open next questions + +1. **A checkable F3 length-five certificate.** *Why:* it would remove the + local-SAT label from result 4. *First step:* reduce by the target-preserving + symmetries (conjugation by `diag(1,−1)` and by the swap, and the + reversal–transpose map `G → G^op`), then emit DRAT proofs for the heavy + tuples. *Blocker:* the symmetry reductions need their own soundness lines. +2. **F5 and F4 at length five.** *Why:* this is the rest of #6097's field + question at width two. *First step:* run the SAT encoding on `F5`. It has 30 + projectors and 24.3M tuples, so it needs the symmetry reduction first. `F4` + needs `GF(4)` arithmetic in place of the mod-`p` code. *Blocker:* compute. + +## Credit + +JoyboyBrian (#6097) supplied the theorem, the collision relaxation and the +controls audited here. Josie Elliston (#6048) supplied the question and the +support-only counts. Nick Petalas (#6038) supplied the four-call `xy/yx` +theorem. Wentao Li (#4089/#4093) supplied the register model, following Cinna +Davis's A5 target (#2246). Prepared for JosieElliston by Claude Opus 5.5 via +Claude Code, Apache-2.0. No frozen predecessor file is changed or copied. diff --git a/research/diagonal-pair-collision-audit/SOURCES.json b/research/diagonal-pair-collision-audit/SOURCES.json new file mode 100644 index 0000000000..40f96c767a --- /dev/null +++ b/research/diagonal-pair-collision-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/diagonal-pair-collision-audit/TASK.json b/research/diagonal-pair-collision-audit/TASK.json new file mode 100644 index 0000000000..b18a458716 --- /dev/null +++ b/research/diagonal-pair-collision-audit/TASK.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Adversarial audit of PR6097 (JoyboyBrian, head 0a24101a977a652a306dd252b009d54840e4fdc9): independent soundness review of its PROOF.md, an independent stdlib engine for the same collision relaxation restated over F_p, a local method-independent SAT cross-check over F2, and the F3 instance of PR6097 open question 2 (width two).", + "scope_change_reason": "Adversarial-audit effort on a recent unaudited finite claim, as the coordinator directed; the card is PR6097's own card. The F3 run answers PR6097's open question 2 for F3 at width two.", + "bottleneck_link": "Confirms (or refutes) a scoped all-group lower bound that closes a shared-call saving route for diagonal pair targets; the F3 row removes one field restriction. No supplier, native or kappa consequence.", + "budget_minutes": 60, + "stop_rule": "Stop at agreement or a concrete disagreement (survivor, unsound rule) with PR6097 on F2, and at the first F3 survivor or a complete F3 length-five refutation.", + "outcome": "completed", + "evidence": "README.md; verify.py (stdlib) reproduces F2 lengths 0..5 and F3 lengths 0..4 by default and F3 length 5 under --f3-full; controls listed in VERIFY.json.", + "author": "Josie Elliston (Claude Opus 5.5 via Claude Code)", + "ai_assistance": "Audit, verifier and package prepared by Claude Opus 5.5 via Claude Code for JosieElliston. No human or proof-kernel acceptance.", + "open_questions": [] +} diff --git a/research/diagonal-pair-collision-audit/VERIFY.json b/research/diagonal-pair-collision-audit/VERIFY.json new file mode 100644 index 0000000000..25c88b2e9e --- /dev/null +++ b/research/diagonal-pair-collision-audit/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 300, + "checks": "Independent F_p collision relaxation: zero survivors for all F2 tuples of length 0-5 (9331) and all F3 tuples of length 0-4 (22621); projector inventories; rule authentication; subset vs free-monoid expansion; six-call endpoint over F2/F3; acceptance of six-call and #6038 four-call words; #6097 controls; exact no-cancellation counts 20, 938 (F2) and 84 (F3)." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 300, + "checks": "Same checks under -O (explicit require(), no assert)." + } + ] +} diff --git a/research/diagonal-pair-collision-audit/sat_crosscheck.py b/research/diagonal-pair-collision-audit/sat_crosscheck.py new file mode 100644 index 0000000000..062cadd952 --- /dev/null +++ b/research/diagonal-pair-collision-audit/sat_crosscheck.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Local, method-independent SAT cross-check of the same relaxation (not registered; +needs python-sat). Used for the F3 length-five row, which the stdlib branching +search does not finish in reasonable time. + +Encoding: one variable per unordered node pair (equal classes); transitivity +clauses; each cancellation rule as an equivalence of two pair variables; each +forbidden equality as a negative unit; and, for every equation E and every node +u in E, a one-hot mod-p counter forcing sum_{v in E} w_v [v ~ u] = 0 (mod p), +i.e. u's class has total weight zero in E. A model is exactly a partition that +survives the relaxation; UNSAT refutes the projector tuple. + +Usage: sat_crosscheck.py P KMAX [--no-cancel] [--jobs N] +""" +import importlib.util +import itertools +import multiprocessing +import os +import sys +import time + +from pysat.solvers import Cadical153 + +_spec = importlib.util.spec_from_file_location( + "dpca_verify", os.path.join(os.path.dirname(os.path.abspath(__file__)), "verify.py")) +V = importlib.util.module_from_spec(_spec) +_spec.loader.exec_module(V) + + +def satisfiable(tup, p, cancel=True): + k = len(tup) + prob = V.Problem(k, p, cancellation=cancel) + eqs = prob.equations(tup) + n = (1 << k) + 2 + ids = {} + top = [0] + + def pair(u, v): + key = (min(u, v), max(u, v)) + if key not in ids: + top[0] += 1 + ids[key] = top[0] + return ids[key] + + def fresh(): + top[0] += 1 + return top[0] + + cl = [] + for u, v, w in itertools.combinations(range(n), 3): + a, b, c = pair(u, v), pair(v, w), pair(u, w) + cl += [[-a, -b, c], [-a, -c, b], [-b, -c, a]] + for U, W, U2, W2 in prob.rules: + x, y = pair(U, W), pair(U2, W2) + cl += [[-x, y], [-y, x]] + for x, y in prob.forbidden: + cl.append([-pair(x, y)]) + for E in eqs: + for u, wu in E: + cur = [fresh() for _ in range(p)] + for r in range(p): + cl.append([cur[r]] if r == wu % p else [-cur[r]]) + for v, wv in E: + if v == u: + continue + x = pair(u, v) + nxt = [fresh() for _ in range(p)] + for r in range(p): + s = (r + wv) % p + cl += [[x, -cur[r], nxt[r]], [x, cur[r], -nxt[r]], + [-x, -cur[r], nxt[s]], [-x, cur[r], -nxt[s]]] + cur = nxt + cl.append([cur[0]]) + with Cadical153(bootstrap_with=cl) as solver: + return solver.solve() + + +def _work(args): + p, k, head, cancel = args + return [(head,) + rest for rest in itertools.product(V.projectors(p), repeat=k - 1) + if satisfiable((head,) + rest, p, cancel)] + + +def main(argv): + p, kmax = int(argv[0]), int(argv[1]) + cancel = "--no-cancel" not in argv + jobs = int(argv[argv.index("--jobs") + 1]) if "--jobs" in argv else 8 + E00, E11 = (1, 0, 0, 0), (0, 0, 0, 1) + assert satisfiable((E00,) * 3 + (E11,) * 3, p), "six-call construction must be SAT" + t0 = time.time() + with multiprocessing.Pool(jobs) as pool: + for k in range(1, kmax + 1): + parts = pool.map(_work, [(p, k, h, cancel) for h in V.projectors(p)]) + surv = [t for part in parts for t in part] + print("p=%d k=%d cancel=%s tuples=%d sat_survivors=%d seconds=%d" + % (p, k, cancel, len(V.projectors(p)) ** k, len(surv), time.time() - t0), + flush=True) + + +if __name__ == "__main__": + main(sys.argv[1:]) diff --git a/research/diagonal-pair-collision-audit/verify.py b/research/diagonal-pair-collision-audit/verify.py new file mode 100644 index 0000000000..2608537f22 --- /dev/null +++ b/research/diagonal-pair-collision-audit/verify.py @@ -0,0 +1,347 @@ +#!/usr/bin/env python3 +"""Independent re-check of PR6097's five-call diagonal-pair refutation, and its +extension from F2 to F3 (width two). + +Standard library only; imports no repository code and does not read PR6097's +verifier. The relaxation is restated over F_p: a node per chronological subset +U of call positions plus nodes A, B for the targets a, b; an equivalence +relation closed under common-prefix/common-suffix cancellation (every prefix +or suffix length, both directions); forbidden equalities (g_i != e, a != b, +a, b not products of at most two labels); and, in each of the four matrix-entry +equations of sum_U [g_U] P_U = diag([a],[b]) over F_p[G], every class has +total weight 0 mod p. A refutation of the relaxation refutes every group +realization (README.md, "Soundness over F_p"). + +Usage: + verify.py F2 lengths 0..5, F3 lengths 0..4, controls + verify.py --f3-full [--jobs N] + also F3 length 5 with this search. Not registered: + single tuples need up to ~10^5 nodes and the run + takes hours; the F3 length-5 row is the local SAT + result of sat_crosscheck.py instead (README.md). +""" +import itertools +import json +import sys + +NODE_CAP = 10 ** 6 + + +def require(cond, msg): + if not cond: + raise SystemExit("FAIL " + msg) + + +def mat_mul(X, Y, p): + a, b, c, d = X + e, f, g, h = Y + return ((a * e + b * g) % p, (a * f + b * h) % p, + (c * e + d * g) % p, (c * f + d * h) % p) + + +IDENTITY = (1, 0, 0, 1) + + +def projectors(p): + """Rank-one idempotent 2x2 matrices over F_p (row-major a, b, c, d).""" + out = [] + for N in itertools.product(range(p), repeat=4): + a, b, c, d = N + if mat_mul(N, N, p) == N and N != (0, 0, 0, 0) and N != IDENTITY: + out.append(N) + return tuple(out) + + +def outer_products(p): + """Independent inventory: u v^T with v.u = 1.""" + out = set() + for u in itertools.product(range(p), repeat=2): + for v in itertools.product(range(p), repeat=2): + if (u[0] * v[0] + u[1] * v[1]) % p == 1: + out.add((u[0] * v[0] % p, u[0] * v[1] % p, u[1] * v[0] % p, u[1] * v[1] % p)) + return out + + +def subset_coefficients(tup, p): + """P_U = prod_i (N_i if i in U else I - N_i), chronological order.""" + k = len(tup) + out = {} + for U in range(1 << k): + M = IDENTITY + for i, N in enumerate(tup): + F = N if (U >> i) & 1 else tuple((x - y) % p for x, y in zip(IDENTITY, N)) + M = mat_mul(M, F, p) + out[U] = M + return out + + +def free_word_product(tup, word, p): + """Independent expansion: multiply D_N(g) = (I-N) + [g]N in the free monoid + algebra, keyed by label strings. Used only as a control.""" + poly = {"": IDENTITY} + for N, g in zip(tup, word): + IN = tuple((x - y) % p for x, y in zip(IDENTITY, N)) + new = {} + for w, M in poly.items(): + for w2, F in ((w, IN), (w + g, N)): + prod = mat_mul(M, F, p) + old = new.get(w2, (0, 0, 0, 0)) + new[w2] = tuple((x + y) % p for x, y in zip(old, prod)) + poly = {w: M for w, M in new.items() if M != (0, 0, 0, 0)} + return poly + + +def bits(U, k): + return [i for i in range(k) if (U >> i) & 1] + + +def cancellation_rules(k, suffixes=True): + """(U, V, U', V'): g_U = g_V <=> g_U' = g_V', where U, V share a common + nonempty prefix (or suffix) of positions that is removed. Every common + prefix/suffix length is emitted.""" + rules = [] + for U in range(1 << k): + pu = bits(U, k) + for V in range(U + 1, 1 << k): + pv = bits(V, k) + m = 0 + while m < min(len(pu), len(pv)) and pu[m] == pv[m]: + m += 1 + cut = sum(1 << i for i in pu[:m]) + rules.append((U, V, U & ~cut, V & ~cut)) + m = 0 + while suffixes and m < min(len(pu), len(pv)) and pu[-1 - m] == pv[-1 - m]: + m += 1 + cut = sum(1 << i for i in pu[len(pu) - m:]) + rules.append((U, V, U & ~cut, V & ~cut)) + return rules + + +def authenticate_rule(rule, k): + """Check a rule is a single common-context law on increasing sequences.""" + U, V, U2, V2 = rule + pu, pv, pu2, pv2 = (bits(x, k) for x in rule) + for split in range(1, len(pu) + 1): + ctx = pu[:split] + if pu == ctx + pu2 and pv == ctx + pv2: + return True + ctx = pu[len(pu) - split:] + if pu == pu2 + ctx and pv == pv2 + ctx: + return True + return False + + +class Contradiction(Exception): + pass + + +def root(par, x): + while par[x] != x: + x = par[x] + return x + + +def merge(par, x, y): + x, y = root(par, x), root(par, y) + if x != y: + par[max(x, y)] = min(x, y) + + +def close(par, rules, forbidden): + changed = True + while changed: + changed = False + for U, V, U2, V2 in rules: + left = root(par, U) == root(par, V) + right = root(par, U2) == root(par, V2) + if left != right: + if left: + merge(par, U2, V2) + else: + merge(par, U, V) + changed = True + for x, y in forbidden: + if root(par, x) == root(par, y): + raise Contradiction + + +class Problem: + def __init__(self, k, p, cancellation=True, min_target_labels=3, suffixes=True): + self.k, self.p = k, p + self.A, self.B = 1 << k, (1 << k) + 1 + self.rules = cancellation_rules(k, suffixes) if cancellation else [] + forb = [(0, 1 << i) for i in range(k)] + [(self.A, self.B)] + for U in range(1 << k): + if bin(U).count("1") < min_target_labels: + forb += [(self.A, U), (self.B, U)] + self.forbidden = forb + self.nodes = 0 + + def equations(self, tup): + P = subset_coefficients(tup, self.p) + eqs = [] + for entry in range(4): + E = [(U, P[U][entry]) for U in range(1 << self.k) if P[U][entry]] + if entry == 0: + E.append((self.A, self.p - 1)) + if entry == 3: + E.append((self.B, self.p - 1)) + eqs.append(E) + return eqs + + def solve(self, tup): + """Return a surviving partition of the relaxation, or None.""" + require(len(tup) == self.k, "length") + self.count = 0 + return self._search(list(range((1 << self.k) + 2)), self.equations(tup)) + + def _search(self, par, eqs): + self.count += 1 + self.nodes += 1 + require(self.count <= NODE_CAP, "node cap exceeded (not a rejection)") + par = list(par) + p = self.p + while True: + try: + close(par, self.rules, self.forbidden) + except Contradiction: + return None + branch = None + forced = False + for E in eqs: + total = {} + for node, w in E: + r = root(par, node) + total[r] = (total.get(r, 0) + w) % p + live = sorted(r for r, t in total.items() if t) + if len(live) == 1: + return None + if len(live) == 2: + if (total[live[0]] + total[live[1]]) % p: + return None + merge(par, live[0], live[1]) + forced = True + break + if live and (branch is None or len(live) < len(branch)): + branch = live + if forced: + continue + if branch is None: + return par + first = branch[0] + for partner in branch[1:]: + child = list(par) + merge(child, first, partner) + found = self._search(child, eqs) + if found is not None: + return found + return None + + +def census(p, k, first=None): + Ns = projectors(p) + prob = Problem(k, p) + heads = Ns if first is None else (first,) + tested = survivors = 0 + if k == 0: + tested, survivors = 1, int(prob.solve(()) is not None) + return tested, survivors, prob.nodes + for head in heads: + for rest in itertools.product(Ns, repeat=k - 1): + tested += 1 + if prob.solve((head,) + rest) is not None: + survivors += 1 + return tested, survivors, prob.nodes + + +def _job(args): + p, k, head = args + return census(p, k, head) + + +def dec(n): + """PR6097's row-major bit encoding over F2.""" + return (n & 1, (n >> 1) & 1, (n >> 2) & 1, (n >> 3) & 1) + + +def controls(): + for p, count in ((2, 6), (3, 12)): + Ns = projectors(p) + require(len(Ns) == count == p * (p + 1), "projector count p=%d" % p) + require(set(Ns) == outer_products(p), "outer-product inventory p=%d" % p) + require(tuple(sorted(dec(n) for n in (1, 3, 5, 8, 10, 12))) == tuple(sorted(projectors(2))), + "PR6097 encoding") + for k in range(7): + for rule in cancellation_rules(k): + require(authenticate_rule(rule, k), "rule %r" % (rule,)) + E00, E11 = (1, 0, 0, 0), (0, 0, 0, 1) + six = (E00, E00, E00, E11, E11, E11) + for p in (2, 3): + # exact symbolic endpoint of the direct six-call word + poly = free_word_product(six, "xyxyxy", p) + require(poly == {"xyx": (1, 0, 0, 0), "yxy": (0, 0, 0, 1)}, "six-call endpoint p=%d" % p) + require(Problem(6, p).solve(six) is not None, "six-call construction rejected p=%d" % p) + # subset expansion agrees with free-word expansion on distinct letters + for tup in itertools.islice(itertools.product(projectors(p), repeat=4), 0, None, 97): + free = free_word_product(tup, "abcd", p) + sub = {} + for U, M in subset_coefficients(tup, p).items(): + if M != (0, 0, 0, 0): + sub["".join("abcd"[i] for i in bits(U, 4))] = M + require(free == sub, "expansion p=%d %r" % (p, tup)) + # four-call diag([xy],[yx]) (#6038) is accepted when targets need >= 2 labels + require(Problem(4, 2, min_target_labels=2).solve((E00, E00, E11, E11)) is not None, + "four-call xy/yx construction") + require(Problem(4, 3, min_target_labels=2).solve((E00, E00, E11, E11)) is not None, + "four-call xy/yx construction F3") + # removing cancellation reopens PR6097's four-call tuple (1,5,1,10) + t = tuple(map(dec, (1, 5, 1, 10))) + require(Problem(4, 2, cancellation=False).solve(t) is not None, "no-cancel control F2") + require(Problem(4, 2).solve(t) is None, "cancel kills (1,5,1,10)") + # short targets reopen (E00, E11) + require(Problem(2, 2, min_target_labels=1).solve((E00, E11)) is not None, "short control F2") + require(Problem(2, 3, min_target_labels=1).solve((E00, E11)) is not None, "short control F3") + # PR6097's written five-call example is rejected + require(Problem(5, 2).solve(tuple(map(dec, (1, 5, 5, 3, 10)))) is None, "written example") + # Without cancellation the relaxation has exact survivor counts (F2: 20 at + # length four and 938 at length five, the counts of #6048's support-only + # relaxation; F3: 84 at length four). The local SAT encoding reproduces them. + for p, k, expected in ((2, 4, 20), (2, 5, 938), (3, 4, 84)): + relaxed = Problem(k, p, cancellation=False) + got = sum(relaxed.solve(t) is not None for t in itertools.product(projectors(p), repeat=k)) + require(got == expected, "no-cancel count p=%d k=%d: %d" % (p, k, got)) + # Prefix cancellation alone leaves 30 F2 length-five survivors: suffix + # rules are needed too. + prefix_only = Problem(5, 2, suffixes=False) + got = sum(prefix_only.solve(t) is not None for t in itertools.product(projectors(2), repeat=5)) + require(got == 30, "prefix-only control: %d" % got) + + +def main(argv): + full = "--f3-full" in argv + jobs = 1 + if "--jobs" in argv: + jobs = int(argv[argv.index("--jobs") + 1]) + controls() + results = [] + plan = [(2, k) for k in range(6)] + [(3, k) for k in range(5)] + if full: + plan.append((3, 5)) + for p, k in plan: + if jobs > 1 and k >= 4: + import multiprocessing + with multiprocessing.Pool(jobs) as pool: + parts = pool.map(_job, [(p, k, h) for h in projectors(p)]) + tested = sum(x[0] for x in parts) + surv = sum(x[1] for x in parts) + nodes = sum(x[2] for x in parts) + else: + tested, surv, nodes = census(p, k) + require(tested == len(projectors(p)) ** k, "incomplete enumeration") + require(surv == 0, "survivor at p=%d k=%d" % (p, k)) + results.append({"field": p, "calls": k, "tuples": tested, "survivors": surv, "nodes": nodes}) + print("PASS_DIAGONAL_PAIR_COLLISION_AUDIT " + json.dumps(results, sort_keys=True)) + + +if __name__ == "__main__": + main(sys.argv[1:]) From 0e4e99aa9cdf669bba789a7897d1292cd6eb06fe Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 09:14:01 -0400 Subject: [PATCH 2/3] Record open next questions in TASK.json Co-Authored-By: Claude Opus 5.5 --- research/diagonal-pair-collision-audit/TASK.json | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/research/diagonal-pair-collision-audit/TASK.json b/research/diagonal-pair-collision-audit/TASK.json index b18a458716..94bff758ec 100644 --- a/research/diagonal-pair-collision-audit/TASK.json +++ b/research/diagonal-pair-collision-audit/TASK.json @@ -53,5 +53,18 @@ "evidence": "README.md; verify.py (stdlib) reproduces F2 lengths 0..5 and F3 lengths 0..4 by default and F3 length 5 under --f3-full; controls listed in VERIFY.json.", "author": "Josie Elliston (Claude Opus 5.5 via Claude Code)", "ai_assistance": "Audit, verifier and package prepared by Claude Opus 5.5 via Claude Code for JosieElliston. No human or proof-kernel acceptance.", - "open_questions": [] + "open_questions": [ + { + "question": "Can the F3 length-five refutation be given a stdlib-replayable or proof-checked certificate?", + "why_it_matters": "Removes the local-SAT label from the F3 six-call floor.", + "first_step": "Reduce by conjugation by diag(1,-1), by the swap, and by reversal-transpose (G to G^op), then emit DRAT proofs for the heavy tuples.", + "blocked_by": "The symmetry reductions need their own soundness argument." + }, + { + "question": "Does the six-call floor hold over F5 and F4 at width two?", + "why_it_matters": "The rest of #6097's field question at width two.", + "first_step": "Run the SAT encoding on F5 (30 projectors, 24.3M length-five tuples) after symmetry reduction; F4 needs GF(4) arithmetic.", + "blocked_by": "Compute." + } + ] } From 3168ef5a4950ac07b72768adca1b25a49c282c23 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 09:21:48 -0400 Subject: [PATCH 3/3] Record the packaged F3 length-five SAT run Co-Authored-By: Claude Opus 5.5 --- research/diagonal-pair-collision-audit/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/research/diagonal-pair-collision-audit/README.md b/research/diagonal-pair-collision-audit/README.md index 7590f2b384..7b8d36d096 100644 --- a/research/diagonal-pair-collision-audit/README.md +++ b/research/diagonal-pair-collision-audit/README.md @@ -44,7 +44,7 @@ direct six-call word shows the bound is exact. 4. **New: the same six-call floor holds over F3 at width two.** Over `F3` there are 12 rank-one idempotents (`p(p+1)`). The stdlib engine refutes all tuples of length 0–4: 22,621 of them, registered. The local SAT run refutes all - 248,832 tuples of length five, in 555 s on 8 cores. The direct six-call word + 248,832 tuples of length five (783 s with 9 workers; an earlier prototype of the same encoding also found none). The direct six-call word works over every field. So under #6097's hypotheses the minimum over `F3` is also **exactly six**. This answers #6097 open question 2 for `F3` at width two. The length-five row is **local SAT evidence**, not a stdlib replay. @@ -91,7 +91,7 @@ python3 -I -W error -B research/diagonal-pair-collision-audit/verify.py # ~ python3 -I -O -W error -B research/diagonal-pair-collision-audit/verify.py # local only, needs python-sat: python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 2 5 -python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 3 5 --jobs 8 # ~10 min +python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 3 5 --jobs 8 # ~13 min python3 -I -B research/diagonal-pair-collision-audit/sat_crosscheck.py 3 4 --no-cancel # 84 ```