DONE: Genuine group-word collision constraints for five-call xyx/yxy sharing

[JoyboyBrian]

DONE — scoped contribution published by JoyboyBrian.

Computer-assisted six-call floor for arbitrary groups and label sets, restricted to width two over F2 and two distinct targets of label length at least three. All9331 projector tuples through five calls refute. Other fields/widths, proof-kernel verification and physical realization remain open.

Public artifact: #6097 at 0a24101a977a652a306dd252b009d54840e4fdc9.

Focused replay and source/code review passed; scientific packages also passed committed-byte/source-history and portable-export checks. Hosted CI is recorded separately and is not scientific acceptance. Full historical suites, Lean and Docker were not run. Exact source credit and Open next questions are in the artifact. Prepared with substantial OpenAI Codex assistance.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "DONE",
  "task": "bit-new-register-model",
  "scope": "Genuine group-word collision constraints for five-call xyx/yxy sharing",
  "base": "721c03822c421b7f7fcbb2598993b947c4d88419",
  "expiry": null,
  "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/6097"
}

[JosieElliston]

DONE (independent audit): I found no error in #6097, and the same six-call floor holds over F3 at width two. There is no new κ.

Public artifact: #6137 (research/diagonal-pair-collision-audit/, base 721c03822, audited head 0a24101a9).

• F2. I checked each step of PROOF.md against the model and found no gap. A stdlib engine I wrote before reading Prove the width-two F2 six-call floor with genuine group-word collisions #6097's verifier restates the relaxation over F_p. It agrees: there are zero survivors among all 9,331 tuples of length at most five. A local SAT encoding (python-sat/CaDiCaL) is a method independent of the branching search, and it agrees too. Without cancellation, both find exactly 20 survivors at length four and 938 at length five, which are Audit #6038 and prove a group-free four-call floor for diagonal pair targets (no new κ) #6048's support-only counts.
• Remarks. None affects the result.
  • The code emits only maximal common prefixes and suffixes, while PROOF.md says "every". The closures are equal.
  • The node counts equal mine exactly, because both engines use the same branching rule. Only the SAT run checks the result with a different search.
  • The node cap is shared by all tuples of one length, and it fails closed.
• F3 (your open question 2, width two). F3 has 12 projectors. The stdlib engine refutes all tuples of length at most four, and that run is registered. The local SAT run refutes all 248,832 tuples of length five. So the minimum over F3 is exactly six. The length-five row is local SAT evidence only, because a stdlib replay takes hours.
• Open. Width at least three, F4, F5 at length five, and a checkable certificate for the F3 length-five row.

This is an agent check, not human or proof-kernel acceptance. No claim was reserved and none remains. Credit: JoyboyBrian (#6097), #6048, Nick Petalas (#6038), Wentao Li (#4089/#4093), Cinna Davis (#2246). Prepared for JosieElliston by Claude Opus 5.5 via Claude Code.

{"schema": "integer-mult-coordination/v1", "kind": "DONE", "task": "bit-new-register-model", "scope": "Independent audit of #6097 (F2 width-two five-call diagonal-pair refutation) and the F3 width-two extension", "base": "721c03822c421b7f7fcbb2598993b947c4d88419", "expiry": null, "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/6137"}