diff --git a/research/selected-old-leaf-reserve/README.md b/research/selected-old-leaf-reserve/README.md new file mode 100644 index 0000000000..366a377aa1 --- /dev/null +++ b/research/selected-old-leaf-reserve/README.md @@ -0,0 +1,159 @@ +# The old-leaf reserve of the selected BIT stage is one + +**Source-bound audit with exact finite checks. No new κ.** +The selected conditional exponent stays 60403/20000000. + +## Result + +This concerns the one ordinary-BIT stage of the selected record #4470. Its +borrowed digits (DELAYED-COVER-BRIDGE §8) are + +```text +k ≤ D·(N²(w−1) + ceil(log_q(B·|GL_N(F_q)|))) + ceil(log_q S_old) + 1. +``` + +[PR #4954](https://github.com/CrocSwap/integer-mult-bounds/pull/4954) left +the old-leaf reserve `S_old` as its last non-numerical factor (open +question 1). This package derives it. + +1. **`S_old = 1`.** The external old-leaf factor is trivial, so the + old-leaf term contributes exactly one digit and `k = k_par + 1`. +2. **Conservative fallback.** Suppose one instead used the + multiplication-assembly route to supply the old supplier's rows. Then + `log2 S_old ≤ 252·ceil(log2 e')` at the largest old-supplier call width + `e' ≤ e`. At #4954's fit threshold this gives `k_old ≤ 103` digits. +3. **Consequences.** + - #4954's fit side, `log2 e ≥ 52182660963735`, now needs only the `B` + hypothesis `c_B ≤ N²`. The `S_old` hypothesis holds under either reading. + - `lockstep-live-role-audit` assumed `log2 A_old ≤ 64`. This becomes + `A_old = 0` (primary), or `log2 A_old ≤ 9` (fallback). + - `log2 C` is unchanged, because its complex row share dominates by more + than `10^13` bits. + +The six-bit window of #4954 remains. It depends only on `B` now. + +## Chain of custody + +Every step below is a verbatim phrase checked against a pinned source. + +1. **The stage's old saving.** `research/query-thinned-controllers/PROOF.md` + uses the "retained old ordinary saving a_old=0.0000384599". The bridge + reserves `W(w)^D * S_old` and exchanges high pieces "with the old + arbitrary-width supplier". +2. **Its call sites.** The pinned notes call the old supplier for: + - weighted leaves (`three-stage-cover-bit.tex`: four old atom interchanges); + - fixed cover routing (the same note, and bridge §6); + - peeled atoms and small stopped leaves (`stopped-product-interface.tex`, + with radix-q atoms padded to a binary power); + - the width-`k` high-part exchange and residual digits + (`three-stage-cover-rows.tex`). + + These are exactly the four uses PR185's reviewed proof enumerates. That + proof also notes that none of them depends on the numerical value + `384599/10^10`. +3. **Which supplier has saving 384599/10^10.** In + `certificates/copied-centers-network.json` the BIT saving is + `384599/10000000000`, with `W_b = 188181929 = 2N + B_a + B_b`, + `m_b = 575` and largest child 529. `notes/copied-centers-bit.tex` sets + `a_b = 384599/10^{10}`. It states that the complete-row mixed-width proof + in `notes/batched-bit-rows.tex` "therefore gives the all-width interchange + interface". +4. **That interface borrows its own rows.** The paragraph of + `notes/batched-bit-rows.tex` titled "Supplying the bit rows from existing + digits" works as follows: + - At width `e` it takes the least `ρ` with `q^{2ρ} ≥ W^{D(e)}`, so + `ρ = O(log e)`. + - It exchanges the high `ρ` digits of **its own two chunks** and gathers + them into a row field. + - It pads that field once, by a factor below two, and recurses at width + `e − ρ`. + - It removes the padding and undoes the gathering. + + In the note's words, "The row digits were already part of the two input + chunks". Smaller widths use individual-digit interchange. Every call + restores its row index. + +So each old-supplier call draws its rows from the two chunks it is handed, +which are body atoms or the high parts being exchanged. None of these is the +parent's borrowed range, and outer fields stay complete spectators. The +parent therefore needs no external row factor for its old leaves: +`S_old = 1`. This is the same contract PR185 states for its completed leaves +("no *external* extra stock"). Here it is traced to the actual 384599 +supplier, rather than assumed. + +**Why the fallback exists.** `notes/copied-centers-assembly.tex` reserves a +product `Q = W_c^{D_c(e)} W_b^{D_b(e)}` with `D_j(e) = t_j⌈log2 e⌉` and +`(t_b, w_b) = (9, 28)`, supplied "by the retained physically preceding +transformed prefix". This is the multiplication assembly's own row supply, +not a requirement of the interchange interface. If an auditor prefers that +route, the bit factor is `W_b^{9⌈log2 e'⌉} < 2^{252⌈log2 e'⌉}`. + +The verifier checks the ingredients of this fallback: +- `W_b` has 28 bits; +- `t_b = 9` is the least `t` with `575^t > 2·529^t`; +- the batched-bit-rows depth satisfies `D(e) ≤ 9⌈log2 e⌉` on all tested + widths. This bound is loose, for example `D(2^40) = 233 ≤ 360`. + +This coefficient 252 is also the "252 ordinary-leaf allocation" that +PR185 and the #1094 row bill carry as slack. + +## Consequences in numbers + +The cover prime satisfies `q > 2^26 N^5`, so `log2 q > 5·H1 + 26` with +`H1 = 25986965159937`, read from `query-thinned-controllers/RESULT.json`. + +- **Primary.** `k_old = ceil(log_q 1) + 1 = 1`. +- **Fallback.** At `t = log2 e = 52182660963735`, + `k_old ≤ ceil(252(t+1)/log2 q) + 1 = 103`, far below `e/4 = 2^{t−2}`. As + a #4954 envelope, `σ_old = 252/log2 q < 1`. +- **Lockstep.** `252⌈log2 e⌉ ≤ 504·log2 e ≤ 2^9 e^δ log2 e`, so + `log2 A_old ≤ 9 ≤ 64`. + +## Scope + +Card `selected-stock-envelope` (adversarial audit), scope **refined** to +#4954's open question 1 (see `TASK.json`). This package does not cover: + +- the compiled role count `B` or the six-bit window; +- the old supplier's own finite word or its fixed tapes. Its interface is + taken as the pinned notes state it; +- the outer constant `C`, the complex row stock, precision, or any supplier + replay. + +The conclusion is a source-bound reading of the retained contract. It is not +a new proof of that contract. + +Base: canonical main `b91956876e5b4122fd89179f1b57557ff8378f15`, priority +revision 7. The overlap search for `S_old` found only #4954's own posts. +Claim: [#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138075). + +## Reproduce + +```sh +python3.12 -B research/selected-old-leaf-reserve/verify.py +python3.12 -B scripts/research_package.py --package research/selected-old-leaf-reserve +``` + +It runs in under a second. Mutating `W_b`, the fallback digit count or the +batched-bit-rows phrase makes it fail. + +## Open next questions + +1. **Close #4954's six-bit window from `B`.** With `S_old = 1`, the least + fitting width depends only on `c_B = ceil(log_q B)`. *First step:* locate + the compiled role count of the query-thinned BIT producer and bound `c_B` + sharply against `N²`. *Blocked by:* the role count is not materialized in + the pinned sources. + +## Credit + +- JoyboyBrian, #4954, for the stage band and the open question. +- Mark (Matarener), `lockstep-live-role-audit`, for the `A_old` assumption. +- zxv, #4359/#4470, for the delayed-cover bridge and its stock formula. +- Cinna Davis and zxv, for the #4440/#4470 chain. +- The copied-centers, batched-bit-rows and three-stage-cover authors, as + credited in their notes. +- The PR182/PR185 completed-leaf lineage. + +Prepared by James Reed with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review is claimed. diff --git a/research/selected-old-leaf-reserve/SOURCES.json b/research/selected-old-leaf-reserve/SOURCES.json new file mode 100644 index 0000000000..bd7ad26604 --- /dev/null +++ b/research/selected-old-leaf-reserve/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/copied-centers-network.json", + "usage": "input", + "git_blob": "20bbb6806ce0611e481512894d1fd73d97c2970f", + "sha256": "7dbd675e42e22ac076280360f8750031851564bb7a56079e66236fee5d0a6cdf" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "input", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "usage": "input", + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef" + }, + { + "path": "notes/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + }, + { + "path": "notes/three-stage-cover-bit.tex", + "usage": "input", + "git_blob": "f05225d21f92cf8cef21b6e12601d5b4d61991f0", + "sha256": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511" + }, + { + "path": "notes/stopped-product-interface.tex", + "usage": "input", + "git_blob": "20c44ce4866fa972ce64365dcf365b1659a83050", + "sha256": "454a8f3924afc26e575b2a8cec6d0860397cb7f2dc431f3ba63fb8a7142cc96b" + }, + { + "path": "notes/copied-centers-bit.tex", + "usage": "input", + "git_blob": "1b7a2a88a49fb6d61238cde777051424d79b724d", + "sha256": "ccc8191ddb51698251ed4461a4c26104501b9b2ee37ce3cbe82fa73e85ae40dd" + }, + { + "path": "notes/batched-bit-rows.tex", + "usage": "input", + "git_blob": "cbaa8cb42cad1e714a1d24b16ab160ae6eaf60c9", + "sha256": "ef72c0ead19373cbc19c8a3aacb44dd0f75353ee5f4d055f775a986a4878022c" + }, + { + "path": "notes/copied-centers-assembly.tex", + "usage": "input", + "git_blob": "b0c69166c3048d27518355995e3e5b622722c696", + "sha256": "00117892971ae766188ace0af03030c44164fda105e42b70d84f52c3339a7dcb" + }, + { + "path": "research/community-round8-audit/pr185-proof-reviewed.md", + "usage": "input", + "git_blob": "93a588a73a38050dfa0a383cb44f228aff6f243e", + "sha256": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa" + }, + { + "path": "research/selected-bit-stage-stock-band/README.md", + "usage": "input", + "git_blob": "78f06e0376537a2a0a003d6e06bb5ac81e272a13", + "sha256": "b2bf296410af55bd83cfed8cdb385074737d511528985dbe1bc221ddf6da94c8" + }, + { + "path": "research/lockstep-live-role-audit/constant_c.py", + "usage": "input", + "git_blob": "a0fc4aecb910a353dd049926e25e13c20324112c", + "sha256": "74939dfa06092a6ea2cc7c94ce376f89d08c60c66af46ce5923341ed356ab51f" + } + ] +} diff --git a/research/selected-old-leaf-reserve/TASK.json b/research/selected-old-leaf-reserve/TASK.json new file mode 100644 index 0000000000..8d451bb18d --- /dev/null +++ b/research/selected-old-leaf-reserve/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md", + "research/stock-margin-chain/README.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Derive the old-leaf reserve S_old of the selected #4470 ordinary-BIT stage (DELAYED-COVER-BRIDGE section 8) from the retained supplier contract, and state its effect on PR #4954's fit side and on lockstep-live-role-audit's A_old assumption.", + "scope_change_reason": "PR #4954 (merged) left S_old as the last non-numerical factor of the selected stage's stock and asked for it as open question 1. This package traces a_old = 384599/10^10 to the copied-centers BIT supplier and its all-width interface, which borrows its own rows internally. It does not evaluate B, close the six-bit window, or replay any supplier.", + "bottleneck_link": "It removes one inherited hypothesis from the selected record's stock audit. The fit band, kappa and the selected frontier are unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop at the source-bound S_old derivation, its conservative fallback, and the two downstream consequences. Do not derive B or rerun constant C.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/selected-old-leaf-reserve", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", + "open_questions": [ + { + "question": "With S_old = 1, can the six-bit window of PR #4954 be closed by evaluating c_B = ceil(log_q B) from the compiled role count B of the selected stage?", + "why_it_matters": "S_old was one of the two factors that blocked the exact least fitting width. Only B remains.", + "first_step": "Locate the compiled role count B of the query-thinned BIT producer (its finite compiler realization) and bound ceil(log_q B) against N^2 sharply.", + "blocked_by": "The compiled role count is not materialized in the pinned sources; lockstep-live-role-audit gives only an upper bound." + } + ] +} diff --git a/research/selected-old-leaf-reserve/VERIFY.json b/research/selected-old-leaf-reserve/VERIFY.json new file mode 100644 index 0000000000..31660c73ee --- /dev/null +++ b/research/selected-old-leaf-reserve/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/copied-centers-network.json", + "research/query-thinned-controllers/PROOF.md", + "research/query-thinned-controllers/RESULT.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "notes/three-stage-cover-rows.tex", + "notes/three-stage-cover-bit.tex", + "notes/stopped-product-interface.tex", + "notes/copied-centers-bit.tex", + "notes/batched-bit-rows.tex", + "notes/copied-centers-assembly.tex", + "research/community-round8-audit/pr185-proof-reviewed.md", + "research/selected-bit-stage-stock-band/README.md", + "research/lockstep-live-role-audit/constant_c.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pins and verbatim phrases for the a_old chain of custody (query-thinned PROOF, delayed-cover bridge, three-stage-cover notes, copied-centers BIT and assembly notes, batched-bit-rows internal row supply, PR185). Copied-centers certificate: saving 384599/10^10, W_b=188181929 (28 bits), m_b=575, largest child 529; t_b=9 and coefficient 252; the batched-bit-rows depth bound D(e) <= 9 ceil(log2 e) on tested widths. Consequences: k_old = 1, fallback k_old = 103 at the fit threshold, fallback A_old <= 2^9." + } + ] +} diff --git a/research/selected-old-leaf-reserve/verify.py b/research/selected-old-leaf-reserve/verify.py new file mode 100644 index 0000000000..f0813f76b7 --- /dev/null +++ b/research/selected-old-leaf-reserve/verify.py @@ -0,0 +1,132 @@ +#!/usr/bin/env python3 +"""Source-bound derivation of the old-leaf reserve S_old of the selected BIT stage. + +Checks the chain of custody from the #4470 stage's a_old to the copied-centers +BIT supplier and its internal-borrowing all-width interface, then the exact +finite arithmetic of the conservative fallback bound and its consequences for +PR #4954 and lockstep-live-role-audit. No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import json +import sys +from fractions import Fraction +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "selected-old-leaf-reserve" + +# (path, phrase) pairs; each phrase must occur verbatim in the pinned source. +PHRASES = ( + ("research/query-thinned-controllers/PROOF.md", "a_old=0.0000384599, the ordinary saving is exactly"), + ("research/query-thinned-controllers/PROOF.md", "rank witnesses, exceeds 256/(C0-C1)*N^5 and pays the complete fallback."), + ("research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", "A safe reserve is `W(w)^D * S_old`, with"), + ("research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", "with the old arbitrary-width supplier. For clarity, the inherited ordinary"), + ("research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "\"borrowed_digits\": \"k <= D_N(ceil(e/w))*(N^2*(w-1)+ceil(log_q(B*|GL_N(F_q)|)))+ceil(log_q S_old)+1\""), + ("notes/three-stage-cover-rows.tex", "reserve. The old supplier has its retained complete-row contract and"), + ("notes/three-stage-cover-bit.tex", "Thus a weighted leaf uses four old ordinary atom interchanges, three"), + ("notes/stopped-product-interface.tex", "the next binary power and treated by that ordinary interface, with"), + ("notes/copied-centers-bit.tex", "Set $a_b=384599/10^{10}$ and $\\tau=1-a_b$."), + ("notes/copied-centers-bit.tex", "The complete-row mixed-width proof in \\path{notes/batched-bit-rows.tex}"), + ("notes/copied-centers-bit.tex", "therefore gives the all-width interchange interface, with bounded"), + ("notes/batched-bit-rows.tex", "\\paragraph{Supplying the bit rows from existing digits.}"), + ("notes/batched-bit-rows.tex", "The possibly large exponent in $W^{D(e)}=e^{O(1)}$ does not multiply the"), + ("notes/batched-bit-rows.tex", "logical volume by that polynomial. The row digits were already part of"), + ("notes/batched-bit-rows.tex", "Consequently the batched construction is an arbitrary-width interchange"), + ("notes/copied-centers-assembly.tex", " (t_b,w_b)=(9,28),\\qquad(t_c,w_c)=(20,30),"), + ("notes/copied-centers-assembly.tex", "The sufficient stock is therefore $p^{2000}$, supplied by the retained"), + ("research/community-round8-audit/pr185-proof-reviewed.md", + "None of these uses depends on the old numerical saving being `384599/10^10`."), + ("research/selected-bit-stage-stock-band/README.md", + "1. **Derive the old-leaf reserve `S_old` numerically from the retained"), + ("research/lockstep-live-role-audit/constant_c.py", " log2_A_old = 64"), +) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins_and_phrases() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + pinned = {row["path"] for row in sources["files"]} + for row in sources["files"]: + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], "pin " + row["path"]) + for path, phrase in PHRASES: + need(path in pinned, "unpinned phrase source " + path) + need(phrase in (ROOT / path).read_text(encoding="utf-8"), f"phrase in {path}: {phrase}") + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "60403/20000000", "selected kappa") + + +def certificate() -> dict: + sys.set_int_max_str_digits(0) + cert = json.loads((ROOT / "certificates/copied-centers-network.json").read_text(encoding="utf-8")) + bit = cert["bit"] + need(bit["saving"] == "384599/10000000000", "copied-centers BIT saving is a_old") + counts = bit["counts"] + if isinstance(counts, str): + import ast + counts = ast.literal_eval(counts) + need(counts["W"] == 188181929 and counts["m"] == 575 and counts["maxchild"] == 529, "W_b, m_b, largest child") + need(counts["W"] == 2 * counts["N"] + counts["B1"] + counts["B2"], "W_b = 2N + B_a + B_b") + return counts + + +def depth(e: int, m: int = 575, top: int = 529) -> int: + """batched-bit-rows D(e): replace e by top*floor(e/m) until below m.""" + d = 0 + while e >= m: + e = top * (e // m) + d += 1 + return d + + +def depth_and_coefficient(counts: dict) -> None: + w_b = counts["W"].bit_length() + need(w_b == 28, "wire bitlength of W_b is 28") + t_b = next(t for t in range(1, 100) if 575**t > 2 * 529**t) + need(t_b == 9, "least halving degree t_b = 9") + need(t_b * w_b == 252, "bit reserve coefficient 252") + # D(e) <= 9*ceil(log2 e): nine replacements at least halve e (575^9 > 2*529^9). + for e in list(range(1, 200001)) + [2**k + j for k in range(18, 64) for j in (-1, 0, 1)]: + need(depth(e) <= 9 * max(1, (e - 1).bit_length()), f"depth bound at e={e}") + + +def consequences() -> None: + result = json.loads((ROOT / "research/query-thinned-controllers/RESULT.json").read_text(encoding="utf-8")) + h1 = result["bit_strictification"]["uniform_H1"] + need(h1 == 25986965159937 and result["bit_strictification"]["uniform_N"] == "2^25986965159937", "selected stage rank") + log2_q_lower = 5 * h1 + 26 # cover prime q > 2^26 N^5 + # Primary: S_old = 1, so k_old = ceil(log_q 1) + 1 = 1 <= e/4 at every fitting width. + t_fit = 52182660963735 + need(1 <= 2 ** 10, "k_old = 1 is far below e/4") + # Fallback (assembly-level supply): log2 S_old <= 252*ceil(log2 e'), e' <= e. + # Then k_old <= ceil(252*(t+1)/log2 q) + 1, compared with e/4 = 2^(t-2). + k_old_fallback = -(-252 * (t_fit + 1) // log2_q_lower) + 1 + need(k_old_fallback == 103, "fallback k_old at the fit threshold") + need(k_old_fallback.bit_length() < t_fit - 2, "fallback k_old <= e/4") + # #4954 sufficient envelope: log_q S_old <= sigma*(1+log2 e) with sigma <= 2^(t-3)/(1+t). + sigma = Fraction(252, log2_q_lower) + need(sigma < 1, "fallback sigma is below one") + # lockstep-live-role-audit: log2 S_old <= A_old e^delta log2 e with log2 A_old <= 64. + # 252*ceil(log2 e) <= 504*log2 e <= 2^9 e^delta log2 e for e >= 2. + need(504 <= 2**9 and 9 <= 64, "fallback A_old <= 2^9") + + +def main() -> None: + pins_and_phrases() + counts = certificate() + depth_and_coefficient(counts) + consequences() + print("PASS_SELECTED_OLD_LEAF_RESERVE S_old=1_internal_borrowing " + "fallback_log2_S_old<=252*ceil(log2_e) fallback_k_old_at_fit=103 no_new_kappa") + + +if __name__ == "__main__": + main()