[petalas]

Result

The retained BIT fallback elimination's swap counts add over direct sums of headers, and its same-bank swap excess e = s − 2(m − r) is unbounded. This answers open question 2 of #4247 (can the excess exceed one?): yes, and it grows at least linearly.

• Scoped proof (field model). For P = P₁ ⊕ P₂, the opposite-bank, same-bank and tail-phase swap counts of the first-unit elimination over F_q are the sums of the blocks' counts. The residual splits into two position classes; every pivot and row operation stays inside one class, and the increasing relabelling keeps pivot order and bank side. The proof is in the README. Transfer to the retained Z/q^w program uses Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's reduction to F_q, which is cited, not reproved.
• Finite certificates (retained code). New atoms H8 (m = 8, r = 4, s = 10, e = 2) and K13 (m = 13, r = 7, s = 17, e = 5), plus Refute the rank-dependent fallback swap bound s ≤ 2(m − r): s = 7 at m = 6, r = 3 (no new κ) #4247's G6 (e = 1), checked over Z/3^w for w = 1, 2, 3 and f = 1, 2, 3. K13^{⊕k} ⊕ I has excess 5⌊m/13⌋ for every 13 ≤ m ≤ 64. At m = 64, K13^{⊕4} ⊕ H8 ⊕ I₄ has r = 36, s = 78, e = 22 and pays 33160 children, 66 more than the refuted rank-r formula 8m² + 8m − 6 − 5r.
• Consequence. E(m), the largest excess over F₃, is superadditive, so E(m)/m converges to a limit in [5/13, 1). At f ≥ 2 a header pays 8m² + 8m − 6 − 5r + 3e children, so a rank-dependent bill cannot stay within a constant of that formula. Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's uniform maximum 8m² + 8m − 11 (33269 at m = 64) is not contradicted.

H8 and K13 came from a hill-climbing search. The search is not evidence; the verifier only replays the fixed charts. No new κ, no other #4100 premise audited, no supplier admission, no frontier change.

Evidence and reproduction

research/fallback-swap-excess-unbounded/verify.py checks the SHA256 pins, imports the unchanged research/selected-bit-recursive-closure/vendor program and checks:

• the three atoms: rank law, Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237's closed forms and 2m − 1 − r ceiling, stated excess, 3 children per unit of excess, agreement with an independent F_q elimination;
• direct-sum additivity exhaustively on 470,804 ordered idempotent pairs of every rank (including 0 and full): block sizes {1, 2, 3} over F₃, {1, 2} over F₅, and 4 against {1, 2} over F₃;
• families H8^{⊕k} ⊕ I and H8^{⊕k} ⊕ W for every 8 ≤ m ≤ 64, K13^{⊕k} ⊕ I for every 13 ≤ m ≤ 64, and the m = 64 header, through the retained code;
• the field-model rank grid H8^{⊕k} ⊕ W ⊕ I (excess 2k for 4k < r ≤ m − 4k) for 8 ≤ m ≤ 32.

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/fallback-swap-excess-unbounded/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/fallback-swap-excess-unbounded/verify.py --quick

Expected status PASS_FALLBACK_SWAP_EXCESS_UNBOUNDED. Locally the full run takes 30 s and the quick run 6.5 s.

Limitations

• The exact rank-r maximum of s and lim E(m)/m are open. Denser atoms may exist.
• The direct-sum law is proved for the field model; the retained-code checks cover m ≤ 64 directly.
• Atoms and families are checked over F₃ only.
• The package counts what paid_children charges. It does not decide which headers reach the fallback or audit BIT.md's recurrence.
• Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. What is lim E(m)/m? It lies in [5/13, 1); any denser atom raises the lower bound at once. First step: search indecomposable headers at m = 9…16 seeded from sums of the known atoms.
2. Is the ceiling s ≤ 2m − 1 − r attained (e = r − 1) at any r ≥ 2? K13 has e = 5 against a ceiling of 6.
3. Which headers reach the fallback in the auxiliary BIT recurrence? A restricted header class could still admit a tight rank-dependent bill.

Related open work

• Refute the rank-dependent fallback swap bound s ≤ 2(m − r): s = 7 at m = 6, r = 3 (no new κ) #4247 (research/fallback-swap-rank-bound): the predecessor whose open question 2 this answers. Its m = 6 header G6 is reused as an atom; this package reproduces s = 7 and 318 children at f = 2 for it, checked numerically. Its excess-one families are direct sums of G6 with excess-zero blocks, consistent with the additivity law.
• Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237 (research/fallback-child-count): rank law, closed forms, reduction to F_q and rank-one witness, all used here. Its closed forms are checked on every header in this package, and every header obeys its ceiling s ≤ 2m − 1 − r and uniform maximum.
• Prove a pivot-policy swap floor for the pivoted BIT fallback: at least 385 of 505 boundary children remain (no new κ) #4245 and Construct a paid pivoted BIT fallback with at most 1+12r children #4235: a different, pivoted fallback program; their swap counts are of another 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.

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

CI notes

Locally, on commit 3f4767099a29dd8a528d0a0932ab67010255aabf: research_package.py gives PASS_REGISTERED_RESEARCH_PACKAGE, check_research_commit.py --check-source-history gives PASS_RESEARCH_COMMIT_BYTES, and both registered commands pass. Hosted CI is green on that head in run 39505201733: plan passed in 2m35s and the package replay in 2m5s. 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, and #4247 for the G6 header; 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.