[JosieElliston]

This is an independent adversarial audit of #6097's five-call diagonal-pair refutation, plus the same floor over F3. No new κ. It adds only research/diagonal-pair-collision-audit/.

Audit (F2, width two). I found no error in #6097's PROOF.md. I checked the basis-change normalization, dropping identity-labelled calls, cancellation, the forbidden equalities, parity, and the completeness of partner branching. Two methods agree with its zero survivors for all 9,331 tuples of length at most five:

• a stdlib engine I wrote before reading Prove the width-two F2 six-call floor with genuine group-word collisions #6097's verifier, which restates the relaxation over F_p;
• a local SAT encoding (python-sat/CaDiCaL), a method independent of the branching search.

Without cancellation, both find exactly 20 survivors at length four and 938 at length five. These are #6048's support-only counts. I have three remarks, and none affects the result:

• Prove the width-two F2 six-call floor with genuine group-word collisions #6097's code emits only maximal common prefixes and suffixes, but its PROOF.md says "every" prefix and suffix. The two closures are equal; the README gives the short argument.
• Its node counts equal my engine's exactly (1,392 and 10,634). Both use the same branching rule, so only the SAT run checks the result with a different search order.
• Its node cap is shared by all tuples of one length, and it fails closed.

Extension (F3, width two). F3 has 12 rank-one idempotents. The stdlib engine refutes all 22,621 tuples of length at most four, and this run is registered. The local SAT run refutes all 248,832 tuples of length five. 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: a stdlib replay takes hours, and single tuples need ~1.4·10⁵ nodes. Without cancellation, F3 has exactly 84 survivors at length four, so the F3 result depends on cancellation as the F2 one does.

Checks. python3 -I -W error -B research/diagonal-pair-collision-audit/verify.py (also run with -O) takes ~30 s and prints PASS_DIAGONAL_PAIR_COLLISION_AUDIT. Its controls check:

• the projector inventories, against an independent u vᵀ enumeration;
• every cancellation rule, as a single context law;
• the subset expansion, against a free-monoid expansion;
• the six-call endpoint over F2 and F3, and acceptance of the six-call and Prove the conjugate-pair target needs four calls in every group (no new κ) #6038 four-call words;
• Prove the width-two F2 six-call floor with genuine group-word collisions #6097's (1,5,1,10), short-target and written-example controls;
• the exact no-cancellation counts 20, 938 and 84, and the 30 F2 length-five survivors left with prefix cancellation only.

research_package.py --package passes. The SAT script sat_crosscheck.py is included but not registered, because it needs python-sat. A read-only Codex review found no errors; it could not rerun the SAT row.

Not covered. This does not cover width at least three, F4, or F5 and larger primes at length five. There is no stdlib or proof-checked certificate for the F3 length-five row. It also does not cover native conversion, restoration, tariffs, suppliers or the selected frontier. There is no human or proof-kernel acceptance.

Base 721c03822c421b7f7fcbb2598993b947c4d88419. The audited head is #6097 0a24101a977a652a306dd252b009d54840e4fdc9; this package does not import or copy its files.

Credit: JoyboyBrian (#6097: the theorem, the relaxation and the controls), Josie Elliston (#6048), Nick Petalas (#6038), Wentao Li (#4089/#4093) and Cinna Davis (#2246). Prepared for JosieElliston by Claude Opus 5.5 via Claude Code.

🤖 Generated with Claude Code