[petalas]

Summary

FALLBACK.md in research/unconditional-batched-crt (#4100) bounds the retained BIT fallback program at m = 64 by 16637 swaps and 3 × 16637 = 49911 reversed children. This PR gives the exact count for every header and its sharp maximum:

m = 64, f >= 2: at most 33269 children (FALLBACK.md: 49911)
                at most 16637 swaps    (FALLBACK.md's count is attained)

Claim type: scoped proof with a finite certificate for one tape-cost term. No new κ, no audit of other #4100 premises, no supplier admission and no change to the selected frontier. Package: research/fallback-child-count. Claim.

Result

For a rank-r projector header (1 ≤ r < m), let s be the number of same-bank elimination swaps.

1. Rank law (proved). The head phase of the unnormalized residual elimination makes exactly r opposite-bank swaps. The proof is a dimension count: the reduced unused head rows span a space of dimension dim(H+V_k) − k, which drops by one at each head pivot and stays fixed at each tail pivot. It follows that s ≤ 2m − 1 − r.
2. Closed forms (proved). The program has N = (2m−1)(2m+2) + r + s swaps, of which S = 2(m²−1) + s are same-bank. paid_children pays 8m² + 2m − 6 + r + 3s children when f ≥ 2 and N children when f = 1. The total width is fN + 2⌊f/2⌋S.
3. Sharp maximum. There are at most 8m² + 8m − 11 children when f ≥ 2, and at most (2m−1)(2m+3) swaps. The rank-one header P = 1·e₀ᵀ attains both, for every odd prime power and every 2 ≤ m ≤ 64. Over Q, every intermediate entry of its elimination stays in {−1, 0, 1}, so its itinerary is the same modulo every odd prime power.

This answers PR4215's Open next question 2 and the matching open question in PR4228's package.

Evidence

verify.py loads the unchanged prepare/paid_children path after checking SHA256 pins. It checks:

• the witness for every 2 ≤ m ≤ 64 with f ∈ {1, 2, 3}, over (q,w) = (3,1) at every m, and also over (3,2), (5,1) and (7,2) at m ∈ {2, 3, 64};
• complete idempotent censuses for (q,m) = (3,2), (3,3), (5,2) and (7,2): 332 idempotents, each count matched to q^{r(m−r)}[m choose r]_q;
• 24 seeded m = 64 headers with ranks from 1 to 61, as a control only;
• controls: the recomputed 16637 and 49911, and a bank-interchange matrix with 64 opposite swaps, which shows the rank law needs the residual structure.

Exact reproduction from the repository root:

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

Any CPython 3.12 works. Expected markers: PASS_REGISTERED_RESEARCH_PACKAGE research/fallback-child-count outcome=completed, PASS_RESEARCH_COMMIT_BYTES and "status": "PASS_FALLBACK_CHILD_COUNT". Locally, all four passed, and each verify command took about 25 seconds.

Limitations and unrun obligations

This counts what paid_children charges for the retained program. It does not execute physical reversals, price preparation or parking, decide which headers reach the fallback, or audit BIT.md's recurrence. The maximum is attained at rank one, and in the censuses only there, so an actual caller may pay less. The bound s ≤ 2(m − r) for every rank is an observation from the censuses, not a proof. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Prove s ≤ 2(m − r) for every rank-r header, which would give the exact rank-dependent maximum 8m² + 8m − 6 − 5r, or find a counterexample.
2. Bind the auxiliary BIT recurrence's fallback branch to its header ranks, then substitute the rank-dependent count for the uniform 49911.

Related open work

• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215 checks PR4100's good-packet normal form and raises this question. Its quoted 49911 equals 3 × 16637 as recomputed here. Its normal-form check is not rerun.
• Prove exact intermediate-rank BIT header densities #4228 proves exact intermediate-rank BIT header densities. That is a different quantity, the good-header fraction, and no shared number is compared. Its package lists this question as open.
• Prove exact extreme-rank BIT header densities #4227 proves extreme-rank BIT header densities. That is also a different quantity, with no overlapping count.
• Construct a paid pivoted BIT fallback with at most 1+12r children #4235 builds a different, pivoted fallback for the same Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 BIT bad-packet path. Both quote the retained envelope 49,911 = 3 × 16,637, and that number agrees. Its bound of at most 1+12r children (505 at r = 42, m = 64) includes one width-rf child, whereas every child here has width at most f. The two bills therefore count different quantities and are not compared.
• Conditional kappa = 0.001274032592088050: sharper bit bad-class charge on #458 #461, Conditional kappa = 0.001283479306671789: certified R715 assembly with sharp bit charge #465 and Conditional κ = 0.001295625678120464: whole-owner GL cover with sharp fallback #490 (all open; cited as earlier sharper fallback pricing in research/selected-bit-bad-class-fallback) price an earlier Gaussian local-ring fallback at m = 78. They use the uniform count 6N(N−1) + 3N + 6(N−1) rank-one children with N = 2m, which charges every swap alike and has no orientation or rank dependence; at m = 64 it would be 98,682. None of them states the orientation-aware count or the rank law for the fallback program Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 retains.

CI notes

Hosted run 39488451544 is green on head 34af2cd420ccf5339ce05e3aefe5c569aaf17f85: plan passed in 2m55s and the package replay passed in 3m32s. All four reproduction commands also passed locally. No local obligation was left to CI.

Produced by Nick Petalas. Apache-2.0. The fallback program and descriptors are retained from source527, commdata2338, Ross Richardson (PR2159/PR2188) and Jose Manuel; FALLBACK.md is from #4100.

[rcfc-jreed]

Independent scoped audit of #4237 sharp fallback child count at 34af2cd4: 13/13

Code-disjoint checks; nested PACKAGE/ROOT fork of package verify.py (does not import it as a library). Package bytes from head 34af2cd420ccf5339ce05e3aefe5c569aaf17f85 via GitHub contents API. CLAIM.

No packaging defect in SOURCES scope. All 7 SOURCES.json digests match the sealed tree.

What passes:

1. Fork verify status PASS_FALLBACK_CHILD_COUNT.
2. Controls: sharp_children_m64_f3 = 33269, retained bound 49911.
3. README states the sharp count vs the looser FALLBACK.md bound.

Not covered here: physical fallback execution; BIT recurrence retuning; new κ; Lean; merge/close.

Finite pin/seal/census replay ≠ formal proof / all-size admission.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).