[JosieElliston]

Independent finite corroboration of #5481; no new κ. Package research/bit-span4-five-call-two-relation.

JoyboyBrian's merged #5481 (research/bit-fivecall-dirty-block) proves in writing that three invertible 2×2 targets need six rank-one calls in the formal abelian BIT model with any number of dirty auxiliaries. That closes open question 1 of research/bit-span4-auxiliary-structure and the eight-call span-four case. Its README says no five-call word enumeration was run, and the inherited low-span, one-relation and three-register lemmas were cited, not re-proved.

This PR runs that enumeration. Three data registers with one auxiliary (W = 4) are in the default replay, and two auxiliaries (W = 5) are in --long. W = 2, 3 are also covered. The census includes every relation lattice of rank at most 2, so every five-call word of frame span at least 3. It uses neither the conic argument nor the one-relation or three-register theorems.

Result. No diagonal five-call word at W ≤ 5 has three registers whose endpoint class is not 0 or ±A_j modulo the relations. The maximum is two, and it is attained. An invertible 2×2 target is never such a class, so this agrees with #5481 for one and two auxiliaries.

How the 120^5 search becomes small

1. Two call subsets share an address iff 1_S - 1_T is in L ∩ {-1,0,1}^5. So only the saturation of that cube part matters. That leaves 4,060 rank-2 lattices with nonzero frames, plus 117 of rank ≤ 1.
2. Derivative condition over F2 (seed04's step 1, with one more relation): offdiag N_j = (b1)_j M1 + (b2)_j M2 mod 2 for a Z-basis b1, b2 of L. Each call's pattern is therefore fixed by its column class. Non-zero patterns have at most 2 lifts, and the zero pattern has W.
3. One representative per register-permutation orbit, weighted by orbit size. The weighted counts equal the unreduced run at W = 2.

Evidence (CPython 3.12, stdlib only)

• W = 4, rank-2 lattices: 18.8M orbit representatives (222M words), 9,388,016 diagonal, high histogram 0/1/2 = 2,843,284 / 4,763,716 / 1,781,016. Rank ≤ 1: 183,432 diagonal. W = 5 (--long): 71.4M representatives (3.04G words), 53,463,710 diagonal, 0/1/2 = 28,198,385 / 21,187,785 / 4,077,540; rank ≤ 1: 785,591 diagonal.
• Unpruned cross-checks enumerate every word for every lattice at (W,k) = (2,4) and (3,3), plus (2,5) with --long. Each finds identical diagonal sets and histograms, and no diagonal word violates step 2.
• Five controls: the detector fires on six coordinate calls, a cancelling pair is low, non-diagonal rejection, D_N(B)D_N(-B) accepted, saturated bases.
• python3 -I -B research/bit-span4-five-call-two-relation/verify.py (about 3 min) → PASS_FIVE_CALL_TWO_RELATION_CENSUS ...; --long adds W = 5. Registered replay: PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=negative-result (python3.12, 2m44s); the --long run (CPython 3.14, macOS) wrote the W = 5 and (2,5) rows.
• OpenAI Codex read-only adversarial review: no gap in steps 1–2, the enumeration, orbit weights, diagonal acceptance or the high test. Its must-fix was the then-pending W = 5 receipt (now recorded). Its should-fix on control 5's description was applied. This is not independent human review.

Scope. This is a finite census in a formal model. It is not a proof for three or more auxiliaries and does not re-check the conic argument. Frame span ≤ 2 is cited (Lemma 2 of bit-dirty-auxiliary-registers). The high test is a necessary condition only. No physical supplier, pricing, compiler or recursive-bill obligation is addressed. The selected record is unchanged.

Open next questions. (1) Prove "at most two high registers" for every W, which would give a conic-free proof of #5481. (2) Use the derivative condition to prune #5481's remaining eight-call span-5/6 cases.

Overlap. I chose the span-four open question first. The overlap check then found #5481, so I reframed the work as corroboration. The span-four README's open question 1 is now stale. That package is frozen, so I did not edit it.

Credit. unpaidmoon (span-four reduction), JoyboyBrian #5481 (the theorem corroborated here), waynenilsen (dirty-auxiliary lemmas), Ali Romman #468, eumemic #288, huxint #203, Hanson Sun (seed04 derivative step), and the seed52 and woklerx pattern-plane censuses. Card bit-new-register-model, seed df1ea4ba466d07a5fa28dab974fcdd78, base 721c0382 (priority revision 8).

Prepared for Josie Elliston with substantial assistance from Claude (Anthropic). No independent human review is claimed. Apache-2.0.

🤖 Generated with Claude Code