[petalas]

Summary

#4235's paid pivoted BIT fallback uses a first-unit pivot rule and proves at most s <= 2r paid swaps, so at most 1+12r children (505 at the retained m = 64, r <= 42 boundary). Its open question 2 asks whether another pivot policy can reduce the swaps. This PR bounds how much any policy can gain:

every pivot policy, diagonal suffix projector D_r:  s >= 2 min(r, m-r)   (attained)
m = 64, r <= 42, f >= 2: best policy's worst packet >= 385 children  (#4235: <= 505)
m = 64, r <= 42, f = 1:                              >= 129 children  (#4235: <= 169)

Claim type: scoped proof with a finite certificate. No new κ, no supplier admission, no audit of #4235 or #4100, and no change to the selected frontier. Package: research/bit-pivot-policy-floor. Claim.

Result

The compiler family is #4235's: at stage k a policy may take any unit pivot in residual rows k..m-1 and columns 0..m-1-k of M = P C. A head swap is paid if the row is not k and a tail swap if the column is not m-1-k. Ordered clearing ADDs follow.

1. Floor (proved). On D_r = diag(0^(m-r), 1^r) every policy pays at least 2 min(r, m-r) swaps. Zero rows and columns of M keep zero residual, and swaps only move zero labels out of the way of later stages. So each stage k < min(r, m-r) pays both a head swap and a tail swap.
2. Attainment (proved). An explicit policy pays exactly 2 min(r, m-r).
3. Boundary consequence (proved). For r <= 32 the bound s <= 2r is sharp for every policy. Across r <= 42, a changed pivot policy can save at most 120 worst-case children (40 when f = 1), and only in ranks 33 to 42.
4. Optimal-policy census (finite certificate). Exhaustive optimal-policy search over all 142,070 idempotents in 13 complete (q, m, r) domains over F3 and F5. The worst case equals the floor except at corank one, where s*(m, m-1) = 3 at m = 4, 5, 6 (F3) and m = 4 (F5), while the first-unit rule pays 2r (up to 10). So the floor is not sharp above m/2, and a better rule does gain there.

Evidence and reproduction

verify.py is standalone; #4235 is unmerged, so it reimplements the stage process. It checks each census count against q^(r(m-r)) [m choose r]_q, computes exact optimal and first-unit swap counts per idempotent, checks the suffix optimum equals the floor, runs the explicit policy and the first-unit rule on all 63 literal m = 64 suffix fixtures, recomputes the boundary bills, and rejects a zero home pivot.

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bit-pivot-policy-floor
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-pivot-policy-floor --check-source-history
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/bit-pivot-policy-floor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/bit-pivot-policy-floor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/bit-pivot-policy-floor/verify.py --extended   # opt-in, several minutes

Expected markers: PASS_REGISTERED_RESEARCH_PACKAGE research/bit-pivot-policy-floor outcome=completed, PASS_RESEARCH_COMMIT_BYTES and "status": "PASS_BIT_PIVOT_POLICY_FLOOR". Locally all four registered/package commands passed; each verify command took about 37 seconds. The opt-in run adds m = 5, ranks 2 and 3 over F3.

Limitations and unrun obligations

The floor holds for the declared compiler family and only for the projector D_r. A different normal form, pivot positions or swap pricing is outside it. The census optima are finite facts for the listed fields and sizes, not a formula. Whether the best policy reaches 385 at the boundary depends on s*(64, r) <= 64 for 33 <= r <= 42, which is open. No caller is built; preparation, routing and stock costs stay caller obligations as in #4235. Independent human and formal proof-kernel review are unclaimed.

Open next questions

1. Determine s*(m, r) for m/2 < r < m. Is s*(m, m-1) = 3 for every m >= 4? A bound s* <= 2(m-r)+2 would make the best-policy boundary maximum exactly 385.
2. Find a polynomial-time pivot rule that attains s*. The home-first greedy rule is not optimal (10 against 3 at m = 6, r = 5).

Related open work

• Construct a paid pivoted BIT fallback with at most 1+12r children #4235 defines the compiler and proves s <= 2r. Its attained 2r on suffix projectors agrees with this package's first-unit runs on all 63 m = 64 fixtures; its 1+12r = 505 and 1+4r = 169 boundary bounds are recomputed here.
• Prove the sharp fallback child count: 33269, not 49911, at m = 64 (no new κ) #4237 counts children of the retained, unpivoted Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 fallback program (33269 at m = 64). Different algorithm and bill; no shared number.
• Independently check PR4100's good-packet normal form on small rings (no new κ) #4215 checks Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100's good-packet normal form; not rerun here.

CI notes

Both jobs passed on head b55d08ec0: plan and replay (research/bit-pivot-policy-floor) (2m22s). The opt-in --extended run is not registered in CI; it passed locally (882,090 idempotents for each of m = 5, r = 2, 3 over F3, optimal worst case 4 in both, equal to the floor).

[rcfc-jreed]

Independent scoped audit of #4245 BIT pivot-policy floor at b55d08ec: 7/7

Code-disjoint local fork. Head b55d08ec08b08bea170aea5b28e33c81411365c9. CLAIM.

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

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