Audit #6097's five-call diagonal-pair floor: no error, two independent engines agree; the same six-call minimum holds over F3 (no new κ)

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 (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.
+   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   # ~13 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.

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"
+    }
+  ]
+}

research/diagonal-pair-collision-audit/TASK.json

@@ -0,0 +1,70 @@
+{
+  "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": [
+    {
+      "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."
+    }
+  ]
+}

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)."
+    }
+  ]
+}

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:])