From b55d08ec08b08bea170aea5b28e33c81411365c9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 21:34:15 +0100 Subject: [PATCH] feat(research): prove a pivot-policy swap floor for the pivoted BIT fallback Every pivot policy of the paid pivoted fallback pays at least 2 min(r, m-r) swaps on the diagonal suffix projector, and an explicit policy attains it. At m = 64, r <= 42 the best policy's worst packet still needs at least 385 children (f >= 2). Complete optimal-policy idempotent censuses show the floor is exceeded at corank one. --- research/bit-pivot-policy-floor/README.md | 173 +++++++++++++ research/bit-pivot-policy-floor/SOURCES.json | 18 ++ research/bit-pivot-policy-floor/TASK.json | 71 +++++ research/bit-pivot-policy-floor/VERIFY.json | 32 +++ research/bit-pivot-policy-floor/verify.py | 256 +++++++++++++++++++ 5 files changed, 550 insertions(+) create mode 100644 research/bit-pivot-policy-floor/README.md create mode 100644 research/bit-pivot-policy-floor/SOURCES.json create mode 100644 research/bit-pivot-policy-floor/TASK.json create mode 100644 research/bit-pivot-policy-floor/VERIFY.json create mode 100644 research/bit-pivot-policy-floor/verify.py diff --git a/research/bit-pivot-policy-floor/README.md b/research/bit-pivot-policy-floor/README.md new file mode 100644 index 0000000000..04ea934ad9 --- /dev/null +++ b/research/bit-pivot-policy-floor/README.md @@ -0,0 +1,173 @@ +# A pivot-policy swap floor for the paid pivoted BIT fallback + +This contribution is a **scoped proof with a finite certificate**. It was +produced by Nick Petalas. No new kappa, supplier admission or complete +multiplication theorem is claimed. The selected frontier is unchanged. + +It answers open question 2 of the pivoted fallback in +[#4235](https://github.com/CrocSwap/integer-mult-bounds/pull/4235): can another +pivot policy reduce the paid swaps? That package proves at most `s <= 2r` +swaps for its first-unit rule, so at most `1+12r` children (`1+4r` when +`f = 1`), which is 505 at the retained `m = 64, r <= 42` boundary. + +## Result + +Fix the compiler family of #4235. At stage `k = 0..r-1` a policy may choose +**any** unit pivot in residual rows `k..m-1` and columns `0..m-1-k` of +`M = P C`. A paid head swap is charged if its row is not `k`, and a paid +tail swap if its column is not `m-1-k`. Ordered clearing ADDs follow. Let +`D_r = diag(0^(m-r), 1^r)` be the diagonal suffix projector. + +1. **Floor (proved).** Every pivot policy pays at least `2 min(r, m-r)` + swaps on `D_r`. +2. **Attainment (proved).** An explicit policy pays exactly that many. +3. **Consequence at m = 64 (proved).** For `r <= 32` the first-unit bound + `s <= 2r` is sharp for every policy. Over the retained ranks `r <= 42`, + the best policy's worst-case packet still needs at least + `1 + 6*64 = 385` children when `f >= 2` and `1 + 2*64 = 129` when + `f = 1`, against #4235's 505 and 169. A changed pivot policy can save at + most 120 (or 40) worst-case children at this boundary, and only in ranks + 33 to 42. +4. **Optimal policy on small censuses (finite certificate).** Over every + idempotent in 13 complete `(q, m, r)` domains, the exhaustive + optimal-policy worst case `s*(m, r)` equals the floor except at corank + one, where `s*(m, m-1) = 3` for `m = 4, 5, 6` over F3 and `m = 4` over F5. + The first-unit rule pays `2r` there (up to 10 at `m = 6`). So the floor + is not sharp above `m/2`, and a better rule does gain in that range. + +| q | m | r | idempotents | floor | optimal worst | first-unit worst | +|---|---|---|---:|---:|---:|---:| +| 3 | 2 | 1 | 12 | 2 | 2 | 2 | +| 3 | 3 | 1 | 117 | 2 | 2 | 2 | +| 3 | 3 | 2 | 117 | 2 | 2 | 4 | +| 3 | 4 | 1 | 1,080 | 2 | 2 | 2 | +| 3 | 4 | 2 | 10,530 | 4 | 4 | 4 | +| 3 | 4 | 3 | 1,080 | 2 | 3 | 6 | +| 3 | 5 | 1 | 9,801 | 2 | 2 | 2 | +| 3 | 5 | 4 | 9,801 | 2 | 3 | 8 | +| 3 | 6 | 5 | 88,452 | 2 | 3 | 10 | +| 5 | 2 | 1 | 30 | 2 | 2 | 2 | +| 5 | 3 | 1 | 775 | 2 | 2 | 2 | +| 5 | 3 | 2 | 775 | 2 | 2 | 4 | +| 5 | 4 | 3 | 19,500 | 2 | 3 | 6 | + +The opt-in `--extended` run adds `m = 5`, ranks 2 and 3 over F3 +(882,090 idempotents each); both have optimal worst case 4, equal to the floor. + +## Proof of the floor + +Write labels for the original rows and columns of `M = D_r C`. Its only +nonzero entries are `M[i][m-1-i] = 1` for `i >= m-r`. Rows `0..m-r-1` and +columns `r..m-1` are zero. + +*Zero labels stay zero in the residual.* A clearing row ADD adds a multiple +of the pivot row chosen to cancel the pivot column. A residual row that is +zero has a zero coefficient. Column clearing and column swaps act inside +each row. So a label whose original row is zero has zero residual at every +stage. Any other ordered ADD from an earlier pivot row also leaves the +residual unchanged, because after column clearing a pivot row is zero on +every later residual column. + +*Positions below `m-r` keep zero labels until their stage.* Claim: at the +start of stage `k`, every head position `p` with `k <= p < m-r` holds a zero +label. This holds at `k = 0`. Stage `k` swaps position `k` with the +position `i` of its pivot row. That row has a nonzero residual, so its label +is nonzero and `i` lies outside `[k, m-r)` by the claim. The swap moves the +zero label from `k` to `i >= m-r`, so the claim holds at `k+1`. ADDs do not +move labels. + +Hence at each stage `k < min(r, m-r)` the row at position `k` has zero +residual. The pivot cannot lie in it, so a head swap is paid. The tail side +is the same argument for columns: the tail position `m-1-k` holds a zero +column label iff `m-1-k >= r`, that is, `k < m-r`. Column swaps exchange +position `m-1-k` with an earlier position, so zero labels again move only out +of the way. That gives `min(r, m-r)` paid tail swaps, and the floor follows. +Units over `Z/q^w` are the nonzero residues, and `D_r` has 0/1 entries, so +the argument is the same over every odd prime-power ring. + +## Attaining policy + +If `r <= m/2`, every stage pays at most two swaps, so `2r` is attained. If +`r > m/2`, at stage `k` take the home pivot `(k, m-1-k)` when it is a unit. +This happens exactly for `m-r <= k < r`. For `k < m-r`, take row label +`r+k` with its column label `m-1-r-k`. Those labels lie outside every later +home position, `[m-r, r)` on both sides, and the zero labels they displace +move to positions `>= r` and `<= m-1-r`. So later home pivots stay in place +and the policy pays exactly `2(m-r)`. The verifier executes this policy +(written as label `max(r, m-r)+k`, which agrees when `r > m/2`) on all 63 +literal `m = 64` suffix fixtures and checks that it pays exactly the floor. +On the same fixtures it checks that the first-unit rule pays `2r`. + +## Boundary bill + +#4235 charges `2s` children of width `f` and `4s` half-width children +(`2s` width-one children when `f = 1`), plus one rank-`r` child. With +`s >= 2 min(r, 64-r)` on `D_r`, the worst packet over `r <= 42` under any +policy needs at least `max_r 1 + 12 min(r, 64-r) = 385` children (at +`r = 32`) for `f >= 2`, and 129 for `f = 1`. The upper bounds 505 and 169 +come from #4235. Whether the best policy reaches 385 depends on +`s*(64, r) <= 64` for `33 <= r <= 42`, which is open; corank one shows the +floor `2(64-r)` itself can be exceeded. + +## Evidence and reproduction + +`verify.py` is standalone. It enumerates every rank-`r` idempotent once, with +the image in reduced row echelon form and the kernel as a graph over a +coordinate complement, and checks each count against +`q^(r(m-r)) [m choose r]_q`. For each idempotent it computes the exact +optimal-policy swap count by memoized search over every unit pivot at every +stage, and the first-unit count. It checks `optimum <= first-unit <= 2r`, +that the suffix optimum equals the floor, and that each domain's worst +optimum lies between the floor and `2r`. A control rejects a zero home pivot. + +From the repository root: + +```sh +/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 +``` + +Any CPython 3.12 works. Each registered command prints JSON with +`"status": "PASS_BIT_PIVOT_POLICY_FLOOR"` and the SHA256 of every package +file, and takes about 20 to 35 seconds. The opt-in `--extended` run takes +several minutes. `--receipt /absolute/new/path.json` writes the generated +report. + +## Scope and limitations + +The floor holds for the declared compiler family: stage-ordered pivots at +head `k` and tail `m-1-k`, paid swaps, ordered ADDs. A compiler with a +different normal form, pivot positions or swap pricing is outside it. The +floor is proved only for the projector `D_r`. The table's optimal worst +cases are finite facts about the listed fields and sizes, not a formula. +No caller is built, and preparation, routing and stock costs remain 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. Every residual block keeps corank `m-r`, which is a + natural first handle. +2. Find a polynomial-time rule that attains `s*`. The home-first greedy rule + is not optimal (it pays up to 10 at `m = 6, r = 5`, against an optimum + of 3). + +Structured questions are in [TASK.json](TASK.json). + +## Sources and credit + +Base: canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority +revision 7. [SOURCES.json](SOURCES.json) pins the selected record and task +catalogue as provenance. The compiler family, its swap pricing and the +residue-itinerary argument come from #4235 (head `27f1ce441`), which builds on +Cinna Davis's #4100 normal-form identity and its credited source527 and +commdata2338 normalizer lineage. That code is not merged, so this verifier +reimplements the stage process instead of importing it. The floor, the +attaining policy, the boundary consequence and the optimal-policy censuses +were produced by Nick Petalas. Independent human and formal proof-kernel +review are unclaimed. Apache-2.0. diff --git a/research/bit-pivot-policy-floor/SOURCES.json b/research/bit-pivot-policy-floor/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/bit-pivot-policy-floor/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/bit-pivot-policy-floor/TASK.json b/research/bit-pivot-policy-floor/TASK.json new file mode 100644 index 0000000000..f39be7a915 --- /dev/null +++ b/research/bit-pivot-policy-floor/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "For the paid pivoted BIT fallback compiler of PR4235, bound the paid pivot swaps achievable by any pivot policy: a policy-independent floor of 2 min(r, m-r) swaps on the diagonal suffix projector, its consequence at the m = 64, r <= 42 boundary, and exact optimal-policy worst cases over complete small idempotent censuses.", + "scope_change_reason": "The card's register-model question does not cover this; the assignment asks for original work and PR4235's open question 2 asks whether another pivot policy can reduce paid swaps.", + "bottleneck_link": "Side result for the BIT fallback bill: it caps how much any pivot-policy change can save at the retained boundary (at least 385 of 505 worst-case children remain) and shows the remaining gain lies only in ranks above m/2.", + "budget_minutes": 60, + "stop_rule": "Stop if the policy-independent floor fails on any census projector or if the explicit policy does not attain it at m = 64.", + "outcome": "completed", + "evidence": "Written scoped proof of the floor and its attainment; complete optimal-policy censuses of 142,070 idempotents over F3 and F5 (13 (q,m,r) domains), opt-in m = 5 ranks 2 and 3 over F3; literal m = 64 suffix fixtures for all 63 ranks under the explicit and first-unit policies; one zero-pivot control.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the optimal-policy worst case s*(m,r) for m/2 < r < m? Is s*(m, m-1) = 3 for every m >= 4?", + "why_it_matters": "If s*(64,r) <= 64 for 33 <= r <= 42, the best-policy boundary maximum is exactly 385 children rather than somewhere in [385, 505].", + "first_step": "Prove s* <= 2(m-r)+1 or s* <= 2(m-r)+2 using the constant corank m-r of every residual block; the censuses give s*(m,m-1) = 3 at m = 4, 5, 6.", + "blocked_by": "A proof; the census sizes grow too fast to reach m = 64." + }, + { + "question": "Does a polynomial-time pivot rule attain s* on every projector?", + "why_it_matters": "A caller needs a concrete rule; the census optimum uses exhaustive search, and the home-first greedy rule is not optimal (it pays up to 10 at m = 6, r = 5).", + "first_step": "Compare the census optimum with a rule that first fixes the selected row and column sets and then orders them by Laplace expansion.", + "blocked_by": "None for small m; the physical caller remains a separate obligation." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19081173" +} diff --git a/research/bit-pivot-policy-floor/VERIFY.json b/research/bit-pivot-policy-floor/VERIFY.json new file mode 100644 index 0000000000..c4e0fa3d12 --- /dev/null +++ b/research/bit-pivot-policy-floor/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Complete optimal-policy idempotent censuses, suffix-projector floor and attainment, literal m=64 fixtures for all ranks, boundary child bills and a zero-pivot control." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same checks with Python assertions disabled; every contract uses explicit exceptions." + } + ] +} diff --git a/research/bit-pivot-policy-floor/verify.py b/research/bit-pivot-policy-floor/verify.py new file mode 100644 index 0000000000..21906e2335 --- /dev/null +++ b/research/bit-pivot-policy-floor/verify.py @@ -0,0 +1,256 @@ +"""Pivot-policy swap floor for the paid pivoted BIT fallback. Apache-2.0. + +The compiler family is the one of PR4235: at stage k = 0..r-1 a unit pivot +is chosen anywhere in residual rows k..m-1 and columns 0..m-1-k of M = P C; +a paid head swap is charged when its row is not k and a paid tail swap when +its column is not m-1-k; ordered clearing ADDs follow. Over Z/q^w the +itinerary depends only on the residue field, so F_q censuses suffice. +""" + +import argparse +import hashlib +import itertools +import json +import sys +from functools import lru_cache +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def mul(a, b, q): + return [[sum(x * y for x, y in zip(row, col)) % q for col in zip(*b)] for row in a] + + +def inverse(a, q): + n = len(a) + rows = [list(row) + [int(i == j) for j in range(n)] for i, row in enumerate(a)] + for k in range(n): + i = next(i for i in range(k, n) if rows[i][k] % q) + rows[k], rows[i] = rows[i], rows[k] + scale = pow(rows[k][k], -1, q) + rows[k] = [x * scale % q for x in rows[k]] + for i in range(n): + if i != k and rows[i][k]: + c = rows[i][k] + rows[i] = [(x - c * y) % q for x, y in zip(rows[i], rows[k])] + return [row[n:] for row in rows] + + +def gaussian_binomial(m, r, q): + num = den = 1 + for i in range(r): + num *= q ** (m - i) - 1 + den *= q ** (i + 1) - 1 + return num // den + + +def idempotents(m, r, q): + """Every rank-r idempotent once: image in RREF, complement as a graph.""" + for piv in itertools.combinations(range(m), r): + free = [(i, j) for i in range(r) for j in range(m) if j > piv[i] and j not in piv] + comp = [j for j in range(m) if j not in piv] + for vals in itertools.product(range(q), repeat=len(free)): + basis = [[int(j == piv[i]) for j in range(m)] for i in range(r)] + for (i, j), v in zip(free, vals): + basis[i][j] = v + for graph in itertools.product(range(q), repeat=r * (m - r)): + kernel = [] + for t, c in enumerate(comp): + v = [int(j == c) for j in range(m)] + for i in range(r): + v = [(x + graph[t * r + i] * y) % q for x, y in zip(v, basis[i])] + kernel.append(v) + g = [list(col) for col in zip(*(basis + kernel))] + e = [[int(i == j and i < r) for j in range(m)] for i in range(m)] + yield mul(mul(g, e, q), inverse(g, q), q) + + +def stage(a, k, i, j, q): + """Swap pivot (i, j) to (k, last) and clear; returns the new residual.""" + m = len(a) + last = m - 1 - k + b = [list(row) for row in a] + b[k], b[i] = b[i], b[k] + for row in b: + row[last], row[j] = row[j], row[last] + inv = pow(b[k][last], -1, q) + for ii in range(k + 1, m): + c = b[ii][last] * inv % q + if c: + b[ii] = [(x - c * y) % q for x, y in zip(b[ii], b[k])] + for jj in range(last): + c = b[k][jj] * inv % q + if c: + for row in b: + row[jj] = (row[jj] - c * row[last]) % q + return tuple(map(tuple, b)) + + +def candidates(a, k, q): + m = len(a) + return [(i, j) for i in range(k, m) for j in range(m - k) if a[i][j] % q] + + +def optimum(p, r, q): + """Minimum paid swaps over every pivot policy (exact DFS with memo).""" + m = len(p) + + @lru_cache(None) + def go(k, a): + if k == r: + require(all(x == 0 for row in a[r:] for x in row[: m - r]), "zero remainder") + return 0 + best = None + cands = candidates(a, k, q) + require(cands, "split rank supplies a unit pivot") + for i, j in sorted(cands, key=lambda c: (c[0] != k) + (c[1] != m - 1 - k)): + cost = (i != k) + (j != m - 1 - k) + if best is not None and cost >= best: + continue + total = cost + go(k + 1, stage(a, k, i, j, q)) + if best is None or total < best: + best = total + return best + + return go(0, tuple(tuple(row[::-1]) for row in p)) + + +def run_policy(p, r, q, choose): + m = len(p) + a, paid = tuple(tuple(row[::-1]) for row in p), 0 + for k in range(r): + cands = candidates(a, k, q) + require(cands, "split rank supplies a unit pivot") + i, j = choose(a, k, cands) + paid += (i != k) + (j != m - 1 - k) + a = stage(a, k, i, j, q) + require(all(x == 0 for row in a[r:] for x in row[: m - r]), "zero remainder") + return paid + + +def first_unit(a, k, cands): + return cands[0] + + +def suffix_policy(r): + """Explicit attaining policy for the diagonal suffix projector.""" + def choose(a, k, cands): + m = len(a) + last = m - 1 - k + if (k, last) in cands: + return (k, last) + want = max(r, m - r) + k # nonzero, outside 0..r-1, still in place + pick = [c for c in cands if c[0] == want] + require(len(pick) == 1, "outside suffix row is untouched and monomial") + return pick[0] + return choose + + +def suffix(m, r): + return [[int(i == j and i >= m - r) for j in range(m)] for i in range(m)] + + +def floor(m, r): + return 2 * min(r, m - r) + + +CENSUS = [(3, 2, (1,)), (3, 3, (1, 2)), (3, 4, (1, 2, 3)), (3, 5, (1, 4)), + (3, 6, (5,)), (5, 2, (1,)), (5, 3, (1, 2)), (5, 4, (3,))] + + +EXTENDED = [(3, 5, (2, 3))] + + +def census(domains): + rows = [] + for q, m, ranks in domains: + for r in ranks: + hist, first_max, count = {}, 0, 0 + for p in idempotents(m, r, q): + count += 1 + s = optimum(p, r, q) + f = run_policy(p, r, q, first_unit) + require(s <= f <= 2 * r, "optimum <= first-unit <= 2r") + hist[s] = hist.get(s, 0) + 1 + first_max = max(first_max, f) + require(count == q ** (r * (m - r)) * gaussian_binomial(m, r, q), + f"complete idempotent census q={q} m={m} r={r}") + d = suffix(m, r) + require(optimum(d, r, q) == floor(m, r), "suffix optimum equals the floor") + worst = max(hist) + require(floor(m, r) <= worst <= 2 * r, "policy floor and ceiling") + rows.append({"q": q, "m": m, "r": r, "idempotents": count, + "optimal_histogram": {str(k): v for k, v in sorted(hist.items())}, + "optimal_worst": worst, "first_unit_worst": first_max, + "floor": floor(m, r)}) + return rows + + +def boundary(): + """Literal m = 64 suffix fixtures for every rank, and the child bills.""" + m, rows = 64, [] + for r in range(1, m): + d = suffix(m, r) + attained = run_policy(d, r, 3, suffix_policy(r)) + first = run_policy(d, r, 3, first_unit) + require(attained == floor(m, r), f"explicit policy attains the floor at r={r}") + require(first == 2 * r, f"first-unit policy pays 2r at r={r}") + rows.append((r, attained, first)) + ranks = range(1, 43) + best_f2 = max(1 + 6 * floor(m, r) for r in ranks) + old_f2 = max(1 + 12 * r for r in ranks) + best_f1 = max(1 + 2 * floor(m, r) for r in ranks) + old_f1 = max(1 + 4 * r for r in ranks) + require((best_f2, old_f2, best_f1, old_f1) == (385, 505, 129, 169), "boundary bills") + return {"m": 64, "ranks_checked": len(rows), + "first_unit_equals_2r": True, "explicit_policy_equals_floor": True, + "boundary_r_le_42_children_f_ge_2": {"every_policy_at_least": best_f2, + "pr4235_at_most": old_f2}, + "boundary_r_le_42_children_f_eq_1": {"every_policy_at_least": best_f1, + "pr4235_at_most": old_f1}} + + +def controls(): + """A policy that skips a required swap must be rejected.""" + m, r, q = 6, 2, 3 + a = tuple(tuple(row[::-1]) for row in suffix(m, r)) + require(not candidates(a, 0, q) or all(c != (0, m - 1) for c in candidates(a, 0, q)), + "home pivot is absent on the suffix projector") + try: + stage(a, 0, 0, m - 1, q) + except ValueError: + pass + else: + raise AssertionError("a zero pivot was accepted") + return {"zero_home_pivot_rejected": True} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--receipt", type=Path) + parser.add_argument("--extended", action="store_true", + help="also run the opt-in m=5 rank-2/3 census over F3 (minutes)") + args = parser.parse_args() + domains = CENSUS + (EXTENDED if args.extended else []) + report = {"status": "PASS_BIT_PIVOT_POLICY_FLOOR", + "files_sha256": {n: hashlib.sha256((HERE / n).read_bytes()).hexdigest() + for n in PACKAGE_FILES}, + "extended": args.extended, "census": census(domains), "boundary": boundary(), "controls": controls()} + text = json.dumps(report, indent=2, sort_keys=True) + if args.receipt: + require(args.receipt.is_absolute() and not args.receipt.exists(), + "receipt path is absolute and new") + args.receipt.write_text(text + "\n") + print(text) + return 0 + + +if __name__ == "__main__": + sys.exit(main())