[petalas]

Result

#4237 proves that the retained BIT fallback elimination makes exactly r opposite-bank swaps and s ≤ 2m − 1 − r same-bank swaps for a rank-r header, so at f ≥ 2 paid_children pays 8m² + 2m − 6 + r + 3s children. Its first open question asks whether s ≤ 2(m − r) always, which would make 8m² + 8m − 6 − 5r the exact rank-r maximum. It does not.

m = 6, r = 3 over Z/3^w (w = 1, 2, 3):  s = 7 > 6,  318 children > 315
every 6 ≤ m ≤ 64, r = m − 3:             s = 7 > 6,  3 children above the formula
every 8 ≤ m ≤ 64, r = 4:                 s = 2(m − 4) + 1, 3 children above the formula

The m = 6 chart over F₃, with axes {0, 1, 2}:

[[1,2,1,0,0,0],[2,0,0,0,2,0],[0,0,2,0,2,0],[1,2,0,0,0,2],[2,1,1,2,1,0],[1,2,0,0,2,2]]

It makes 3 head-phase and 4 tail-phase same-bank swaps. Family A is diag(G6, I) and family B is diag(G6, #4237's rank-one witness). Complete idempotent censuses for (q, m) = (3, 2), (3, 3), (3, 4), (3, 5) and (5, 3) obey the bound, with maximum exactly 2(m − r) per rank. So m = 6 is the smallest violating dimension over F₃.

Claim type: finite certificate. It refutes a conjectured formula through the unchanged retained code. It does not determine the true rank-r maximum. No new κ, no audit of other #4100 premises, no supplier admission and no selected-frontier change. Package: research/fallback-swap-rank-bound. Claim.

Evidence

verify.py checks the SHA256 pins (the same three vendor files #4237 pins), then runs the unchanged prepare/paid_children path:

• the m = 6 header for (q, w) ∈ {(3,1), (3,2), (3,3)} and f ∈ {1, 2, 3}: rank law, Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's swap and child closed forms, the 2m − 1 − r ceiling and the excess;
• families A and B for every m in their ranges;
• a rank-one control: Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's witness at m = 6 attains 2(m − r) and does not exceed it.

A separate F_q elimination, cross-checked against the vendor path on the counterexample, runs the censuses (counts matched to q^{r(m−r)}[m choose r]q) and checks that diag(1·e₀ᵀ, I{r−1}) attains 2(m − r) for q ∈ {3, 5}, m ≤ 12.

Reproduce from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/fallback-swap-rank-bound/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/fallback-swap-rank-bound/verify.py --quick
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fallback-swap-rank-bound
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fallback-swap-rank-bound --check-source-history

Expected status: PASS_FALLBACK_SWAP_RANK_BOUND_REFUTED. Local timing: research_package.py runs both registered commands in 97 s; the full command uses about 95 s of CPU, mostly the (3, 5) census of 1.78 million idempotents; --quick skips only that census and takes about 7 s.

Limitations and unrun obligations

• The exact rank-r maximum of s for 2 ≤ r ≤ m − 2 is open. Every header found has excess at most one; a larger excess is not excluded.
• Families A and B are checked over F₃ only. The m = 6 counterexample holds for every Z/3^w by Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's reduction to F_q, checked at w ≤ 3.
• The counterexample was found by an uncommitted local hill-climbing search. The verifier replays only fixed charts.
• The (3, 6) census (about 6.7 × 10⁸ rank-3 idempotents) was not run.
• No physical reversal, recurrence binding or other Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 premise is checked. Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's uniform maximum 8m² + 8m − 11 is unaffected. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. What is the exact rank-r maximum of s for 2 ≤ r ≤ m − 2? Start by bounding the tail-phase swaps in terms of the displaced head rows; the head phase is already capped at m − r.
2. Can the excess s − 2(m − r) exceed one?
3. Which header ranks reach the fallback in the auxiliary BIT recurrence? Until the maximum is known, a rank-dependent bill can use only the proved ceiling 2m − 1 − r.

Related open work

• Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237 (head 34af2cd420ccf5339ce05e3aefe5c569aaf17f85): the predecessor whose open question 1 this answers. Its closed forms are reproduced on every header here; at m = 6 its formula predicts 8·36 + 12 − 6 + 3 + 3·7 = 318 children, which equals paid_children, checked numerically. Its census maxima at (3, 2) and (3, 3), max s = 2(m − r), agree with this package's separate enumeration. Its uniform maximum is not contradicted.
• Prove a pivot-policy swap floor for the pivoted BIT fallback: at least 385 of 505 boundary children remain (no new κ) #4245 (head b55d08ec08b08bea170aea5b28e33c81411365c9): a pivot-policy swap floor for Construct a paid pivoted BIT fallback with at most 1+12r children #4235's pivoted compiler on M = P C. Its s counts paid swaps of a different program, so no number is compared.
• Construct a paid pivoted BIT fallback with at most 1+12r children #4235: a different, pivoted fallback for the same Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 bad-packet path. It counts a different program, so no number is compared.
• Prove exact intermediate-rank BIT header densities #4228 and Prove exact extreme-rank BIT header densities #4227: header densities, a different quantity with no shared number.
• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215: raises the orientation-aware count that Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237 settles; not rerun.

Fresh overlap included the open PR list, this account's PRs, the latest 30 handoff comments, a title search for "fallback same-bank swap" and a grep of merged package READMEs for "same-bank" and "2(m − r)".

CI notes

Locally, research_package.py (PASS_REGISTERED_RESEARCH_PACKAGE), check_research_commit.py --check-source-history (PASS_RESEARCH_COMMIT_BYTES) and both registered commands pass on commit 1ed4cf2ed0da7946a06587901356927a5c11c8ca. Hosted CI is green on that head in run 39494001266: plan passed in 2m50s and the package replay in 5m12s. No check failed, and no local obligation was left to CI.

Produced by Nick Petalas. Credit #4237 for the rank law, closed forms, reduction to F_q and rank-one witness; the fallback program and descriptors are retained from source527, commdata2338, Ross Richardson (PR2159/PR2188) and Jose Manuel's continuation; FALLBACK.md comes from #4100. Independent human and formal proof-kernel review are unclaimed. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4247 fallback swap rank-bound refutation at 1ed4cf2e: 10/10

Code-disjoint local fork. Head 1ed4cf2ed0da7946a06587901356927a5c11c8ca. CLAIM.

No packaging defect. PASS_FALLBACK_SWAP_RANK_BOUND_REFUTED. Pins + vendor SOURCES digests; fork rc=0.

Finite replay ≠ formal proof. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).