diff --git a/.github/workflows/fixed-prime-bootstrap.yml b/.github/workflows/fixed-prime-bootstrap.yml
new file mode 100644
index 0000000000..3709b9329c
--- /dev/null
+++ b/.github/workflows/fixed-prime-bootstrap.yml
@@ -0,0 +1,65 @@
+name: Fixed prime finite bootstrap
+on: [push, pull_request, workflow_dispatch]
+permissions:
+  contents: read
+jobs:
+  exact-replay:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    strategy:
+      matrix:
+        python: ['3.11', '3.13', '3.14']
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: af3fe331ca60c936229e060681ffccbc1c208678
+          path: .prerequisite
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: a8b0ce212bc9f09353a8161bf8a5cee9cefd600c
+          path: .banks
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: ${{ matrix.python }}
+      - run: python -m pip install -r research/fixed-prime-bootstrap/requirements.txt
+      - run: python -B research/fixed-prime-bootstrap/verify.py --parent-root .prerequisite --banks-root .banks
+      - run: make paired-cube-verify
+      - run: git diff --exit-code
+      - run: git -C .prerequisite diff --exit-code
+      - run: git -C .banks diff --exit-code
+  prime-kernel:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.12'
+      - name: Install the fixed Lean release in runner temporary storage
+        run: |
+          python -m pip install zstandard==0.25.0
+          curl -fsSL https://github.com/leanprover/lean4/releases/download/v4.24.0/lean-4.24.0-linux.tar.zst -o "$RUNNER_TEMP/lean.tar.zst"
+          python - <<'PY'
+          import hashlib,os,tarfile,zstandard
+          from pathlib import Path
+          root=Path(os.environ['RUNNER_TEMP'])
+          expected='b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec'
+          assert hashlib.sha256((root/'lean.tar.zst').read_bytes()).hexdigest()==expected
+          with (root/'lean.tar.zst').open('rb') as f:
+              with zstandard.ZstdDecompressor().stream_reader(f) as reader:
+                  with tarfile.open(fileobj=reader,mode='r|') as archive:
+                      archive.extractall(root,filter='data')
+          PY
+          echo "$RUNNER_TEMP/lean-4.24.0-linux/bin" >> "$GITHUB_PATH"
+      - name: Kernel-check the prime in a separate project copy
+        env:
+          MATHLIB_CACHE_DIR: ${{ runner.temp }}/mathlib-cache
+        run: |
+          cp -R research/fixed-prime-bootstrap "$RUNNER_TEMP/prime-proof"
+          cd "$RUNNER_TEMP/prime-proof"
+          lake update
+          lake exe cache get Mathlib.NumberTheory.LucasLehmer
+          lake env lean Prime.lean
diff --git a/research/fixed-prime-bootstrap/LICENSE b/research/fixed-prime-bootstrap/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/research/fixed-prime-bootstrap/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/research/fixed-prime-bootstrap/NOTICE.md b/research/fixed-prime-bootstrap/NOTICE.md
new file mode 100644
index 0000000000..06c535de6a
--- /dev/null
+++ b/research/fixed-prime-bootstrap/NOTICE.md
@@ -0,0 +1,13 @@
+# Attribution and assistance
+
+Apache-2.0. Original copied arithmetic headers and LICENSE are preserved.
+
+- Rohan Arun supplies PR237’s completed width-120 entrance banks at a8b0ce212bc9f09353a8161bf8a5cee9cefd600c, based on Evan McKinney’s PR197 bank endpoint construction. PR237’s original Anthropic Claude assistance disclosure is retained in the pinned prerequisite.
+- hcg890’s PR234 at af3fe331ca60c936229e060681ffccbc1c208678 supplies the immutable five-stage source-bound construction, finite admission bill, geometry and dependency closure. Its original notices and ChatGPT assistance disclosure remain in that prerequisite.
+- eumemic supplies the PR210 bit helper, frames, gauges, source borrowing and retiming. Jacob Sussman supplies the five-stage complex geometry and gcert/1 source export f010392c923279e3dd59ef3aa5fedad23affc5fd. Avi Eisenberg / ikeboy supplies the retained PR193 complex helper.
+- Rohan Arun's PR185 and later completed ordinary bootstrap arguments supply the finite recurrence. The prime-density bound and paid fallback are from the retained public bit/row/copied-center proofs; no priority is claimed for those lemmas.
+- The copied independent `base_two_moment.py` is maintainer arithmetic carried by PR230 at 1e7c15afb12b28321e12bf47b1180cba70f4a75b (SHA256 recorded in SOURCE.json), not a new implementation attributed to this author.
+- Mathlib's Lucas–Lehmer criterion and norm_num implementation credit Kim Morrison, Thomas Murrills and mathlib contributors; its pinned Apache-2.0 project is used without modification. Mersenne prime 2^127−1 is classical.
+- Other contributors and OpenAI retain the credits in the parent source notices. Attribution does not imply review or endorsement.
+
+Gabriele Nespoli's contribution, developed with OpenAI Codex, is the explicit fixed-prime density parameter, exact paid refinement, seven-level finite admission and reproducible certificate. AI assisted the research, code, proof exposition and validation. No human mathematical review is represented as completed.
diff --git a/research/fixed-prime-bootstrap/PROOF.md b/research/fixed-prime-bootstrap/PROOF.md
new file mode 100644
index 0000000000..d9144db977
--- /dev/null
+++ b/research/fixed-prime-bootstrap/PROOF.md
@@ -0,0 +1,100 @@
+# Fixed prime and seven completed ordinary suppliers
+
+This is a conditional refinement of Rohan Arun’s completed-bank PR237 at a7b0ce212bc9f09353a7161bf8a5cee9cefd600c, on hcg890’s PR234 at af3fe331ca60c936229e060681ffccbc1c208678. It inherits that construction's computational model and all-size interfaces, and changes two fixed parameters. It does not assert unconditional formal verification of integer multiplication.
+
+## A smaller positive rare-case bill
+
+Choose q = 2^127 − 1 = 170141183460469231731687303715884105727 **before** choosing any input or atom width. `Prime.lean` proves primality with mathlib's Lucas–Lehmer sufficiency theorem and a kernel-checked `norm_num` residue calculation; it also proves q > 2^80. The Python certificate independently records all 126 residues, beginning at 4 and ending at zero after 125 updates. This prime is classical; no discovery of a prime is claimed.
+
+PR234's immutable `proof/three-stage-cover-bit.tex`, subsection “Finite covers, batching, and the strict moment”, proves an upper bound 2m^3/q on bad low classes, separately for every edge type. Each cleared minor polynomial is nonzero after preservation of rank modulo q; the total degree is at most m^3. Conditioning on invertibility costs at most two. The condition remains valid for our fixed larger prime. Its freshly regenerated prime check excludes only 2,3,5,7 and verifies every remaining fixed factor is below 2^80. The route denominators are 1,2,3,6. Thus no consumed witness or rational denominator vanishes modulo q. No simultaneous union bound over edges is substituted for the separately averaged moments.
+
+For m=120, retain the sharper positive density
+
+    rho = 3456000 / 170141183460469231731687303715884105727.
+
+PR234 replaced this with the looser envelope 10^-16. Every rare class still executes the entire 32m^2 rank-one fallback. We add its full cost, without subtracting the displaced good case. With PR237’s unchanged freshly regenerated banked histogram H, W=261659, E=5916300 and rank mass 31346280, the normalized paid moment is
+
+    P(c) = sum_r [r H_r/(mW)] exp(c log(m/r))
+           + rho [32mE/W] exp(c log m).
+
+This is the original weighted moment with tau=1−c. All ranks satisfy 0<r<m, so P is strictly increasing. Rational Mercator logarithm and Taylor exponential enclosures inherited from the parent admit
+
+    c = 709084859748818674574370 / 10^27
+
+and exclude c+10^-27. A second independently implemented positive atanh logarithm and Taylor exponential enclosure checks both signs. Floating-point root finding is not used. Reinstating density 10^-16 at this c makes even the **lower** moment bound exceed one. The improvement consequently requires the proved rare-density change; it is not just printing more digits of the parent result.
+
+Both recurrence gaps are positive: delta_tau = 1−P_upper(c)>0 and delta_linear = 1−31346280/(120·261659)−rho·32·120·5916300/261659>0. The coefficient A=C(1+1/delta_linear+1/delta_tau) is finite. The banked maximum child ratio is 50/120<1/2, so its halving degree is one. No histogram multiplicative factor is introduced.
+
+## The large prime has large, fully paid constants
+
+The new prime makes the cover and all initialization/table costs enormous. Their size is a constant, not a missing term: q never grows with n,w or ancestors. The retained exact-tape contract permits C_primitive to depend on q, the fixed source recipe, the fixed bootstrap level and retained primitive implementations, but not on n,w,ancestor values, or spectator widths except through the logical volume V.
+
+PR234's regenerated finite ledger retains all scalar operations, all 120 rank-22 center-copy children, the single extra copied work stream, 24 temporary roles, generic wrappers, high affine factors, low transpositions, descriptor/matrix preparation, port routing and restoration. These original charges are paid twelve times for twelve data copies. The banked live denominator is W=261659; physical temporary stock is bounded separately by W+12·24=261947, never used to dilute the moment. Complete high fibers are batched and their cardinality cancels in normalized child volumes. They are not independent growing tapes or free row fields.
+
+In particular, writing d=14400, N=240, J=208670, W0=23683 and E0=495304, each original copy retains the parent's exact bound B_base(q):
+
+    B_base(q) <= [unit + J·16(d+1)^2 + J(W0+24)
+             + E0(8m^2+8) + E0·128N^3 +16m^3+120+E0+1] q^14400
+          = 1568901757016837 q^14400 < q^14401.
+
+PR237’s exact 231 address charts and proper 60-edge-colouring are recomputed from the pinned source. Twelve copies give 177179 full width-120 banks and 998580 incidences. The endpoint uses disjoint residual projectors and the retained PR197 completed-bank lemma. Source-owned gauges are still unbanked. All chart numerators and denominators are below 2^80<q, so their exact inverse and factor replay remain valid over this prime. The removed exterior rank mass is **225370**, calculated directly from 2200·100+18·60+48·65+13·90; PR237’s prose “226200” is a transcription error, while its executable profile correctly uses 31346280 and deficit 52800. We use the executable fresh count.
+
+PR237’s additional selector/routing bill K=12227329044<2^40 stays paid in the ordinary toll. To make the larger-prime overcharge explicit, we conservatively assign each selector an entire high-affine, stock, wrapper and matrix-preparation allowance, despite many of these not being required:
+
+    B_bank(q) <= [12·1568901757016837
+                  + 12·208670·(261659+12·24)
+                  + K(16(d+1)^2 + (261659+12·24)
+                       +128N^3+(8m^2+8)+1)] q^14400 < q^14401.
+
+The coefficient is freshly computed and is below 2^80<q. The extra middle term charges every original routing family against the entire enlarged bank role set, in addition to its original per-copy charge. This adds costs; it never reduces the existing inventory. All q-dependent preprocessing and tape scans remain in C_primitive(q,source,j)(1+B_bank(q)) times the logical-volume-normalized linear/ordinary-width toll. That constant is not assigned the numerical value one. The signed payload prefix upper bound 303094329841208644962256113408<2^98 also lies below q; choosing a larger prime introduces no tighter digit constraint. The separately paid row reserve is bounded by
+
+    log_q stock <= 4 ceil(log2(max(2,n))) (14400w+1) + log_q S_old_leaf.
+
+It is restored and reused. One outer padding factor is less than two, and conversion from binary input has volume factor below q^2, another fixed paid constant. Ordinary leaf algorithms may retain their own primes; complete restored interfaces, rather than a common prime, are required.
+
+## Seven finite levels, with no circular supplier
+
+Start with the parent's completed ordinary saving a0=384599/10^10. For j=1,...,7 define
+
+    a_j = (1−c)c + c a_(j−1) = c−c^j(c−a0).
+
+At level j every ordinary leaf uses only the already completed level j−1 algorithm; recursive coarse children have rank r<m. Seven is an input-independent fixed integer. Each level retains the weighted recurrence and its original coarse/ordinary decomposition:
+
+    T_j(e)/V = O(e^(1−c) + e^((1−c)^2+c(1−a_(j−1))) + e^c log e).
+
+The middle exponent is 1−a_j. The certificate verifies all four finite admission gaps:
+
+    atom: c−a_j;
+    borrowing: 1−a_j−c;
+    remainder: 1−a_j−c(1−a_(j−1));
+    stock: 1−c.
+
+They are strictly positive, including at level seven. The parent finite-cutoff argument therefore applies anew at every level. For each quantified actual constant C>=1 and the smallest gap delta, take
+
+    L = ceil(max(1,36/delta^2,2(4+ceil(log2 C))/delta)), e0=2^L.
+
+Then C(1+log2 e)e^(−delta)<=1/16 beyond e0; below it use the previously completed algorithm. The next finite constant can be C_large+C_old·2^(L(a_j−a_(j−1))). It may be immense but is finite and independent of input width. Certificate cutoffs at C=1 are arithmetic illustrations, not asserted bounds on actual primitive constants. No new external row field is added by nested complete calls; they restore their supplied chunks and treat other outer fields as spectators. The unattained limit a=c is used only for a monotone upper bound on this parameter family, never as a completed ordinary supplier.
+
+## Unchanged complex bridge and exact outer reduction
+
+Retain complex saving b=747454944651775/10^18, the parent's finite bridge, eta=10^-12 and beta=10^-9. The complex cap remains inactive: a7<(1−beta)b. For z=a7(1−2eta), the active outer margin is g(a7)=(1−eta)z/(1+z). The unchanged assembly checks all 47 strict constraints and seven margins. On the 10^-24 grid it admits
+
+    kappa = 354291207342277673841 / 500000000000000000000000
+          = 7.08582414684555347682 × 10^-4.
+
+The next grid point fails. Seven levels improve on six by exactly 85·10^-24 and attain the grid floor of the monotone family upper bound, even if the coarse moment is replaced by its adjacent excluded endpoint. This is only a certificate of this fixed parameter family and grid, not global optimality.
+
+The gain over PR237's published 177145602695277/250000000000000000 is exactly
+
+    1951723673841 / 500000000000000000000000
+    = 3.903447347682 × 10^-12.
+
+The certificate also compares against the banked parent's unrounded three-level outer bound and a matched 10^-24-grid comparator. Thus the claimed improvement exceeds a reporting/rounding change.
+
+## Verification scope and dependencies
+
+The verifier first checks the exact parent commit and every immutable package byte, then executes all six parent stages afresh: bit physical/geometry, all-column F2 word and inverse, all-used determinant witnesses, complex label/scalar/splice/guard, exact mathematics and finite accounting. It then regenerates PR237’s charts, inverse factor replays, completed banks, colouring, profile, selector bill and original arithmetic, and compares the entire bank certificate to the pinned publication. It consumes those fresh outputs and independently computes this refinement. Saved execution receipts are not inputs. Source drift, missing parent stages, cyclic suppliers, a coarse ordinary oracle, corrupted prime residues, the old rare density and adjacent coarse/kappa points are rejected.
+
+The pinned complex scalar identities hAi,hBi,hx,hy,hid, Lab.inv and five-window NetCert proof sources remain inherited; this package does not rebuild their entire Lean chain or claim a fresh all-column complex scalar proof. The same weighted q-local compiler, complete-stream tape movement, unit-pivot fallback, prime supply, Clifford synthesis, common precision, restored-row, recovery and all-size reduction interfaces remain hypotheses. The new Lean result certifies only the fixed prime and its size. The conditional theorem is T(n)=O(n(log n)^(1−kappa)) in the retained model under those interfaces.
+
+Developed with OpenAI Codex. Original construction and bootstrap attribution are preserved in NOTICE.md.
diff --git a/research/fixed-prime-bootstrap/Prime.lean b/research/fixed-prime-bootstrap/Prime.lean
new file mode 100644
index 0000000000..4c323ab609
--- /dev/null
+++ b/research/fixed-prime-bootstrap/Prime.lean
@@ -0,0 +1,22 @@
+/- Copyright 2026 Gabriele Nespoli. Apache-2.0. Developed with OpenAI Codex.
+   Lucas-Lehmer criterion and norm_num extension: mathlib contributors.
+   This verifies prime eligibility only, not the integer multiplication theorem. -/
+import Mathlib.NumberTheory.LucasLehmer
+
+theorem fixed_prime_prime : (mersenne 127).Prime :=
+  lucas_lehmer_sufficiency _ (by simp) (by norm_num)
+
+theorem fixed_prime_value : mersenne 127 = 170141183460469231731687303715884105727 := by
+  norm_num [mersenne]
+
+theorem fixed_prime_large : 2 ^ 80 < mersenne 127 := by
+  norm_num [mersenne]
+
+theorem fixed_prime_density :
+    (0 : ℚ) < 3456000 / 170141183460469231731687303715884105727 ∧
+    (3456000 / 170141183460469231731687303715884105727 : ℚ) < 1 / 10 ^ 16 := by
+  norm_num
+
+#print axioms fixed_prime_prime
+#print axioms fixed_prime_large
+#print axioms fixed_prime_density
diff --git a/research/fixed-prime-bootstrap/README.md b/research/fixed-prime-bootstrap/README.md
new file mode 100644
index 0000000000..26bb8e75ef
--- /dev/null
+++ b/research/fixed-prime-bootstrap/README.md
@@ -0,0 +1,33 @@
+# Fixed-prime refinement of the five-stage construction
+
+Conditional κ = **354291207342277673841 / 500000000000000000000000 = 7.08582414684555347682 × 10^-4**.
+
+This exceeds PR237's 7.08582410781108 × 10^-4 using its unchanged five-stage geometry and paid finite interfaces. Choose the fixed prime 2^127−1, use the proved rare-class density 2m^3/q in place of 10^-16 while paying the entire fallback, and complete seven finite ordinary bootstrap levels. All prime-dependent costs remain finite paid constants. See [PROOF.md](PROOF.md) for the argument and inherited hypotheses. This is not an unconditional Lean proof of integer multiplication.
+
+Reproduce with Python 3.11 or later:
+
+```sh
+git clone https://github.com/CrocSwap/integer-mult-bounds.git /tmp/five-stage-parent
+git -C /tmp/five-stage-parent fetch origin af3fe331ca60c936229e060681ffccbc1c208678
+git -C /tmp/five-stage-parent checkout --detach af3fe331ca60c936229e060681ffccbc1c208678
+git clone https://github.com/CrocSwap/integer-mult-bounds.git /tmp/five-stage-banks
+git -C /tmp/five-stage-banks fetch origin a8b0ce212bc9f09353a8161bf8a5cee9cefd600c
+git -C /tmp/five-stage-banks checkout --detach a8b0ce212bc9f09353a8161bf8a5cee9cefd600c
+python -m pip install -r research/fixed-prime-bootstrap/requirements.txt
+python -B research/fixed-prime-bootstrap/verify.py --parent-root /tmp/five-stage-parent --banks-root /tmp/five-stage-banks
+make paired-cube-verify
+```
+
+The verifier replays all parent stages, checks immutable source pins, verifies two independent rational moment enclosures, records the positive rare density and all fallback children, checks seven acyclic levels and their cutoff gaps, checks all 47 outer constraints, and reproduces `certificate.json`. No historical receipt or numerical experiment is used as proof. Use `--write` only when authoring a new certificate before freezing `SOURCE.json`.
+
+Separately kernel-check prime eligibility with the pinned Lean 4.24.0/mathlib project:
+
+```sh
+cp -R research/fixed-prime-bootstrap /tmp/fixed-prime-lean
+cd /tmp/fixed-prime-lean
+lake update
+lake exe cache get Mathlib.NumberTheory.LucasLehmer
+lake env lean Prime.lean
+```
+
+`#print axioms` discloses dependencies. No `native_decide` or `sorry` is used. Generated `.lake/` and `lake-manifest.json` are excluded from the immutable research package; perform Lean replay in a separate copied package directory so the Python source guard remains strict. CI does this explicitly.
diff --git a/research/fixed-prime-bootstrap/SOURCE.json b/research/fixed-prime-bootstrap/SOURCE.json
new file mode 100644
index 0000000000..2d916bffcd
--- /dev/null
+++ b/research/fixed-prime-bootstrap/SOURCE.json
@@ -0,0 +1,17 @@
+{
+  "files": {
+    "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+    "NOTICE.md": "3d3accb02ba25c79016156569ed82048d2ad4e936ba9b35eaf69a24a2e5f264f",
+    "PROOF.md": "4bc82268e150a0bf815b7064e2913e2d918e957be0e958f5387f5582f7364fd5",
+    "Prime.lean": "9daf5f5c7fea3230bfa2f7496eabcb7c2c433b5b45ec702a6baad322933a6417",
+    "README.md": "3d2724ae1f047346f68cf2e98d7442541e6e76acf23785e9234aeed64a5d6cc6",
+    "base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098",
+    "certificate.json": "91ed664f43e6f9d79744111be510126c9efe852cd45d68d17b5ab3d44e2caa31",
+    "lakefile.toml": "7cc6fa1e76b099cad51cca126c1827e6bee1175c52733e6bf9db0d5548249da0",
+    "lean-toolchain": "42779d67b81608af8a12aa4328d2ab47ca201925b3b2bd68369587b5340bb434",
+    "prerequisite.json": "fca8a3e15ddb8f45010dfccbc271a9e47e458bbae50dcacddd51011825a0a847",
+    "requirements.txt": "25f9f1fb1988b230147a1d3092d34e09c069eb7a6c6d6df46b3973b9f2d36efc",
+    "verify.py": "43a1f0df2ed27c98677c66a989972d6a2547340d48e22df79d00329ff865576d"
+  },
+  "schema": "fixed-prime-bootstrap-source/1"
+}
diff --git a/research/fixed-prime-bootstrap/base_two_moment.py b/research/fixed-prime-bootstrap/base_two_moment.py
new file mode 100644
index 0000000000..14a90fa0e7
--- /dev/null
+++ b/research/fixed-prime-bootstrap/base_two_moment.py
@@ -0,0 +1,63 @@
+#!/usr/bin/env python3
+"""Maintainer arithmetic cross-check of the pinned PR39 certificate.
+
+Uses no producer/checker imports. Counts are inputs, not proved by this script.
+80-term rational logarithms and 12-term exponentials independently enclose
+the two moments. The accompanying written review addresses their realization.
+"""
+import argparse
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+GRID = 10**30
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def log_unit(x):
+    require(1 <= x <= 2, "logarithm range")
+    z = (x-1)/(x+1)
+    lo = 2*sum((z**(2*j+1)/(2*j+1) for j in range(80)), Q(0))
+    return lo, lo+2*z**161/(161*(1-z*z))
+
+
+def log_bounds(x):
+    k = 0
+    while x > 2:
+        x /= 2
+        k += 1
+    lo, hi = log_unit(x)
+    l2, u2 = log_unit(Q(2))
+    lo, hi = lo+k*l2, hi+k*u2
+    # Outward rational rounding keeps later certificates compact.
+    return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID)
+
+
+def exp_bounds(x):
+    require(0 <= x < 1, "exponential range")
+    term = total = Q(1)
+    for j in range(1, 13):
+        term *= x/j
+        total += term
+    tail = term*x/13/(1-x/14)
+    return total, total+tail
+
+
+def moment(m, W, entries, saving):
+    lo = hi = Q(0)
+    for t, count in entries:
+        t, count = int(t), int(count)
+        require(0 < t < m and count > 0, "improper child")
+        l, u = log_bounds(Q(m, t))
+        lower = exp_bounds(saving*l)[0]
+        upper = exp_bounds(saving*u)[1]
+        lo += Q(t*count, m*W)*lower
+        hi += Q(t*count, m*W)*upper
+    return Q((lo*GRID).__floor__(), GRID), Q((hi*GRID).__ceil__(), GRID)
+
diff --git a/research/fixed-prime-bootstrap/certificate.json b/research/fixed-prime-bootstrap/certificate.json
new file mode 100644
index 0000000000..d2a5c16594
--- /dev/null
+++ b/research/fixed-prime-bootstrap/certificate.json
@@ -0,0 +1,553 @@
+{
+  "assembly": {
+    "absorption_gap": "78702094269384270308790366151068968607650994515619187327981512808849591379348638823851123396490629479188583069960976441883107869506581032995114147436400617100912972808496405267037727001152256992119888665649502545338603/192444054780720653943241309983981116294218571367118625105466037626107714007534699307026890928086945905883789400239697540994315254391611992684917090218768358602269029662830428152287672554742375276911211313465696472771058500000000000000000000000",
+    "margins": {
+      "Gaussian_arithmetic": "436359913921204508810750640853089521531466142191163194757083153333752748858822354470981571264173116971952188955264552381329418971169746082951464714688913346823358203852832027994891318871025541006391452536406290240455807054457883/615820975298306092618372191948739572141499428374779600337491320403544684824111037782486050969878226898828126080767032131181808814053158376591734688700058747527260894921057370087320552175175600886115876203090228712867387200000000000",
+      "balanced_prefix": "272724946441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "bulk_exposure": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "compact_phase_layer": "272724946056419776921178660075749968469180501648813068197838002004495939817183186038712457559838029911404908667627503188151113701235354861050956452166883024100522608456318245249684253180175208712937876377570522915185607054457883/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117000000000000",
+      "coordinate_movement": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "dimension": "384615384615000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "scalar_work": "2181799571145574982299518435811378087529179641309564544722364767512492045302973484415185450777080712284456512023393077108564675183803252449890219514923903455866937888082312377277100019573429085469896264897321141710004607054457883/3079104876491530463091860959743697860707497141873898001687456602017723424120555188912430254849391134494140630403835160655909044070265791882958673443500293737636304474605286850436602760875878004430579381015451143564336936000000000000"
+    },
+    "minimum_margin": "272724946056419776921178660075749968469180501648813068197838002004495939817183186038712457559838029911404908667627503188151113701235354861050956452166883024100522608456318245249684253180175208712937876377570522915185607054457883/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117000000000000",
+    "parameters": {
+      "C0": {
+        "base": 2,
+        "exponent": 210000
+      },
+      "C1": 1,
+      "a_bit": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "a_complex": "29898197786071/40000000000000000",
+      "alpha_squared_power": "545449892497727663403798628037982556906323235886063279129913254219923954886581800092494313733729841678983709147022585176781622484459340230885136889703600228638581934117174549825029362664925762535360503308963468457302607054457883/769776219122882615772965239935924465176874285468474500421864150504430856030138797228107563712347783623535157600958790163977261017566447970739668360875073434409076118651321712609150690218969501107644845253862785891084234000000000000",
+      "beta": "1/1000000000",
+      "c": "3545424299987002524274059583509023649682855545084252742116978278800564195902181982699164130260593552978524406232136065852196614181911809807844345687977323658994771233591131959479486423301757199691494150108108292047521/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "delta": "1/8000000000000",
+      "epsilon": "384615384615000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "eta": "1/1000000000000",
+      "kappa": "354291207342277673841/500000000000000000000000",
+      "lambda_": "9992909151402518904102854392646236209605093779376341047785608894043454323352840145809699156395063609535093599593711872116295494788000471763188676075770038393524926488967185578601442580574518329734612651873652391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "lambda_prime": "4996454575701262997475725940416490976350317144454915747257883021721199435804097818017300835869739406447021475593767863934147803385818088190192155654312022676341005228766408868040520513576698242800308505849891891707952479/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "q": "3545424298737002524274059583509023649682855545084252742116978278800564195902181982699164130260593552978524406232136065852196614181911809807844345687977323658994771233591131959479486423301757199691494150108108292047521/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "sigma": "39970101802213929/40000000000000000",
+      "tau": "9992909151402511813254256904459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    "recurrence": {
+      "internal": "9992909151402511813254256904459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "leaf": "39970101802243827197786071/40000000000000000000000000",
+      "reservations": "4996454575700012997475725940416490976350317144454915747257883021721199435804097818017300835869739406447021475593767863934147803385818088190192155654312022676341005228766408868040520513576698242800308505849891891707952479/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    "strict_constraints": {
+      "Gaussian_arithmetic_above_kappa": "72166520542848947322984875514301708976483033231277135409065383297118374265634361831514432736856455838102911654569075160942829196838737605126350489865033248623287286740662323529916373613295428455842856499541756065954796440045338603/192444054780720653943241309983981116294218571367118625105466037626107714007534699307026890928086945905883789400239697540994315254391611992684917090218768358602269029662830428152287672554742375276911211313465696472771058500000000000000000000000",
+      "K_dominates_log": "272724946152573623074928660075749968469180501648813068197838002004495939817183186038712457559838029911404908667627503188151113701235354861050956452166883024100522608456318245249684253180175208712937876377570522915185607054457883/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117000000000000",
+      "K_geometry": "288734263407691307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117000000000000",
+      "alpha_below_one": "769230769230384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/769776219122882615772965239935924465176874285468474500421864150504430856030138797228107563712347783623535157600958790163977261017566447970739668360875073434409076118651321712609150690218969501107644845253862785891084234000000000000",
+      "alpha_below_one_fourth": "191898604888222926279837511355943133737312248131232561826336124371887790052648117506934396614353216064204805691092674955817533631907152652454031953329064758373630447728713253602462643192077449514375850810156733004313755892945542117/769776219122882615772965239935924465176874285468474500421864150504430856030138797228107563712347783623535157600958790163977261017566447970739668360875073434409076118651321712609150690218969501107644845253862785891084234000000000000",
+      "alpha_positive": "545449892497727663403798628037982556906323235886063279129913254219923954886581800092494313733729841678983709147022585176781622484459340230885136889703600228638581934117174549825029362664925762535360503308963468457302607054457883/769776219122882615772965239935924465176874285468474500421864150504430856030138797228107563712347783623535157600958790163977261017566447970739668360875073434409076118651321712609150690218969501107644845253862785891084234000000000000",
+      "artificial_boundary": "21555915935013398369063572001873242333519881021688949324927855527892420189190198157583487246990971237298693564906116587983673790747372300955195737219958459403631748406993908417670799069575937761479963502375270615782576282178836626351/3079104876491530463091860959743697860707497141873898001687456602017723424120555188912430254849391134494140630403835160655909044070265791882958673443500293737636304474605286850436602760875878004430579381015451143564336936000000000000",
+      "balanced_prefix_above_kappa": "192444054780799356037510694254289906660369640335726276099981656813435695520343548898406239566910797029280280029718886124064276230833495100554423671251763472749705430279931341125096168960009413003912363570457816361436708002545338603/192444054780720653943241309983981116294218571367118625105466037626107714007534699307026890928086945905883789400239697540994315254391611992684917090218768358602269029662830428152287672554742375276911211313465696472771058500000000000000000000000",
+      "beta_below_one": "999999999/1000000000",
+      "beta_positive": "1/1000000000",
+      "bit_positive": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "bulk_exposure_above_kappa": "5024450642633268923095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "c_below_one": "4996454575700012997475725940416490976350317144454915747257883021721199435804097818017300835869739406447021475593767863934147803385818088190192155654312022676341005228766408868040520513576698242800308505849891891707952479/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "c_positive": "3545424299987002524274059583509023649682855545084252742116978278800564195902181982699164130260593552978524406232136065852196614181911809807844345687977323658994771233591131959479486423301757199691494150108108292047521/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cell_above_band": "769230769229615111890438558692113517380032037767411562857265762749789067924747784571984930601385946218143826108188232421199520604918011369491216776014630165819562463282795461940674339143695424654890515249446177577373068607054457883/1539552438245765231545930479871848930353748570936949000843728301008861712060277594456215127424695567247070315201917580327954522035132895941479336721750146868818152237302643425218301380437939002215289690507725571782168468000000000000",
+      "compact_leaf": "191850420784597752467065416490976350317144454915747257883021721199435804097818017300835869739406447021475593767863934147803385818088190192155654312022676341005228766408868040520513576698242800308505849891891707952479/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "compact_phase_layer_above_kappa": "78702094269384270308790366151068968607650994515619187327981512808849591379348638823851123396490629479188583069960976441883107869506581032995114147436400617100912972808496405267037727001152256992119888665649502545338603/192444054780720653943241309983981116294218571367118625105466037626107714007534699307026890928086945905883789400239697540994315254391611992684917090218768358602269029662830428152287672554742375276911211313465696472771058500000000000000000000000",
+      "compact_reservations": "1/4000000000000",
+      "complex_above_bit": "383700849029563254256904459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "complex_below_one_over32": "1220101802213929/40000000000000000",
+      "coordinate_movement_above_kappa": "5024450642633268923095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "delta_below_one_eighth": "999999999999/8000000000000",
+      "delta_positive": "1/8000000000000",
+      "dimension_above_kappa": "192171329834471790111539489372056394400035718539541744534869688649992267649278736388493452620811460333683121396789582739035403631732452283545916404881786065068982733809919277277992258786382720892048798099538215890799399316361436708002545338603/192444054780720653943241309983981116294218571367118625105466037626107714007534699307026890928086945905883789400239697540994315254391611992684917090218768358602269029662830428152287672554742375276911211313465696472771058500000000000000000000000",
+      "epsilon_below_one": "272724946441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "epsilon_positive": "384615384615000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "gamma_sublinear": "1/2000000000000",
+      "guard_width": "272724946441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "lambda_above_internal": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "lambda_above_sigma": "383700849036654102854392646236209605093779376341047785608894043454323352840145809699156395063609535093599593711872116295494788000471763188676075770038393524926488967185578601442580574518329734612651873652391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "lambda_above_tau": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "lambda_prime_above_lambda": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "lambda_prime_below_one": "3545424298737002524274059583509023649682855545084252742116978278800564195902181982699164130260593552978524406232136065852196614181911809807844345687977323658994771233591131959479486423301757199691494150108108292047521/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "leaf_saving_above_bit": "383700841555013807739154459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "literal_scalar_guard": "1",
+      "phase_boundary": "436359913921204508810750640853089521531466142191163194757083153333752748858822354470981571264173116971952188955264552381329418971169746082951464714688913346823358203852832027994891318871025541006391452536406290240455807054457883/615820975298306092618372191948739572141499428374779600337491320403544684824111037782486050969878226898828126080767032131181808814053158376591734688700058747527260894921057370087320552175175600886115876203090228712867387200000000000",
+      "phase_local": "2181799571145574982299518435811378087529179641309564544722364767512492045302973484415185450777080712284456512023393077108564675183803252449890219514923903455866937888082312377277100019573429085469896264897321141710004607054457883/3079104876491530463091860959743697860707497141873898001687456602017723424120555188912430254849391134494140630403835160655909044070265791882958673443500293737636304474605286850436602760875878004430579381015451143564336936000000000000",
+      "prime_interval_packing": "272724946441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "q_below_internal": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "q_below_leaf": "191850420784597752467065416490976350317144454915747257883021721199435804097818017300835869739406447021475593767863934147803385818088190192155654312022676341005228766408868040520513576698242800308505849891891707952479/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "q_below_reservations": "1/4000000000000",
+      "q_positive": "3545424298737002524274059583509023649682855545084252742116978278800564195902181982699164130260593552978524406232136065852196614181911809807844345687977323658994771233591131959479486423301757199691494150108108292047521/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "record_suffix": "272724946441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117",
+      "row_product_gap": "23971789/25",
+      "scalar_work_above_kappa": "168388547933209274294605530506292267123592318914836447961798402110172231269401711485027878200899928791044806354688923931439986824034543601468809034974417427924421801572077537606060209890666616094298462156274604302340325690045338603/192444054780720653943241309983981116294218571367118625105466037626107714007534699307026890928086945905883789400239697540994315254391611992684917090218768358602269029662830428152287672554742375276911211313465696472771058500000000000000000000000",
+      "short_record_fallback": "3843424662838126374342993277631519394264601564575517373552070550555158323987979594316258771916953065696464840989732130062525530647193293306388700496854663816767788973041415979431776005839629749746315168171081419095584847135979916274335249597566058169424166998851512201598149985705758930806192656998982968650465316529628186230781564911866381597131383296227442482069743310939536409510011633970812412629319721928834985599270941957/3848881095614413078864826199679622325884371427342372502109320752522154280150693986140537818561738918117675788004793950819886305087832239853698341804375367172045380593256608563045753451094847505538224226269313929455421170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "small_field_exposure": "1/1000000000000"
+    }
+  },
+  "bank_extra_selector_calls": 12227329044,
+  "bank_physical": {
+    "W": 261659,
+    "banks": 177179,
+    "chart_sha256": "339f8a0001bfeac857d426d49a26523edecf32442641e69819f9f4422b64e21c",
+    "color_stats": {
+      "longest_swapped_path": 1,
+      "swaps": 192
+    },
+    "colors": 60,
+    "conflicting_assignment_rejected": true,
+    "conservative_selector_calls": 12227329044,
+    "copies": 12,
+    "distinct_charts": 231,
+    "entrance_ranks": {
+      "12": 18,
+      "13": 48,
+      "18": 13,
+      "20": 2200
+    },
+    "full_chains": 14364,
+    "gauge_chains": 2279,
+    "incidence_sha256": "78b1e0600c7a2f144eb062ffa3f411770e4608d91082f79111cd99e2009747db",
+    "incidences": 998580,
+    "m": 120,
+    "max_chart_factors": 221,
+    "max_den": 36,
+    "max_num": 40,
+    "plan": {
+      "r11x8+r4x8": 360,
+      "r12x10": 108,
+      "r24x5": 172368,
+      "r4x30": 4304,
+      "r6x20": 39
+    },
+    "removed_exteriors": {
+      "100": 2200,
+      "60": 18,
+      "65": 48,
+      "90": 13
+    },
+    "residual_occurrences": {
+      "11": 2880,
+      "12": 1080,
+      "24": 861840,
+      "4": 132000,
+      "6": 780
+    },
+    "status": "PASS exact charts and width-120 bank incidence"
+  },
+  "banked_physical_stock_role_upper": 261947,
+  "banked_profile": {
+    "W": 261659,
+    "calls": 5916300,
+    "copies": 12,
+    "deficit": 52800,
+    "histogram": {
+      "1": 2525640,
+      "10": 46260,
+      "11": 27300,
+      "12": 90420,
+      "13": 34680,
+      "14": 65520,
+      "15": 17940,
+      "16": 60840,
+      "17": 29220,
+      "18": 28080,
+      "19": 23160,
+      "2": 1121040,
+      "20": 102960,
+      "21": 291240,
+      "22": 105180,
+      "23": 42240,
+      "3": 612540,
+      "4": 217260,
+      "46": 42240,
+      "5": 149040,
+      "50": 42240,
+      "6": 90960,
+      "7": 74640,
+      "8": 39060,
+      "9": 36600
+    },
+    "m": 120,
+    "maxchild": 50,
+    "rank_mass": 31346280
+  },
+  "beta": "1/1000000000",
+  "coarse": "70908485974881867457437/100000000000000000000000000",
+  "coarse_grid": 1000000000000000000000000000,
+  "complex_saving": "29898197786071/40000000000000000",
+  "controls": [
+    "cyclic supplier",
+    "unattained coarse ordinary leaf",
+    "corrupt Lucas-Lehmer residue",
+    "old-density paid moment at new coarse point",
+    "adjacent coarse and kappa grid points"
+  ],
+  "cutoff": {
+    "formula": "e0(C)=2^ceil(max(1,36/delta^2,2*(4+ceil(log2(C)))/delta))",
+    "inequality": "C*(1+log2(e))*e^(-delta)<=1/16 for e>=e0",
+    "next_constant": "C_large+C_old*2^(L*(a_next-a_old))",
+    "small_widths": "Use the previously completed ordinary supplier"
+  },
+  "delta_linear": "74862120722606461961942335119535054519880/44518971923082918705681568202994519220421093",
+  "delta_tau_lower": "12850708323992610540965622851070029443501/6739986666787659948666753771754907668409286105635143120275902562304",
+  "depth": 7,
+  "eta": "1/1000000000000",
+  "excluded_coarse": "709084859748818674574371/1000000000000000000000000000",
+  "fallback_histogram": [
+    [
+      1,
+      2726231040000
+    ]
+  ],
+  "gain": "1951723673841/500000000000000000000000",
+  "independent_accepted": [
+    "170141183460469231731687303391363208326239961074450651848391730185821/170141183460469231731687303715884105727000000000000000000000000000000",
+    "42535295865117307932921825847883337377425107576545584788026958004887/42535295865117307932921825928971026431750000000000000000000000000000"
+  ],
+  "independent_excluded": [
+    "170141183460469231731687303795278377861393917205476312311358031549719/170141183460469231731687303715884105727000000000000000000000000000000",
+    "85070591730234615865843651897724259522427193218603999807537066691723/85070591730234615865843651857942052863500000000000000000000000000000"
+  ],
+  "kappa": "354291207342277673841/500000000000000000000000",
+  "kappa_decimal": "0.000708582414684555347682",
+  "kappa_grid": 1000000000000000000000000,
+  "matched_gain": "1951723539821/500000000000000000000000",
+  "minimum_margin": "272724946056419776921178660075749968469180501648813068197838002004495939817183186038712457559838029911404908667627503188151113701235354861050956452166883024100522608456318245249684253180175208712937876377570522915185607054457883/384888109561441307886482619967962232588437142734237250210932075252215428015069398614053781856173891811767578800479395081988630508783223985369834180437536717204538059325660856304575345109484750553822422626931392945542117000000000000",
+  "ordinary_chain": [
+    "384599/10000000000",
+    "7086093297432911263155972653324440237600993391031/10000000000000000000000000000000000000000000000000000",
+    "709084522557691398717843852958398331592778818297134172805105447948690047547/1000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "70908485950972155138142320804785060871671556670654124219743708115018415959839675030845243059528757039/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "7090848597486491344243043833033502205365844612010370006375262252030065836672191158898650343010972823544595518166791367846649043/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "709084859748818554356016468928513448770473032160650086303146006184729245334408658478477677574465465438621569102790324365199126722095317386667270879282791/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "70908485974881867448912498564718627468925103051723087984766019806513753180933070829555824601339623411979110833823859799480639337831540807073732201473381426238376490300257279066667/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+  ],
+  "original_per_copy_paid_inventory": {
+    "W": 23683,
+    "bridge_additions": 10560,
+    "copy_children_already_paid": true,
+    "copy_erase_episodes": 120,
+    "fallback_children": 460800,
+    "generic_wrappers": 57062983232,
+    "high_affine_factors": 692413137674720,
+    "low_transposition_coefficient": 4946939690,
+    "m": 120,
+    "matrix_preparation_per_edge_per_low_class": 1769472000,
+    "payload_prefix_bits": 98,
+    "payload_prefix_upper": 303094329841208644962256113408,
+    "physical_stock_roles": 23707,
+    "positive_rank_children": 495304,
+    "rank_mass": 2837560,
+    "route_and_final_exchange_families": 208670,
+    "simultaneous_extra_work_streams": 1,
+    "terminal_exchange_stream_movements": 7040,
+    "unit_expanded_additions": 21787770,
+    "weighted_additions": 12858690
+  },
+  "paid_family_grid_cap_attained": true,
+  "parent_matched_kappa": "17714560269527706701/25000000000000000000000",
+  "parent_published_kappa": "177145602695277/250000000000000000",
+  "parent_unrounded_bound": "2479317677754218976434673007431036344157389915092993076420970368365616078186793395588085153/3498982814181253201790615926209221652270366611567363359687988333728053604411914847000000000000",
+  "prerequisite": {
+    "banks_commit": "a8b0ce212bc9f09353a8161bf8a5cee9cefd600c",
+    "banks_files": {
+      "NOTICE": "86fd7612f1acfd909d10e69cf0d28ea1627c6d4bafab093db1ea2f8c0c1ed208",
+      "PROOF.md": "29856b59ea866e8202b8e44f55eee2f97e41ae0a736b5dff862af96785ed0d58",
+      "README.md": "1ceba095158d0e73d33151567fd116f523a787c662edaedf35ff4980dbfce40f",
+      "SOURCE.json": "b6c0f2a75a40e85332e6aab895579fdf27ca182024a8d23b1d906095bbd6c50a",
+      "arithmetic5.py": "1f9e2043aadbbd74605296f74f5acdd3bdabe7482add56c0d16fba3e5d8ad206",
+      "banks.py": "0548a1c15bd6f6dea4505f5fd2ca1bb4ecbe914c8c90769b8cd8beeef428d0cf",
+      "certificate.json": "48bca1692c0eeb93c7080b4638aa9e841db53403c6bed47c65d60f567d59106e",
+      "packing5.py": "1b4ecf41aebeefdd25eda15e25b07aab39732b69c6758331d7a2a76b9f71c138",
+      "verify.py": "87cf0244a143a262d477b12ad04eabcacf2b0b0460dafb0a886a6c1af84da5ee"
+    },
+    "banks_pull_request": 237,
+    "commit": "af3fe331ca60c936229e060681ffccbc1c208678",
+    "manifest_sha256": "fc691fdf74a7b06c9290d6e91e6d63dc1c7e20c6556519dcf9b7f53fa02350de",
+    "pull_request": 234,
+    "repository": "https://github.com/CrocSwap/integer-mult-bounds"
+  },
+  "prime": {
+    "criterion": "Lucas-Lehmer sufficiency, independently kernel-checked in Prime.lean",
+    "fixed_before_all_widths": true,
+    "iterations": 125,
+    "p": 127,
+    "q": 170141183460469231731687303715884105727,
+    "residues": [
+      4,
+      14,
+      194,
+      37634,
+      1416317954,
+      2005956546822746114,
+      4023861667741036022825635656102100994,
+      148295852275705128589952510455019292911,
+      17934813421766634732012365957609373869,
+      85902463759488963702490017444612081724,
+      116475895319100247619106962527555061737,
+      49976279066382381059963127566460774395,
+      160668395611328156886231636609761589125,
+      94281146402315220816856494248417316624,
+      108007687823445325965842618064742685120,
+      31734492925565095550179541226941707640,
+      40502963312906587195023713454534295598,
+      94088105965254764875368473681747882892,
+      144493995864766378690749087262700586682,
+      20955297820352149233036565636331346012,
+      158915090152235934934479130912004389942,
+      52870398708381174466959392316679307296,
+      151490860312186869918440828859019512842,
+      95080894369933623491452109744508211636,
+      16832551656452962969322409924830603304,
+      50174049518004850581182191673210576861,
+      144336566379264365321651202616996055222,
+      130822199398052164937252409514558681721,
+      102532921936216636347982935976260898227,
+      113510945853789792879800143796642024867,
+      818764630715300415439121721750598757,
+      98873676748258741042292766411306359072,
+      115157140590183601330851495358050270577,
+      61932212331753972177049746744878494891,
+      162235341974786734396644569954762754962,
+      138222088850540840559618349986527965434,
+      12643335933642280592896036123803678462,
+      107874906898446614736459591766452551411,
+      105127310369349743611680099371735190865,
+      9288955258648756974993511313169148987,
+      22544078789156567134084495007232388871,
+      145330281715042877722945273276030728719,
+      2984059486841025471869552930115409684,
+      37572228739714097091268646718694828173,
+      137863838131209681188612129313912947511,
+      56951438527019760670940985275669549587,
+      33425539749822146052823924594117170181,
+      107032723030256277290622289200228566672,
+      53753380576481396758706859471945799623,
+      47099113889942965118806100149717565037,
+      99592518053374632198667753856515678006,
+      71264320053401377760498554706288870501,
+      93303582026251481068288102203876023525,
+      120228733067825856598036469060895809969,
+      118032048866201789290845587608054171643,
+      2650987091797688081935257855065994022,
+      145145919991993592884437642677980118562,
+      62997327855360484015702535758367792966,
+      83098680626625704955924126176100860767,
+      47102745120534589629594563604260423772,
+      23086037567407917159207583474834256176,
+      1648903944353085502350569803700249218,
+      146001941445125883362200107861188525242,
+      58072554876864005167998859270477790277,
+      85183974222777764635811000451869083253,
+      2178744815368192602929511049691246435,
+      142650016674409483015140356448611524239,
+      131180293024080215139431333296642157751,
+      23796400979692190167798559040061980681,
+      94691321662907057932605046718559371950,
+      28963125299159837855551115831455735161,
+      151145149675516943070949943379933758640,
+      76394190749566845285279900410093015143,
+      47725036928709433877841763022477907753,
+      104312534247659063865391654129512337576,
+      18945859719359721770108285233329380324,
+      164494116784207012462580689820261092953,
+      19312431404447051481513679243141178566,
+      27736528190775597167138586218006816402,
+      2300146040010405501321960790364494805,
+      148671707681260870148526487891403027688,
+      44689644596926350087083033086752357927,
+      114252518218238942159527597790043383515,
+      132347767817386283653136701980558442215,
+      82898165451862550147177322318323559762,
+      82550532064404830850169960592302750413,
+      75643059898515530266520341907002980339,
+      123982986142288470036528246058979625829,
+      82251894353697560270857485942566454845,
+      138612996512155828504361896311563427332,
+      38110442230077683457296715174480894554,
+      139824088758964839080901930176959179789,
+      91384193027872879688983922241190087851,
+      169520666637091361903503058366366526051,
+      169025277276139840475937137620617270244,
+      75767585679605360512739263520802144959,
+      49956247714329574425552443869563509087,
+      183690004880779837464570338561315540,
+      163703822629639553167738612906045835358,
+      169082445910970886147479859194469813067,
+      4415171566587865141382642765195174023,
+      110059221777184243569539344972552339165,
+      5064148876153793895511724877772701976,
+      26339871245616999480560619437480231895,
+      92058826383142394228174232088236221101,
+      25358529928264030171413979572591657174,
+      57391611503696291044494362875786761933,
+      4628408976566823773472049228202071599,
+      62888400681175191832847866264356373833,
+      83454791660308671184475704797189993564,
+      134424104788780027271116197574228580517,
+      15898780365670245164798848628558077094,
+      158133952358979283618604204477670831346,
+      6721506539191163416499937441762326133,
+      882594379818242655466533853441665046,
+      161925513938892243375929285060210027401,
+      80309984059206838477625980764275616860,
+      111061271103311825402106204765050643448,
+      8300180540889597001844078179358966103,
+      132515367850942399280896079195237732275,
+      46864209815407210576219476880150425377,
+      51366641762479717422620116634081008320,
+      142797848550190257259709111711506044974,
+      87676307088191859152273331489412200665,
+      18446744073709551616,
+      0
+    ]
+  },
+  "primitive_contract": {
+    "C_independent_of": [
+      "n",
+      "w",
+      "ancestor_values",
+      "spectator_width_except_logical_volume"
+    ],
+    "C_may_depend_on": [
+      "q",
+      "source_recipe",
+      "finite_bootstrap_level",
+      "retained_primitive_implementations"
+    ],
+    "eligible_prime": "any fixed odd prime q>2^80",
+    "exact_tapes": "Complete high fibers batched; polynomial descriptor preparation amortized over q^w; spectator counters ripple; one extra copied work stream.",
+    "initialization_and_table_scans_charged": true,
+    "numeric_machine_constant_required": false,
+    "q_fixed_before_width": true
+  },
+  "public_accepted": [
+    "26959946667150639794667015035616797377666702258678081076823492475209/26959946667150639794667015087019630673637144422540572481103610249216",
+    "6739986666787659948666753758904199344416675564669520269205873118803/6739986666787659948666753771754907668409286105635143120275902562304"
+  ],
+  "public_excluded": [
+    "26959946667150639794667015099617744664470699630052498678750493617709/26959946667150639794667015087019630673637144422540572481103610249216",
+    "1684996666696914987166688443726109041529418726878281167421905851107/1684996666696914987166688442938726917102321526408785780068975640576"
+  ],
+  "q_power_bound": {
+    "coefficient": 62232333223549834692,
+    "enlarged_role_charge": 655925765880,
+    "low_matrix_power": 14400,
+    "original_coefficient": 1568901757016837,
+    "original_copies": 12,
+    "per_selector_coefficient": 5088069972,
+    "strict_upper": "q^14401",
+    "toll": "C_primitive(q,source,j)*(1+B(q))*(n+w^(1-a_previous))"
+  },
+  "rare_density": "3456000/170141183460469231731687303715884105727",
+  "refined_three_level_kappa": "28343296577831877779/40000000000000000000000",
+  "row_reserve": {
+    "binary_padding_volume_factor_less_than": "q^2",
+    "coarse_coefficient": 57604,
+    "log_q_bound": "4*ceil(log2(max(2,n)))*(14400*w+1)+log_q(S_old_leaf)",
+    "one_outer_padding_factor_less_than": 2,
+    "outside_moment": true,
+    "restored_and_reused": true
+  },
+  "schema": "fixed-prime-bootstrap/1",
+  "scope": "Conditional on the unchanged PR234 all-size and symbolic interfaces",
+  "seventh_level_gain": "17/200000000000000000000000",
+  "six_level_kappa": "708582414684555347597/1000000000000000000000000",
+  "steps": [
+    {
+      "cutoff_log2_at_C_equals_1": 159201314488995,
+      "gaps": {
+        "atom": "4755300055275482587727346675559762399006608969/10000000000000000000000000000000000000000000000000000",
+        "borrowing": "9985823058105078901991100327346675559762399006608969/10000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 1,
+      "minimum_gap": "4755300055275482587727346675559762399006608969/10000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 0,
+      "saving": "7086093297432911263155972653324440237600993391031/10000000000000000000000000000000000000000000000000000"
+    },
+    {
+      "cutoff_log2_at_C_equals_1": 316628660972437393814,
+      "gaps": {
+        "atom": "337191127275856526147041601668407221181702865827194894552051309952453/1000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "borrowing": "998581830617693489926707786147041601668407221181702865827194894552051309952453/1000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 2,
+      "minimum_gap": "337191127275856526147041601668407221181702865827194894552051309952453/1000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 1,
+      "saving": "709084522557691398717843852958398331592778818297134172805105447948690047547/1000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    {
+      "cutoff_log2_at_C_equals_1": 629729153122846809085584527,
+      "gaps": {
+        "atom": "23909712319294679195214939128328443329345875780256291884981584040160324969154756940471242961/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "borrowing": "99858183028074145977404420679195214939128328443329345875780256291884981584040160324969154756940471242961/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 3,
+      "minimum_gap": "23909712319294679195214939128328443329345875780256291884981584040160324969154756940471242961/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 2,
+      "saving": "70908485950972155138142320804785060871671556670654124219743708115018415959839675030845243059528757039/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    {
+      "cutoff_log2_at_C_equals_1": 1252441282715522676358985825842929,
+      "gaps": {
+        "atom": "1695401500656166966497794634155387989629993624737747969934163327808841101349656989027176455404481833208632153350957/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "borrowing": "9985818302805025321910013256166966497794634155387989629993624737747969934163327808841101349656989027176455404481833208632153350957/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 4,
+      "minimum_gap": "1695401500656166966497794634155387989629993624737747969934163327808841101349656989027176455404481833208632153350957/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 3,
+      "saving": "7090848597486491344243043833033502205365844612010370006375262252030065836672191158898650343010972823544595518166791367846649043/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    {
+      "cutoff_log2_at_C_equals_1": 2490926708524325541050407785230987387004,
+      "gaps": {
+        "atom": "120218353531071486551229526967839349913696853993815270754665591341521522322425534534561378430897209675634800873277904682613332729120717209/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "borrowing": "998581830280502362771069613531071486551229526967839349913696853993815270754665591341521522322425534534561378430897209675634800873277904682613332729120717209/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 5,
+      "minimum_gap": "120218353531071486551229526967839349913696853993815270754665591341521522322425534534561378430897209675634800873277904682613332729120717209/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 4,
+      "saving": "709084859748818554356016468928513448770473032160650086303146006184729245334408658478477677574465465438621569102790324365199126722095317386667270879282791/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    {
+      "cutoff_log2_at_C_equals_1": 4954097212275586230463234872753964138165381281,
+      "gaps": {
+        "atom": "8524501435281372531074896948276912015233980193486246819066929170444175398660376588020889166176140200519360662168459192926267798526618573761623509699742720933333/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "borrowing": "99858183028050236265093650501435281372531074896948276912015233980193486246819066929170444175398660376588020889166176140200519360662168459192926267798526618573761623509699742720933333/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 6,
+      "minimum_gap": "8524501435281372531074896948276912015233980193486246819066929170444175398660376588020889166176140200519360662168459192926267798526618573761623509699742720933333/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 5,
+      "saving": "70908485974881867448912498564718627468925103051723087984766019806513753180933070829555824601339623411979110833823859799480639337831540807073732201473381426238376490300257279066667/100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    },
+    {
+      "cutoff_log2_at_C_equals_1": 9852991300260513285888657280692875045232059886615751,
+      "gaps": {
+        "atom": "604459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "borrowing": "9985818302805023626508513204459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "remainder": "9985823330818406876527013749974803189762399006608969/10000000000000000000000000000000000000000000000000000",
+        "stock": "99929091514025118132542563/100000000000000000000000000"
+      },
+      "level": 7,
+      "minimum_gap": "604459490466509553269842850601055451744644509775097484655584796641050648406176144247999888016364295382804364767145993040842916031434367842520401553421121844133995640173868608292047521/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "ordinary_predecessor": 6,
+      "saving": "7090848597488186745743095540509533490446730157149398944548255355490224902515344415203358949351593823855752000111983635704617195635232854006959157083968565632157479598446578878155866004359826131391707952479/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+    }
+  ]
+}
diff --git a/research/fixed-prime-bootstrap/lakefile.toml b/research/fixed-prime-bootstrap/lakefile.toml
new file mode 100644
index 0000000000..9a3ab1f712
--- /dev/null
+++ b/research/fixed-prime-bootstrap/lakefile.toml
@@ -0,0 +1,6 @@
+name = "fixed_prime_certificate"
+version = "0.1.0"
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "f897ebcf72cd16f89ab4577d0c826cd14afaafc7"
diff --git a/research/fixed-prime-bootstrap/lean-toolchain b/research/fixed-prime-bootstrap/lean-toolchain
new file mode 100644
index 0000000000..c00a53503c
--- /dev/null
+++ b/research/fixed-prime-bootstrap/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.24.0
diff --git a/research/fixed-prime-bootstrap/prerequisite.json b/research/fixed-prime-bootstrap/prerequisite.json
new file mode 100644
index 0000000000..a78531890f
--- /dev/null
+++ b/research/fixed-prime-bootstrap/prerequisite.json
@@ -0,0 +1,19 @@
+{
+  "banks_commit": "a8b0ce212bc9f09353a8161bf8a5cee9cefd600c",
+  "banks_files": {
+    "NOTICE": "86fd7612f1acfd909d10e69cf0d28ea1627c6d4bafab093db1ea2f8c0c1ed208",
+    "PROOF.md": "29856b59ea866e8202b8e44f55eee2f97e41ae0a736b5dff862af96785ed0d58",
+    "README.md": "1ceba095158d0e73d33151567fd116f523a787c662edaedf35ff4980dbfce40f",
+    "SOURCE.json": "b6c0f2a75a40e85332e6aab895579fdf27ca182024a8d23b1d906095bbd6c50a",
+    "arithmetic5.py": "1f9e2043aadbbd74605296f74f5acdd3bdabe7482add56c0d16fba3e5d8ad206",
+    "banks.py": "0548a1c15bd6f6dea4505f5fd2ca1bb4ecbe914c8c90769b8cd8beeef428d0cf",
+    "certificate.json": "48bca1692c0eeb93c7080b4638aa9e841db53403c6bed47c65d60f567d59106e",
+    "packing5.py": "1b4ecf41aebeefdd25eda15e25b07aab39732b69c6758331d7a2a76b9f71c138",
+    "verify.py": "87cf0244a143a262d477b12ad04eabcacf2b0b0460dafb0a886a6c1af84da5ee"
+  },
+  "banks_pull_request": 237,
+  "commit": "af3fe331ca60c936229e060681ffccbc1c208678",
+  "manifest_sha256": "fc691fdf74a7b06c9290d6e91e6d63dc1c7e20c6556519dcf9b7f53fa02350de",
+  "pull_request": 234,
+  "repository": "https://github.com/CrocSwap/integer-mult-bounds"
+}
diff --git a/research/fixed-prime-bootstrap/requirements.txt b/research/fixed-prime-bootstrap/requirements.txt
new file mode 100644
index 0000000000..1ca5fd0616
--- /dev/null
+++ b/research/fixed-prime-bootstrap/requirements.txt
@@ -0,0 +1 @@
+sympy==1.14.0
diff --git a/research/fixed-prime-bootstrap/verify.py b/research/fixed-prime-bootstrap/verify.py
new file mode 100644
index 0000000000..af86d4ad2a
--- /dev/null
+++ b/research/fixed-prime-bootstrap/verify.py
@@ -0,0 +1,205 @@
+#!/usr/bin/env python3
+"""Fixed-prime paid moment and seven finite levels on immutable PR237/234.
+
+Copyright 2026 Gabriele Nespoli. Apache-2.0. Developed with OpenAI Codex.
+No floating-point decisions; no parent mutation; no saved execution receipt input.
+"""
+import argparse,importlib.util,json,subprocess,sys,tempfile
+from fractions import Fraction as Q
+from hashlib import sha256
+from pathlib import Path
+HERE=Path(__file__).resolve().parent
+DEPTH=7;GRID=10**24;COARSE_GRID=10**27;PRIME=2**127-1
+sys.dont_write_bytecode=True
+if hasattr(sys,'set_int_max_str_digits'):sys.set_int_max_str_digits(0)
+
+def require(ok,message):
+    if not ok:raise ValueError(message)
+def digest(p):return sha256(p.read_bytes()).hexdigest()
+def serial(x):
+    if isinstance(x,Q):return str(x)
+    if isinstance(x,dict):return {str(k):serial(v)for k,v in x.items()}
+    if isinstance(x,(tuple,list)):return [serial(v)for v in x]
+    return x
+def load(name,path):
+    spec=importlib.util.spec_from_file_location(name,path)
+    mod=importlib.util.module_from_spec(spec);spec.loader.exec_module(mod);return mod
+def inventory(root,manifest):
+    require(not any(p.is_symlink()for p in root.rglob('*')),'Package symlink')
+    actual={p.relative_to(root).as_posix():digest(p)for p in root.rglob('*')if p.is_file()and p!=root/manifest}
+    require(actual==json.loads((root/manifest).read_text())['files'],'Source drift: '+str(root))
+    return actual
+def point(x,grid=GRID):
+    z=x*grid;return Q((z.numerator-1)//z.denominator,grid)
+
+def prime_certificate():
+    require(all(127%d for d in range(2,12)),'Composite Mersenne exponent')
+    values=[4]
+    for _ in range(125):values.append((values[-1]**2-2)%PRIME)
+    require(values[-1]==0 and PRIME>2**80 and PRIME%2==1,'Ineligible prime')
+    return dict(q=PRIME,p=127,iterations=125,residues=values,
+        criterion='Lucas-Lehmer sufficiency, independently kernel-checked in Prime.lean',
+        fixed_before_all_widths=True)
+
+def validate_step(j,predecessor,c,old,a):
+    require(1<=j<=DEPTH and predecessor==j-1,'Cyclic completed supplier')
+    require(a==(1-c)*c+c*old and old<a<c<1-a,'Unpaid finite toll or unattained coarse leaf')
+    gaps=dict(atom=c-a,borrowing=1-a-c,remainder=1-a-c*(1-old),stock=1-c)
+    require(min(gaps.values())>0,'Nonpositive cutoff gap')
+    return gaps
+
+def arithmetic(parent,fresh,banks_root):
+    unbanked=json.loads((fresh/'certificate.json').read_text())
+    bank_package=banks_root/'research/five-stage-banks'
+    sys.path.insert(0,str(bank_package))
+    packing=load('retained_completed_banks',bank_package/'packing5.py')
+    bank_math=load('retained_banked_arithmetic',bank_package/'arithmetic5.py')
+    physical=packing.build(parent.parents[1],16643)
+    computed=bank_math.build(parent.parents[1],unbanked,physical)
+    old=json.loads((bank_package/'certificate.json').read_text())
+    require(serial(computed)==old['arithmetic']and serial(physical)==old['physical'],'Fresh bank certificate mismatch')
+    old=old['arithmetic']
+    finite=json.loads((fresh/'finite.json').read_text())
+    primes=json.loads((fresh/'primes.json').read_text())
+    public=load('retained_five_stage_moment',parent/'code/five_stage_bit_cost_20261009.py')
+    independent=load('independent_atanh_moment',HERE/'base_two_moment.py')
+    outer=load('retained_outer47',parent/'code/paired_cube_assembly.py')
+    cutoffs=load('retained_finite_cutoff',parent/'finite_check.py')
+    prime=prime_certificate();m=120;W=261659
+    H={int(r):n for r,n in old['bit_profile']['histogram'].items()}
+    E=sum(H.values());mass=sum(r*n for r,n in H.items())
+    require((E,mass,max(H))==(5916300,31346280,50)and m*W-mass==52800,'Changed banked profile')
+    require(physical['distinct_charts']==231 and max(physical['max_num'],physical['max_den'])<2**80,'Ineligible bank charts')
+    require(physical['conservative_selector_calls']==12227329044<2**40,'Unpaid bank selectors')
+    require(all(0<r<m and n>0 for r,n in H.items()),'Nonmonotone moment')
+    require(primes['prime_factors']==[2,3,5,7]and primes['all_remaining_factors_below_2_power_80'],'Unverified excluded primes')
+    require(finite['primitive_contract']['eligible_prime']=='any fixed odd prime q>2^80','Prime-specific primitive contract')
+    require(finite['primitive_contract']['initialization_and_table_scans_charged'],'Unpaid prime-dependent tables')
+    proof=(parent/'proof/three-stage-cover-bit.tex').read_text()
+    require('bad fraction at most $2m^3/q<10^{-16}$'in proof,'Detached rare-density bound')
+    rho=Q(2*m**3,PRIME)
+    require(0<rho<Q(1,10**16),'Fallback omitted or no density improvement')
+    fallback=[(1,32*m*m*E)]
+    def paid(a,density=rho):
+        lo,hi=public.moment(H,m,W,a,False)
+        l,u=public.logarithm(Q(m));e,f=public.exponential(a*l,a*u)
+        bill=density*Q(32*m*E,W)
+        return public.floor(lo+bill*e),public.ceil(hi+bill*f)
+    def separate(a):
+        lo,hi=independent.moment(m,W,list(H.items()),a)
+        fl,fu=independent.moment(m,W,fallback,a)
+        return lo+rho*fl,hi+rho*fu
+    c0=Q(old['bit_coarse_saving']);lo=int(c0*COARSE_GRID);hi=lo+COARSE_GRID//10**8
+    require(paid(Q(lo,COARSE_GRID))[1]<1<paid(Q(hi,COARSE_GRID))[0],'Coarse bracket')
+    while hi-lo>1:
+        mid=(lo+hi)//2;l,u=paid(Q(mid,COARSE_GRID))
+        if u<1:lo=mid
+        elif l>1:hi=mid
+        else:raise ValueError('Inconclusive rational moment enclosure')
+    c=Q(lo,COARSE_GRID);excluded=Q(hi,COARSE_GRID)
+    pa,pe,ia,ie=paid(c),paid(excluded),separate(c),separate(excluded)
+    require(pa[1]<1<pe[0]and ia[1]<1<ie[0],'Independent paid moment bracket')
+    require(paid(c,Q(1,10**16))[0]>1,'Improvement does not depend on the certified smaller density')
+    base=Q(384599,10**10);b=Q(747454944651775,10**18)
+    require(Q(old['ordinary_chain'][0])==base,'Changed completed base supplier')
+    require(public.moment({int(r):n for r,n in unbanked['complex_profile']['histogram'].items()},110,14692,b,False)[1]<1,'Complex moment')
+    bridge=unbanked['finite_bridge'];bridge['rows']['degree_gap']=Q(bridge['rows']['degree_gap'])
+    eta=Q(1,10**12);beta=Q(1,10**9)
+    def assemble(a,grid=GRID):
+        require(a<(1-beta)*b,'Complex cap became active')
+        z=a*(1-2*eta);bound=(1-eta)*z/(1+z);k=point(bound,grid)
+        result=outer.assembly(a,b,bridge,k,eta=eta,beta=beta)
+        require(len(result['strict_constraints'])==47 and len(result['margins'])==7,'Incomplete outer assembly')
+        require(all(v>0 for v in result['strict_constraints'].values())and all(v>k for v in result['margins'].values()),'Non-strict outer inequalities')
+        try:outer.assembly(a,b,bridge,k+Q(1,grid),eta=eta,beta=beta)
+        except AssertionError:pass
+        else:raise ValueError('Adjacent kappa point admitted')
+        return dict(kappa=k,bound=bound,assembly=result)
+    chain=[base];steps=[]
+    for j in range(1,DEPTH+1):
+        old_a=chain[-1];a=(1-c)*c+c*old_a;gaps=validate_step(j,j-1,c,old_a,a)
+        require(a==c-c**j*(c-base),'Recurrence mismatch')
+        delta=min(gaps.values());L=cutoffs.cutoff_log2(delta,1)
+        require(L*delta**2>=36 and L*delta>=8,'Cutoff arithmetic')
+        steps.append(dict(level=j,ordinary_predecessor=j-1,saving=a,gaps=gaps,
+            minimum_gap=delta,cutoff_log2_at_C_equals_1=L))
+        chain.append(a)
+    result=assemble(chain[-1]);previous=assemble(Q(old['ordinary_chain'][-1]))
+    require(assemble(Q(old['ordinary_chain'][-1]),10**18)['kappa']==Q(old['kappa']),'Published comparator')
+    require(result['kappa']>previous['bound'],'No genuine improvement over unrounded parent')
+    sixth=assemble(chain[6]);third=assemble(chain[3])
+    require(result['kappa']>sixth['kappa'],'Seventh level does not improve reported grid')
+    require(result['kappa']==assemble(c)['kappa']==assemble(excluded)['kappa'],'Not at this paid family grid cap')
+    delta1=1-Q(mass,m*W)-rho*Q(32*m*E,W)
+    require(delta1>0 and 1-pa[1]>0,'Recurrence contraction gap')
+    require(finite['paid_inventory']['fallback_children']==32*m*m,'Fallback count changed')
+    base_coefficient=finite['q_power_bound']['coefficient']
+    require(base_coefficient==1568901757016837,'Changed base q-power bill')
+    # Pay twelve copies of every original charge plus an intentionally excessive
+    # per-selector wrapper/high-affine/stock/matrix-preparation bill for new banks.
+    d=m*m;N=2*m;K=physical['conservative_selector_calls']
+    per_selector=16*(d+1)**2+(W+12*24)+128*N**3+(8*m*m+8)+1
+    # Also overcharge every original routing family against the entire enlarged
+    # bank role set, instead of relying on a per-copy stock accounting shortcut.
+    enlarged_role_charge=12*208670*(W+12*24)
+    coefficient=12*base_coefficient+enlarged_role_charge+K*per_selector
+    require(coefficient<2**80<PRIME,'Invalid banked q-power overcharge')
+    controls=[]
+    for name,j,pred,a in [('cyclic supplier',DEPTH,DEPTH,chain[-1]),('unattained coarse ordinary leaf',DEPTH,DEPTH-1,c)]:
+        try:validate_step(j,pred,c,chain[-2],a)
+        except ValueError:controls.append(name)
+        else:raise ValueError('Invalid supplier admitted')
+    # An omitted or larger rare density may not be substituted into the published certificate.
+    corrupted=prime['residues'][:];corrupted[37]+=1
+    require(any(corrupted[i+1]!=(corrupted[i]**2-2)%PRIME for i in range(125)),'Corrupt prime residue accepted')
+    controls.extend(['corrupt Lucas-Lehmer residue','old-density paid moment at new coarse point','adjacent coarse and kappa grid points'])
+    return serial(dict(schema='fixed-prime-bootstrap/1',scope='Conditional on the unchanged PR234 all-size and symbolic interfaces',
+        prime=prime,rare_density=rho,depth=DEPTH,coarse_grid=COARSE_GRID,kappa_grid=GRID,
+        banked_profile=old['bit_profile'],bank_physical=physical,
+        coarse=c,excluded_coarse=excluded,public_accepted=pa,public_excluded=pe,
+        independent_accepted=ia,independent_excluded=ie,fallback_histogram=fallback,
+        delta_linear=delta1,delta_tau_lower=1-pa[1],ordinary_chain=chain,steps=steps,
+        eta=eta,beta=beta,complex_saving=b,kappa=result['kappa'],kappa_decimal=public.decimal(result['kappa']),
+        parent_published_kappa=Q(old['kappa']),parent_matched_kappa=previous['kappa'],parent_unrounded_bound=previous['bound'],
+        gain=result['kappa']-Q(old['kappa']),matched_gain=result['kappa']-previous['kappa'],
+        refined_three_level_kappa=third['kappa'],six_level_kappa=sixth['kappa'],seventh_level_gain=result['kappa']-sixth['kappa'],
+        assembly=result['assembly'],minimum_margin=result['bound'],paid_family_grid_cap_attained=True,
+        primitive_contract=finite['primitive_contract'],original_per_copy_paid_inventory=finite['paid_inventory'],
+        bank_extra_selector_calls=K,banked_physical_stock_role_upper=W+12*24,
+        q_power_bound=dict(coefficient=coefficient,low_matrix_power=14400,strict_upper='q^14401',
+            original_copies=12,original_coefficient=base_coefficient,
+            enlarged_role_charge=enlarged_role_charge,per_selector_coefficient=per_selector,
+            toll='C_primitive(q,source,j)*(1+B(q))*(n+w^(1-a_previous))'),
+        cutoff=finite['finite_cutoff'],row_reserve=finite['row_reserve'],controls=controls))
+
+def main():
+    p=argparse.ArgumentParser(description=__doc__);p.add_argument('--parent-root',type=Path,required=True)
+    p.add_argument('--banks-root',type=Path,required=True)
+    p.add_argument('--write',action='store_true');args=p.parse_args()
+    require(not sys.flags.optimize,'Run without -O')
+    own=None if args.write else inventory(HERE,'SOURCE.json')
+    prerequisite=json.loads((HERE/'prerequisite.json').read_text());root=args.parent_root.resolve()
+    require(subprocess.check_output(['git','-C',str(root),'rev-parse','HEAD'],text=True).strip()==prerequisite['commit'],'Wrong parent commit')
+    parent=root/'research/five-stage-source-bound-v8'
+    require(digest(parent/'MANIFEST.json')==prerequisite['manifest_sha256'],'Parent manifest drift')
+    before=inventory(parent,'MANIFEST.json')
+    banks_root=args.banks_root.resolve();banks_package=banks_root/'research/five-stage-banks'
+    require(subprocess.check_output(['git','-C',str(banks_root),'rev-parse','HEAD'],text=True).strip()==prerequisite['banks_commit'],'Wrong bank commit')
+    def bank_inventory():
+        actual={p.relative_to(banks_package).as_posix():digest(p)for p in banks_package.rglob('*')if p.is_file()}
+        require(actual==prerequisite['banks_files'],'Bank source drift');return actual
+    banks_before=bank_inventory()
+    with tempfile.TemporaryDirectory(prefix='fixed-prime-')as tmp:
+        fresh=Path(tmp)/'fresh'
+        print('Replaying all six immutable parent stages.',flush=True)
+        subprocess.run([sys.executable,'-B',str(parent/'verify.py'),'--output',str(fresh)],check=True)
+        result=arithmetic(parent,fresh,banks_root)
+    require(inventory(parent,'MANIFEST.json')==before,'Parent mutation')
+    require(bank_inventory()==banks_before,'Bank source mutation')
+    result['prerequisite']=prerequisite
+    if args.write:(HERE/'certificate.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n')
+    else:
+        require(result==json.loads((HERE/'certificate.json').read_text()),'Certificate mismatch')
+        require(inventory(HERE,'SOURCE.json')==own,'Own source changed')
+    print('PASS kappa='+result['kappa']+' = '+result['kappa_decimal'],flush=True)
+if __name__=='__main__':main()