diff --git a/.github/workflows/lean-bit-moment-discharge.yml b/.github/workflows/lean-bit-moment-discharge.yml
new file mode 100644
index 0000000000..c14f6def3a
--- /dev/null
+++ b/.github/workflows/lean-bit-moment-discharge.yml
@@ -0,0 +1,41 @@
+name: Lean BIT moment discharge
+on:
+  pull_request:
+    paths:
+      - 'research/lean-bit-moment-discharge/**'
+      - '.github/workflows/lean-bit-moment-discharge.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'research/lean-bit-moment-discharge/**'
+      - '.github/workflows/lean-bit-moment-discharge.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  formal:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.12'
+      - name: Download checksum-pinned official Lean
+        shell: bash
+        run: |
+          curl --fail --location --retry 3 https://github.com/leanprover/lean4/releases/download/v4.33.0-rc1/lean-4.33.0-rc1-linux.tar.zst -o "$RUNNER_TEMP/lean.tar.zst"
+          echo "25e7b3e18ec75a4e2529fc23194be8e3cc3183df99b553f870d8a111c7488210  $RUNNER_TEMP/lean.tar.zst" | sha256sum --check
+          tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP"
+      - name: Build local proofs and check actual Lean rejection controls
+        shell: bash
+        run: |
+          python -I -O -B research/lean-bit-moment-discharge/verify.py \
+            --lake "$RUNNER_TEMP/lean-4.33.0-rc1-linux/bin/lake" \
+            --work-dir "$RUNNER_TEMP/bit-moment-build" \
+            --fetch-cache --out "$RUNNER_TEMP/bit-moment-result.json"
+      - name: Source and receipt failure controls
+        run: python -I -O -B research/lean-bit-moment-discharge/test_package.py
+      - run: git diff --exit-code
diff --git a/research/lean-bit-moment-discharge/DYADIC.json b/research/lean-bit-moment-discharge/DYADIC.json
new file mode 100644
index 0000000000..9bcaed94aa
--- /dev/null
+++ b/research/lean-bit-moment-discharge/DYADIC.json
@@ -0,0 +1,194 @@
+{
+  "schema": "bit-dyadic-moment/1",
+  "grid": 1000000000000,
+  "numerator": 130849,
+  "bits": 17,
+  "exponent": "9983/10000",
+  "base_denominator": 64,
+  "rows": [
+    {
+      "rank": 1,
+      "count": 381024,
+      "upper_numerators": [
+        125000000000,
+        353553390594,
+        594603557502,
+        771105412705,
+        878126080188,
+        117135477132,
+        342250605744,
+        585021884842,
+        95608404185,
+        38650760865,
+        24574745951,
+        19595417972,
+        17497954333,
+        16534979180,
+        16073551247,
+        15847688735,
+        15735950448
+      ]
+    },
+    {
+      "rank": 2,
+      "count": 400416,
+      "upper_numerators": [
+        176776695297,
+        420448207628,
+        648419777327,
+        805245165976,
+        897354537503,
+        167458440507,
+        409216862443,
+        639700603754,
+        141388273444,
+        66470922554,
+        45576488784,
+        37739439245,
+        34341774509,
+        32759433045,
+        31995816644,
+        31620709514,
+        31434808292
+      ]
+    },
+    {
+      "rank": 3,
+      "count": 22752,
+      "upper_numerators": [
+        216506350947,
+        465302429553,
+        682130800913,
+        825912102414,
+        908797063384,
+        206397340938,
+        454309741188,
+        674025030091,
+        177749608398,
+        91279860286,
+        65412104774,
+        55373210231,
+        50947220038,
+        48868711251,
+        47861475530,
+        47365669694,
+        47119696168
+      ]
+    },
+    {
+      "rank": 4,
+      "count": 26880,
+      "upper_numerators": [
+        250000000000,
+        500000000000,
+        707106781187,
+        840896415254,
+        917004043205,
+        239400820175,
+        489286031045,
+        699489836270,
+        209088772456,
+        114315564464,
+        84526462005,
+        72683587387,
+        67399734508,
+        64903647099,
+        63690485504,
+        63092434919,
+        62795518809
+      ]
+    },
+    {
+      "rank": 5,
+      "count": 29376,
+      "upper_numerators": [
+        279508497188,
+        528685631721,
+        727107716725,
+        852706113925,
+        923420875834,
+        268593104760,
+        518259688535,
+        719902554889,
+        237154774569,
+        136116555802,
+        103121801391,
+        89757399326,
+        83739457978,
+        80883528327,
+        79492299317,
+        78805684340,
+        78464604053
+      ]
+    },
+    {
+      "rank": 6,
+      "count": 17376,
+      "upper_numerators": [
+        306186217848,
+        553340959851,
+        743868913083,
+        862478355139,
+        928697127776,
+        295068391613,
+        543201980495,
+        737022374488,
+        262860890222,
+        156981554517,
+        121313728556,
+        106645028258,
+        99989856482,
+        96819672822,
+        95272474132,
+        94508171340,
+        94128322322
+      ]
+    },
+    {
+      "rank": 7,
+      "count": 26784,
+      "upper_numerators": [
+        330718913884,
+        575081658449,
+        758341386481,
+        870827989032,
+        933181648466,
+        319478861275,
+        565224611350,
+        751814213321,
+        286757178781,
+        177099030007,
+        139176888912,
+        123379383306,
+        116166346457,
+        112719537543,
+        111034676650,
+        110201713955,
+        109787578824
+      ]
+    },
+    {
+      "rank": 42,
+      "count": 288,
+      "upper_numerators": [
+        810092587301,
+        900051435920,
+        948710406774,
+        974017662455,
+        986923331600,
+        804778501430,
+        897094477427,
+        947150715265,
+        788395622066,
+        719294534236,
+        687049516478,
+        671473190224,
+        663817957791,
+        660023132020,
+        658133862059,
+        657191256011,
+        656720459372
+      ]
+    }
+  ]
+}
diff --git a/research/lean-bit-moment-discharge/FINITE.json b/research/lean-bit-moment-discharge/FINITE.json
new file mode 100644
index 0000000000..d6d68012ec
--- /dev/null
+++ b/research/lean-bit-moment-discharge/FINITE.json
@@ -0,0 +1,30 @@
+{
+  "schema": "bit-moment-discharge-finite/1",
+  "certificate": {
+    "square_steps": 136,
+    "rounded_exponent": "130849/131072",
+    "exponent_gap": "111/81920000",
+    "ordinary_upper": "73992244255723/74000000000000",
+    "fallback_upper": "4635220903839/705718994140625000000000",
+    "moment_upper": "11290320473664709188758299/11291503906250000000000000",
+    "margin": "54282194665811241701/11291503906250000000000000",
+    "upper_numerators": {
+      "1": 15735950448,
+      "2": 31434808292,
+      "3": 47119696168,
+      "4": 62795518809,
+      "5": 78464604053,
+      "6": 94128322322,
+      "7": 109787578824,
+      "42": 656720459372
+    }
+  },
+  "direct_actual_exponent_controls": 8,
+  "calibration": {
+    "cases": 4774,
+    "domain": "1<=r<=m, 2<=m<=12, 1<=k<=5, 0<=p<2^k",
+    "trace_sha256": "025edcb3258c87bbce18d514a6e7b439aaf6028375f353662b3a0dca424eddba"
+  },
+  "kernel_checked": false,
+  "scope": "Finite exact arithmetic and source-to-Lean binding only; explicit kernel mode builds the Real theorem."
+}
diff --git a/research/lean-bit-moment-discharge/PROOF-SOURCES.json b/research/lean-bit-moment-discharge/PROOF-SOURCES.json
new file mode 100644
index 0000000000..895f490cbc
--- /dev/null
+++ b/research/lean-bit-moment-discharge/PROOF-SOURCES.json
@@ -0,0 +1,94 @@
+{
+  "axiom_targets": [
+    "ClosedBitRecurrence.uniform_bound",
+    "DyadicPower.half_step",
+    "DyadicPower.upper_of_rounded_exponent",
+    "DyadicPower.negative_square_is_not_upper",
+    "DyadicPower.upward_exponent_is_not_upper",
+    "SelectedStoppedRecurrence.exact_linear_moment",
+    "SelectedStoppedRecurrence.selected_bound",
+    "SelectedStoppedRecurrence.selected_positive_bound",
+    "SelectedStoppedRecurrence.selected_uniform_bound",
+    "SelectedBitMoment.rank_1_upper",
+    "SelectedBitMoment.rank_2_upper",
+    "SelectedBitMoment.rank_3_upper",
+    "SelectedBitMoment.rank_4_upper",
+    "SelectedBitMoment.rank_5_upper",
+    "SelectedBitMoment.rank_6_upper",
+    "SelectedBitMoment.rank_7_upper",
+    "SelectedBitMoment.rank_42_upper",
+    "SelectedBitMoment.per_rank_upper",
+    "SelectedBitMoment.fractional_moment_upper",
+    "SelectedBitMoment.fractional_moment_strict",
+    "StoppedRecurrence.worst_eq_positive",
+    "StoppedRecurrence.stopped_bound"
+  ],
+  "dependencies": {
+    "Cli": {
+      "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
+      "url": "https://github.com/leanprover/lean4-cli"
+    },
+    "LeanSearchClient": {
+      "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715",
+      "url": "https://github.com/leanprover-community/LeanSearchClient"
+    },
+    "Qq": {
+      "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
+      "url": "https://github.com/leanprover-community/quote4"
+    },
+    "aesop": {
+      "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
+      "url": "https://github.com/leanprover-community/aesop"
+    },
+    "batteries": {
+      "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366",
+      "url": "https://github.com/leanprover-community/batteries"
+    },
+    "importGraph": {
+      "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
+      "url": "https://github.com/leanprover-community/import-graph"
+    },
+    "mathlib": {
+      "rev": "55b7917b472489c7c56a0fa6393af05cfd536599",
+      "url": "https://github.com/leanprover-community/mathlib4.git"
+    },
+    "plausible": {
+      "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+      "url": "https://github.com/leanprover-community/plausible"
+    },
+    "proofwidgets": {
+      "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
+      "url": "https://github.com/leanprover-community/ProofWidgets4"
+    }
+  },
+  "files": {
+    "DYADIC.json": "6c56d2399880eba4280628b24aa880a1f9f7bb09742a07c1de863f096273cbff",
+    "lean/ClosedRecurrence.lean": "783775e173f952631ae801f72ca8eb08708bff918e34370971d7c19df73fa8eb",
+    "lean/DyadicPower.lean": "1b1e3fde020eaf2e4153dd22b435bef88bdf75e12da0f04ab8e950a00f4df887",
+    "lean/Selected.lean": "1d63b79d222e3518c90a9018ee8116397361ec34bd3cba85a921bc3850a8cf45",
+    "lean/SelectedMoment.lean": "c17c0550f9a62c5aa181b01fdbcbcb3e8909a21844e385d09815804f45cd33e4",
+    "lean/StoppedRecurrence.lean": "c6092eb394d2f97ca6cb701fc59cf79e6bcfc63e40e126e67c3b1021ca2abb95",
+    "lean/lake-manifest.json": "d15034efffe21744b6338258cb5779d73b62c81488658a81f1a0be4b46beb053",
+    "lean/lakefile.toml": "ca0788110a757b9ca53a6068ce39d8731a2bd9382f0806395ddab545da1455de",
+    "lean/lean-toolchain": "62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef",
+    "sources/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045",
+    "sources/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4",
+    "sources/GLOBAL.json": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819"
+  },
+  "lean_commit": "62eed1db4d67327ec8120be05f1a1b0847d74561",
+  "lean_version": "4.33.0-rc1",
+  "schema": "bit-moment-discharge-proof-sources/1",
+  "toolchain": "leanprover/lean4:v4.33.0-rc1",
+  "toolchain_archive": {
+    "sha256": "25e7b3e18ec75a4e2529fc23194be8e3cc3183df99b553f870d8a111c7488210",
+    "url": "https://github.com/leanprover/lean4/releases/download/v4.33.0-rc1/lean-4.33.0-rc1-linux.tar.zst"
+  },
+  "recurrence_predecessor": {
+    "pr": 2289,
+    "head": "32ef80ad161b8602b32698ed43186ecc2266cb5b",
+    "unchanged_modules": [
+      "StoppedRecurrence.lean",
+      "Selected.lean"
+    ]
+  }
+}
diff --git a/research/lean-bit-moment-discharge/README.md b/research/lean-bit-moment-discharge/README.md
new file mode 100644
index 0000000000..95436c6099
--- /dev/null
+++ b/research/lean-bit-moment-discharge/README.md
@@ -0,0 +1,103 @@
+# Discharge the selected BIT fractional moment in Lean
+
+This proves the numerical hypothesis left explicit in [PR2289](https://github.com/CrocSwap/integer-mult-bounds/pull/2289), then composes it with that package's unchanged stopped-recurrence theorem. For the literal selected BIT profile, including its fallback allowance, Lean proves fractionalMoment < 9999/10000 at τ=9983/10000. The resulting root-family time bound has no supplied numerical moment premise.
+
+The moment point and inequality are credited predecessor results from [Jose Manuel's PR2234](https://github.com/CrocSwap/integer-mult-bounds/pull/2234). The new coverage is the checked implication from rational certificate steps to the actual Real.rpow expression and its recurrence corollary. It does not prove that the physical machine satisfies the recurrence or has one uniform local-charge constant. No selected supplier, frontier or κ changes.
+
+## Exact statement and source binding
+
+The inherited [Selected.lean](lean/Selected.lean) fixes m=64, W=28416, ranks (1,2,3,4,5,6,7,42) and counts (381024,400416,22752,26880,29376,17376,26784,288). Write a_r=H_r/W and b=118606528512/(10^16 W), where the fallback numerator equals 32·64²·ΣH_r. The expression is
+
+\[
+\mu_\tau=\sum_r a_r(r/64)^\tau+b(1/64)^\tau.
+\]
+
+[SelectedMoment.lean](lean/SelectedMoment.lean) proves the exact Real bound
+
+    μτ ≤ 11290320473664709188758299 / 11291503906250000000000000
+       < 9999 / 10000.
+
+The positive rational margin below 9999/10000 is
+
+    54282194665811241701 / 11291503906250000000000000.
+
+This upper enclosure is deliberately coarser than PR2289's Python certificate. Its purpose is to close the formal numerical premise, not to increase an exponent or print more digits.
+
+The two recurrence modules are retained byte-for-byte from PR2289 head 32ef80ad161b8602b32698ed43186ecc2266cb5b and are rebuilt locally. The selected GLOBAL.json and EXPECTED.json profiles must agree, the inherited Lean literals must match them, and ASSEMBLY.json must bind the same bit endpoint. Those JSON files are immutable snapshots of canonical base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2. [SOURCES.json](SOURCES.json) records Git identities; [PROOF-SOURCES.json](PROOF-SOURCES.json) pins all proof inputs.
+
+## Why the rational certificate bounds a real power
+
+For 0<x≤1, round τ down to q=130849/131072. The exact gap is τ−q=111/81920000. Since powers of such a base decrease as the exponent increases, x^τ≤x^q.
+
+Read the 17 binary digits b_i of 130849 from least significant to most significant. Set e_0=0, u_0=1 and
+
+    e_(i+1) = (e_i+b_i)/2,
+    u_(i+1) ≥ 0,
+    u_i*x^b_i ≤ u_(i+1)^2.
+
+Then e_17=q. If x^e_i≤u_i, the square of x^e_(i+1) is x^e_i·x^b_i≤u_(i+1)^2. Both sides are nonnegative, so x^e_(i+1)≤u_(i+1). [DyadicPower.half_step](lean/DyadicPower.lean) proves this implication over actual real powers; upper_of_rounded_exponent supplies the final exponent comparison.
+
+[DYADIC.json](DYADIC.json) proposes each u_i on the grid 10^-12. The 8 ranks require 136 small rational square inequalities. The generated Lean source proves every inequality with norm_num, checks every exponent transition, and aggregates the full selected profile and fallback. No additional axiom, sorry or native_decide is used; every rational certificate obligation is proved. The Python square-root generator is outside the formal trust base: its proposals must survive Lean.
+
+The same Lean module proves why a negative square root and upward exponent rounding cannot serve as these upper bounds. Kernel-mode controls corrupt the first root downward, replace it by its negative, and attempt the reversed exponent comparison. The first two fail on explicit false arithmetic obligations; the third fails with an actual type mismatch.
+
+## Recurrence corollary and remaining assumptions
+
+[ClosedBitRecurrence.uniform_bound](lean/ClosedRecurrence.lean) supplies the proved moment inequality to PR2289's selected_uniform_bound. For arbitrary root contexts u with limits N_u, widths w_u≥0, costs T_u and **one C≥0 shared across the family**, it assumes T_u(1)≥0 and the following only for 1≤n≤N_u:
+
+- For n<64, T_u(n)≤Cw_u.
+- For n≥64 and f=⌊n/64⌋, T_u(n)≤Σ_r a_r T_u(rf)+b max_(1≤j≤f) T_u(j)+C(n+w_u).
+
+It concludes
+
+\[
+T_u(n)\le200Cn+10000Cn^{9983/10000}w_u\qquad(1\le n\le N_u).
+\]
+
+It retains the actual fallback maximum, allows root-coupled widths, imposes no monotonicity assumption on T and leaves T_u(0) unrestricted. The new formal result removes exactly the numerical moment premise. Completed packet endpoints, frozen-ancestor preparation/access, parking, the physical recurrence and the existence of the shared C remain outside this proof.
+
+## Reproduce and interpret the evidence
+
+Python 3.12 standard-library source and arithmetic checks:
+
+    python3.12 -I -O -B research/lean-bit-moment-discharge/verify.py
+    python3.12 -I -O -B research/lean-bit-moment-discharge/test_package.py
+    python3.12 scripts/research_package.py --package research/lean-bit-moment-discharge
+
+Default replay reports PASS_BIT_MOMENT_SOURCES_AND_FINITE_ONLY and kernel_checked=false. It regenerates the certificate proposals and exact Lean source, checks 136 square steps, checks all 8 final upper bounds by a separate direct 10000th-power comparison at the actual source exponent, and performs 4,774 direct-power calibrations. The calibration domain is 1≤r≤m, 2≤m≤12, 1≤k≤5, 0≤p<2^k. The exponent-one endpoint is explicitly rejected by the low-bit proposal routine; exponent zero is included.
+
+Eleven failure-control groups cover corrupt or negative roots, missing/reversed chains, omitted ranks, changed counts, upward rounding, strict types/JSON, source drift, formal-profile/fallback mismatches, regenerated-source drift, proof escapes, axiom inventory/trust, receipt drift, preserved existing output and incomplete kernel arguments. These are finite checks, not a substitute for running Lean.
+
+Install the official Linux Lean 4.33.0-rc1 binary identified and checksum-pinned in PROOF-SOURCES.json. Then use new paths:
+
+    python3.12 -I -O -B research/lean-bit-moment-discharge/verify.py \
+      --lake /absolute/path/lean-4.33.0-rc1-linux/bin/lake \
+      --work-dir /tmp/bit-moment-new-build \
+      --fetch-cache --out /tmp/bit-moment-new-result.json
+
+Alternatively, --packages /absolute/path/to/.lake/packages reuses a pinned library cache. The driver checks all nine dependency Git heads and tracked-source cleanliness, builds all five local modules from source, requires all 22 axiom reports, and runs the three actual Lean rejection controls. Only this mode reports PASS_BIT_MOMENT_DISCHARGE_KERNEL and kernel_checked=true.
+
+The fresh local build passed with Lean commit 62eed1db4d67327ec8120be05f1a1b0847d74561 and Mathlib 55b7917b472489c7c56a0fa6393af05cfd536599. All inspected theorem dependencies are among propext, Classical.choice and Quot.sound. Trust includes that Lean binary/kernel and imported Mathlib proof objects from the official cache; Mathlib was not rebuilt from source. The scoped [workflow](../../.github/workflows/lean-bit-moment-discharge.yml) performs the checksum-pinned installation and proof build.
+
+The registered replay passed on Python 3.12.3. Both lightweight commands passed on Python 3.14.4 from a Git-free, read-only export with all 22 package files unchanged; a direct write probe was rejected.
+
+To reproduce the untrusted proposals separately:
+
+    python3.12 -I -B research/lean-bit-moment-discharge/certificate.py \
+      --out-dir /tmp/bit-moment-new-proposals
+
+This requires a new output directory and explicitly reports that no kernel has run. TASK.json records environments, source pins, overlap review and verification limits.
+
+## Open next questions
+
+The numerical premise at this point is now discharged; another equivalent enclosure is not the next missing implication. Establish the physical local-charge C(n+w) for the realized recursive caller with one C across the permitted root contexts. First give one explicit frozen-ancestor evaluator a complete preparation/access bill, then amortize each preparation against its complete target fibre with the generation-depth bound. A physical packet/caller and parking implementation remains the prerequisite. This arithmetic proof cannot establish that interface.
+
+## Attribution and overlap
+
+Prepared by Gareth Davidson (@bitplane) with substantial OpenAI Codex assistance, without subagents or independent human review, under Apache-2.0. PR2234's recurrence, profile, moment point and proposed ordinary saving retain Jose Manuel's and the credited predecessor contributors' authorship. The selected PR589 profile retains DreamingOfClouds' tuning, eumemic's base word and the hosting/routing lineage. My PR2289 supplies the unchanged recurrence proofs and adapted build/test wrapper.
+
+Earlier Lean PR585/605/842/885 certify other historical complex expressions; their published scopes were read and their achievements are not claimed here. Dugongue's concurrent PR2284 (e71574b92f6af546013c71293cd03ff58742a1e6) proves generic rational aggregation assuming per-term real upper bounds, alongside other moment lemmas. Its MomentTransfer.lean was inspected; no full replay is claimed. This package supplies the missing concrete Real bounds for the selected BIT expression.
+
+Repeated-square-root numerical enclosure is prior art in [independent-queue-ceilings](../independent-queue-ceilings/README.md) and [idle-stability-radical-audit](../idle-stability-radical-audit/README.md). The new contribution is the Lean proof and this source-bound composition, not invention of that numerical method. No predecessor numerical engine is imported.
+
+Original single OS nonce de346470d4c367b36f566f9208c8fab2, priority revision 4, independent-verification / independent-moment, refined without rerolling. [Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2209#discussioncomment-18940025).
diff --git a/research/lean-bit-moment-discharge/SOURCES.json b/research/lean-bit-moment-discharge/SOURCES.json
new file mode 100644
index 0000000000..104d08adee
--- /dev/null
+++ b/research/lean-bit-moment-discharge/SOURCES.json
@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/community-frontier1094-audit/ASSEMBLY.json",
+      "usage": "provenance",
+      "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0",
+      "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"
+    },
+    {
+      "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json",
+      "usage": "provenance",
+      "git_blob": "1f648db9e63e7bfcaa6d5b1dd9fa6503caac47d2",
+      "sha256": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+      "usage": "provenance",
+      "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13",
+      "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"
+    }
+  ],
+  "scope": "Exact historical source-bound proof. Runtime checks use local immutable snapshots; future selection changes do not rebind this result.",
+  "snapshots": [
+    {
+      "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+      "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json",
+      "local_path": "sources/GLOBAL.json",
+      "git_blob": "1f648db9e63e7bfcaa6d5b1dd9fa6503caac47d2",
+      "sha256": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819"
+    },
+    {
+      "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+      "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+      "local_path": "sources/EXPECTED.json",
+      "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13",
+      "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"
+    },
+    {
+      "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+      "path": "research/community-frontier1094-audit/ASSEMBLY.json",
+      "local_path": "sources/ASSEMBLY.json",
+      "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0",
+      "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"
+    },
+    {
+      "commit": "32ef80ad161b8602b32698ed43186ecc2266cb5b",
+      "path": "research/lean-stopped-recurrence-audit/lean/StoppedRecurrence.lean",
+      "local_path": "lean/StoppedRecurrence.lean",
+      "git_blob": "034da5b718de8e0d8f9d29c42ca4a2a9752dd219",
+      "sha256": "c6092eb394d2f97ca6cb701fc59cf79e6bcfc63e40e126e67c3b1021ca2abb95"
+    },
+    {
+      "commit": "32ef80ad161b8602b32698ed43186ecc2266cb5b",
+      "path": "research/lean-stopped-recurrence-audit/lean/Selected.lean",
+      "local_path": "lean/Selected.lean",
+      "git_blob": "129c0b14ec5510fa587c9cf365481333c3da2d8f",
+      "sha256": "1d63b79d222e3518c90a9018ee8116397361ec34bd3cba85a921bc3850a8cf45"
+    }
+  ],
+  "implementation_lineage": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2289",
+    "head": "32ef80ad161b8602b32698ed43186ecc2266cb5b",
+    "author": "Gareth Davidson",
+    "reuse": "Two unchanged recurrence modules and adapted build/failure-control wrapper; new Real moment proofs are separate."
+  }
+}
diff --git a/research/lean-bit-moment-discharge/TASK.json b/research/lean-bit-moment-discharge/TASK.json
new file mode 100644
index 0000000000..72b64b8937
--- /dev/null
+++ b/research/lean-bit-moment-discharge/TASK.json
@@ -0,0 +1,175 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?",
+    "starting_points": [
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Reconstruct the rank ledger from original operations rather than trusting its aggregate.",
+      "Implement certified moment inequalities through a different exact enclosure method."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove the selected BIT fractionalMoment bound over Real.rpow in Lean and discharge the numerical premise of the root-uniform stopped recurrence at the exact PR2289 source head.",
+  "scope_change_reason": "The point is already numerically checked. This targets its newly explicit missing numerical-to-Real implication in PR2289, using kernel-checked dyadic square certificates instead of another external evaluation or more digits. No reroll or new supplier is claimed.",
+  "bottleneck_link": "Removes an explicit numerical proof premise from one scoped uniform-time implication in the proposed selected BIT closure; physical recurrence and uniform local-charge obligations remain.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at actual Lean acceptance of the Real moment and its composed recurrence corollary, exact source binding and meaningful corrupted-certificate controls. Do not imply physical supplier or full multiplication admission.",
+  "outcome": "completed",
+  "evidence": "Fresh build of five local Lean modules passed; 22 standard-axiom reports and three genuine Lean rejection controls. The certificate has 136 square steps; independent direct powers check eight actual-exponent upper bounds and 4774 small dyadic cases. Eleven failure-control groups pass under optimized Python 3.12.",
+  "author": "Gareth Davidson",
+  "ai_assistance": "Substantial OpenAI Codex assistance for proof development, source review, exact arithmetic, checks and documentation. No subagents or independent human review.",
+  "open_questions": [
+    {
+      "question": "Can the realized recursive caller establish one local-charge C(n+w) across the permitted root contexts?",
+      "why_it_matters": "The numerical premise is now discharged; this physical premise remains necessary for the time theorem.",
+      "first_step": "Give one frozen-ancestor evaluator a complete preparation/access bill and amortize it against the target fibre with the global generation-depth bound.",
+      "blocked_by": "A source-bound physical packet/caller and parking implementation with explicit control, descriptor and scratch costs."
+    }
+  ],
+  "selection": {
+    "seed": "de346470d4c367b36f566f9208c8fab2",
+    "track": "independent-verification",
+    "scope_key": "c191650c0fa8d2fa514e",
+    "draw_method": "Implement certified moment inequalities through a different exact enclosure method.",
+    "rerolled": false
+  },
+  "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2209#discussioncomment-18940025",
+  "predecessor": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2289",
+    "head": "32ef80ad161b8602b32698ed43186ecc2266cb5b",
+    "author": "Gareth Davidson",
+    "reuse": "Two unchanged recurrence modules and adapted build/failure-control wrapper; new Real moment proofs are separate."
+  },
+  "original_claim_source": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2234",
+    "head": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f",
+    "author": "Jose Manuel / jmbarrancoml",
+    "credit": "Original recurrence, selected profile instantiation, moment point and proposed saving; no numerical novelty claimed."
+  },
+  "first_step": {
+    "command": "python3.12 -B scripts/research_baseline.py",
+    "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+    "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+    "scope": "Orientation only; selected full cold replay was not rerun."
+  },
+  "validation": {
+    "checked_at_utc": "2026-10-15T03:59:48.534956+00:00",
+    "lean_version": "Lean (version 4.33.0-rc1, x86_64-unknown-linux-gnu, commit 62eed1db4d67327ec8120be05f1a1b0847d74561, Release)",
+    "dependencies": 9,
+    "local_modules_built": 5,
+    "axiom_targets": 22,
+    "allowed_axioms": [
+      "propext",
+      "Classical.choice",
+      "Quot.sound"
+    ],
+    "rejected_invalid_proofs": [
+      "small_square",
+      "negative_square",
+      "upward_exponent"
+    ],
+    "square_steps": 136,
+    "direct_actual_exponent_controls": 8,
+    "calibration_cases": 4774,
+    "failure_control_groups": 11,
+    "full_replay_kernel_checked": true,
+    "default_replay_kernel_checked": false,
+    "proof_sources_sha256": "273b424aee0255f0a764dcce4d3d9acb81d545decdf17392a7b83c25e65724a0",
+    "finite_receipt_sha256": "86d35c051aab8ab5a37ae99745a4778082c41818904f2ef09fd81997b1136701",
+    "library_trust": "Official Mathlib proof-object cache, exact dependency Git heads and tracked source cleanliness; no Mathlib source rebuild.",
+    "unrun": [
+      "full predecessor recursive-machine replay",
+      "physical uniform local-charge or frozen-ancestor access proof",
+      "selected full cold replay",
+      "full multiplication theorem",
+      "independent human review"
+    ],
+    "registered_python": "3.12.3",
+    "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE",
+    "source_export": {
+      "python": "Python 3.14.4",
+      "git_free": true,
+      "readonly_write_rejected": true,
+      "files": 22,
+      "hashes_unchanged": true,
+      "commands": [
+        "python3.14 -I -O -B verify.py",
+        "python3.14 -I -O -B test_package.py"
+      ]
+    }
+  },
+  "freshness": {
+    "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "predecessor_head": "32ef80ad161b8602b32698ed43186ecc2266cb5b",
+    "overlap_searched_at": "2026-10-15T03:57:30.315615+00:00",
+    "overlap_coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-15T03:56:02.337684+00:00",
+        "complete_pagination": true,
+        "records": 512
+      },
+      "discussions": {
+        "fetched_at": "2026-10-15T03:57:29.915675+00:00",
+        "complete_pagination": true,
+        "records": 1003
+      }
+    },
+    "warnings": [],
+    "decision": "Canonical main and PR2289 are unchanged. Targeted matches cover the predecessor thread, our two scoped claims and prior numerical dyadic methods; no other specific Real discharge was found."
+  },
+  "overlap_review": [
+    {
+      "prs": [
+        585,
+        605,
+        842,
+        885
+      ],
+      "coverage": "Published scopes read: different historical complex expressions, not this fallback-bearing BIT moment. Full packages not replayed."
+    },
+    {
+      "pr": 2284,
+      "head": "e71574b92f6af546013c71293cd03ff58742a1e6",
+      "file_read": "research/kappa-lemma-toolkit/MomentTransfer.lean",
+      "coverage": "Generic rational aggregation retains per-term Real upper bounds; this package proves the concrete selected BIT bounds."
+    },
+    {
+      "paths": [
+        "research/independent-queue-ceilings/README.md",
+        "research/idle-stability-radical-audit/README.md"
+      ],
+      "coverage": "Prior repeated-square-root numerical methods credited; no claim to invent the method."
+    }
+  ]
+}
diff --git a/research/lean-bit-moment-discharge/VERIFY.json b/research/lean-bit-moment-discharge/VERIFY.json
new file mode 100644
index 0000000000..89011c2b58
--- /dev/null
+++ b/research/lean-bit-moment-discharge/VERIFY.json
@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Source-to-Lean binding, 136 rational square steps, 8 direct actual-exponent power controls and 4774 dyadic calibrations; explicitly kernel_checked=false."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Eleven failure-control groups including corrupted square chains, exponent direction, missing ranks, fallback/profile drift, proof escapes, axiom inventory and receipt drift."
+    }
+  ]
+}
diff --git a/research/lean-bit-moment-discharge/certificate.py b/research/lean-bit-moment-discharge/certificate.py
new file mode 100644
index 0000000000..33d4f92d74
--- /dev/null
+++ b/research/lean-bit-moment-discharge/certificate.py
@@ -0,0 +1,172 @@
+"""Untrusted dyadic certificate proposals and exact source/step checks.
+
+Lean proves the Real interpretation independently. This module uses only
+integer square roots and rational arithmetic, never logs, exp or floats.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0.
+"""
+from fractions import Fraction as Q
+from pathlib import Path
+from math import isqrt
+import json
+import re
+
+HERE = Path(__file__).resolve().parent
+GRID, NUMERATOR, BITS = 10**12, 130849, 17
+EXPONENT = Q(9983, 10000)
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def fraction(q):
+    return f"{q.numerator}/{q.denominator}"
+
+
+def profile(root=HERE):
+    read = lambda name: json.loads((root / "sources" / name).read_bytes())
+    global_record, expected, assembly = (read(n) for n in ["GLOBAL.json", "EXPECTED.json", "ASSEMBLY.json"])
+    counts = {int(k): v for k, v in global_record["profile"].items()}
+    need(counts == {int(k): v for k, v in expected["nine"]["profile"].items()}, "profile source agreement")
+    need((global_record["m"], global_record["live"], global_record["maxchild"]) == (64, 28416, 42),
+         "selected dimensions")
+    need(assembly["bit_lower"] == expected["nine"]["bit_lower"], "selected assembly binding")
+    formal = (root / "lean/Selected.lean").read_text()
+    def vector(name):
+        match = re.search(r"def " + name + r"[^\n]*:= !\[([^]]+)\]", formal)
+        need(match is not None, "literal formal vector")
+        return [int(x.strip()) for x in match[1].split(",")]
+    need(list(zip(vector("ranks"), vector("counts"))) == sorted(counts.items()), "formal profile binding")
+    need("counts r / 28416" in formal and "118606528512 / (10000000000000000 * 28416)" in formal
+         and "9983 / 10000" in formal, "formal scalar binding")
+    need(all(type(c) is int and c > 0 and 0 < r < 64 for r, c in counts.items()), "proper positive profile")
+    need(32 * 64**2 * sum(counts.values()) == 118606528512, "fallback count")
+    return counts
+
+
+def propose_chain(x, numerator, bits, grid):
+    need(0 < x <= 1, "base domain")
+    need(type(bits) is int and bits > 0 and type(numerator) is int and 0 <= numerator <= 2**bits,
+         "exponent domain")
+    need(type(grid) is int and grid > 0, "positive grid")
+    # Endpoint one has an exact direct certificate, rather than a lost top bit.
+    if numerator == 2**bits:
+        raise ValueError("unit exponent uses a direct bound")
+    previous, values = Q(1), []
+    for i in range(bits):
+        target = previous * (x if numerator >> i & 1 else 1)
+        a, b = target.numerator * grid**2, target.denominator
+        n = isqrt(a // b)
+        if n * n * b < a:
+            n += 1
+        values.append(n)
+        previous = Q(n, grid)
+    return values
+
+
+def propose(counts):
+    return {"schema": "bit-dyadic-moment/1", "grid": GRID, "numerator": NUMERATOR, "bits": BITS,
+            "exponent": fraction(EXPONENT), "base_denominator": 64,
+            "rows": [{"rank": r, "count": c, "upper_numerators": propose_chain(Q(r, 64), NUMERATOR, BITS, GRID)}
+                     for r, c in sorted(counts.items())]}
+
+
+def check(data, counts):
+    need(data["schema"] == "bit-dyadic-moment/1", "certificate schema")
+    need(type(data["grid"]) is int and data["grid"] == GRID, "certificate grid")
+    need(type(data["numerator"]) is int and data["numerator"] == NUMERATOR
+         and type(data["bits"]) is int and data["bits"] == BITS, "dyadic exponent binding")
+    need(data["exponent"] == fraction(EXPONENT) and type(data["base_denominator"]) is int
+         and data["base_denominator"] == 64, "selected real exponent and base")
+    need(Q(NUMERATOR, 2**BITS) <= EXPONENT, "exponent must round down")
+    need([(r["rank"], r["count"]) for r in data["rows"]] == sorted(counts.items()), "complete ordered profile")
+    uppers = {}
+    for row in data["rows"]:
+        rank, count = row["rank"], row["count"]
+        need(type(rank) is int and type(count) is int, "integer profile types")
+        values = row["upper_numerators"]
+        need(len(values) == BITS, "complete square chain")
+        previous, exponent = Q(1), Q(0)
+        for i, n in enumerate(values):
+            need(type(n) is int and 0 <= n <= GRID, "nonnegative bounded square root")
+            bit = NUMERATOR >> i & 1
+            target = previous * (Q(rank, 64) if bit else 1)
+            bound = Q(n, GRID)
+            need(target <= bound**2, "square certificate inequality")
+            previous, exponent = bound, (exponent + bit) / 2
+        need(exponent == Q(NUMERATOR, 2**BITS), "binary digit orientation")
+        uppers[rank] = previous
+    bad = Q(118606528512, 10**16 * 28416)
+    ordinary = sum((Q(count, 28416) * uppers[rank] for rank, count in counts.items()), Q(0))
+    total = ordinary + bad * uppers[1]
+    need(total < Q(9999, 10000), "full moment margin")
+    return {"square_steps": BITS * len(counts), "rounded_exponent": fraction(Q(NUMERATOR, 2**BITS)),
+            "exponent_gap": fraction(EXPONENT - Q(NUMERATOR, 2**BITS)),
+            "ordinary_upper": fraction(ordinary), "fallback_upper": fraction(bad * uppers[1]),
+            "moment_upper": fraction(total), "margin": fraction(Q(9999, 10000) - total),
+            "upper_numerators": {str(r): int(u * GRID) for r, u in uppers.items()}}
+
+
+def lean_fraction(q):
+    q = Q(q)
+    return str(q.numerator) if q.denominator == 1 else f"{q.numerator} / {q.denominator}"
+
+
+def render_lean(data, counts):
+    result = check(data, counts)
+    lines = ["import DyadicPower", "import Selected", "", "/-! Generated, untrusted certificate proposals; every inequality is proved by Lean.",
+             "Gareth Davidson with OpenAI Codex assistance. Apache-2.0. -/", "",
+             "open scoped BigOperators", "open DyadicPower SelectedStoppedRecurrence", "",
+             "namespace SelectedBitMoment", ""]
+    for row in data["rows"]:
+        rank, values = row["rank"], row["upper_numerators"]
+        base = f"({rank} / 64 : ℝ)"
+        lines.extend([f"theorem rank_{rank}_upper : {base} ^ (9983 / 10000 : ℝ) ≤ {values[-1]} / {GRID} := by",
+                      f"  have h0 : {base} ^ (0 : ℝ) ≤ 1 := by norm_num"])
+        previous, exponent = Q(1), Q(0)
+        for i, n in enumerate(values):
+            bit = NUMERATOR >> i & 1
+            next_exponent = (exponent + bit) / 2
+            lines.extend([f"  have h{i+1} : {base} ^ ({lean_fraction(next_exponent)} : ℝ) ≤ {n} / {GRID} := by",
+                          f"    convert half_step (x := {base}) (e := {lean_fraction(exponent)}) (b := {bit})",
+                          f"      (u := {'1' if i == 0 else str(values[i-1]) + ' / ' + str(GRID)}) (v := {n} / {GRID})",
+                          f"      (by norm_num) h{i} (by norm_num) (by norm_num) using 1; norm_num"])
+            previous, exponent = Q(n, GRID), next_exponent
+        lines.extend(["  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17", ""])
+    values = [row["upper_numerators"][-1] for row in data["rows"]]
+    lines.extend(["noncomputable def upper : Fin 8 → ℝ := ![" + ", ".join(f"{n} / {GRID}" for n in values) + "]", "",
+                  "theorem per_rank_upper : ∀ r, ((ranks r : ℝ) / 64) ^ exponent ≤ upper r := by",
+                  "  intro r", "  fin_cases r"])
+    for row in data["rows"]:
+        lines.append(f"  · simpa [ranks, exponent, upper] using rank_{row['rank']}_upper")
+    total = lean_fraction(Q(result["moment_upper"]))
+    lines.extend(["", f"theorem fractional_moment_upper : fractionalMoment ≤ {total} := by",
+                  "  calc", "    fractionalMoment ≤ (∑ r, weight r * upper r) + bad * upper 0 := by",
+                  "      unfold fractionalMoment", "      apply add_le_add",
+                  "      · exact Finset.sum_le_sum fun r _ => mul_le_mul_of_nonneg_left (per_rank_upper r) (by unfold weight; positivity)",
+                  "      · apply mul_le_mul_of_nonneg_left _ (by norm_num [bad])",
+                  "        simpa [exponent, upper] using rank_1_upper",
+                  f"    _ = {total} := by norm_num [Fin.sum_univ_succ, weight, counts, upper, bad]", "",
+                  "theorem fractional_moment_strict : fractionalMoment < 9999 / 10000 :=",
+                  "  lt_of_le_of_lt fractional_moment_upper (by norm_num)", "", "end SelectedBitMoment", ""])
+    lines.extend("#print axioms SelectedBitMoment." + name for name in
+                 [*(f"rank_{r}_upper" for r in sorted(counts)), "per_rank_upper", "fractional_moment_upper", "fractional_moment_strict"])
+    return "\n".join(lines) + "\n"
+
+
+def main():
+    import argparse
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--out-dir", type=Path, required=True, help="new directory for untrusted proposals")
+    args = parser.parse_args()
+    counts = profile()
+    data = propose(counts)
+    args.out_dir.mkdir(exist_ok=False, parents=True)
+    (args.out_dir / "DYADIC.json").write_text(json.dumps(data, indent=2) + "\n")
+    (args.out_dir / "SelectedMoment.lean").write_text(render_lean(data, counts))
+    print("PROPOSALS_ONLY_KERNEL_NOT_RUN", args.out_dir)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/research/lean-bit-moment-discharge/finite.py b/research/lean-bit-moment-discharge/finite.py
new file mode 100644
index 0000000000..a5752c1ce7
--- /dev/null
+++ b/research/lean-bit-moment-discharge/finite.py
@@ -0,0 +1,55 @@
+"""Independent exact-power controls and deterministic certificate replay.
+
+This does not execute Lean or claim that source checks are a kernel proof.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0.
+"""
+from pathlib import Path
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+import sys
+
+HERE = Path(__file__).resolve().parent
+sys.path.insert(0, str(HERE))
+from certificate import GRID, profile, propose, propose_chain, check, render_lean, need
+
+
+def calibration():
+    cases, digest = 0, sha256()
+    # Complete declared domain, tested against direct integer powers rather
+    # than another square-root implementation. The exact exponent-one endpoint
+    # is handled separately and is not silently truncated to its low bits.
+    for denominator in range(2, 13):
+        for numerator in range(1, denominator + 1):
+            x = Q(numerator, denominator)
+            for bits in range(1, 6):
+                for p in range(2**bits):
+                    ns = propose_chain(x, p, bits, GRID)
+                    upper = Q(ns[-1], GRID)
+                    need(x**p <= upper**(2**bits), "direct power calibration")
+                    digest.update(f"{numerator}/{denominator}:{p}/{2**bits}:{ns[-1]}\n".encode())
+                    cases += 1
+    return {"cases": cases, "domain": "1<=r<=m, 2<=m<=12, 1<=k<=5, 0<=p<2^k",
+            "trace_sha256": digest.hexdigest()}
+
+
+def replay(root=HERE):
+    counts = profile(root)
+    data = json.loads((root / "DYADIC.json").read_bytes())
+    result = check(data, counts)
+    need(data == propose(counts), "proposal replay")
+    need((root / "lean/SelectedMoment.lean").read_text() == render_lean(data, counts),
+         "Lean/certificate semantic binding")
+    # A second method checks each FINAL upper directly at the actual non-dyadic
+    # source exponent. It is not needed as a formal hypothesis of the Lean proof.
+    for rank, value in result["upper_numerators"].items():
+        need(pow(int(rank), 9983) * pow(GRID, 10000)
+             <= pow(value, 10000) * pow(64, 9983), "actual-exponent integer-power control")
+    return {"schema": "bit-moment-discharge-finite/1", "certificate": result,
+            "direct_actual_exponent_controls": len(counts), "calibration": calibration(),
+            "kernel_checked": False,
+            "scope": "Finite exact arithmetic and source-to-Lean binding only; explicit kernel mode builds the Real theorem."}
+
+
+if __name__ == "__main__":
+    print(json.dumps(replay(), indent=2))
diff --git a/research/lean-bit-moment-discharge/lean/ClosedRecurrence.lean b/research/lean-bit-moment-discharge/lean/ClosedRecurrence.lean
new file mode 100644
index 0000000000..45a49f0a7a
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/ClosedRecurrence.lean
@@ -0,0 +1,28 @@
+import SelectedMoment
+
+/-!
+Compose the newly proved numerical bound with PR2289's unchanged recurrence.
+The physical hypotheses remain visible; no full-machine admission is inferred.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0.
+-/
+
+open scoped BigOperators
+open SelectedStoppedRecurrence SelectedBitMoment
+
+namespace ClosedBitRecurrence
+
+/-- The root-family conclusion has no numerical moment hypothesis. -/
+theorem uniform_bound {Root : Type*} (limit : Root → ℕ) (w : Root → ℝ)
+    (C : ℝ) (hC : 0 ≤ C) (hw : ∀ root, 0 ≤ w root)
+    (T : Root → ℕ → ℝ) (one_nonnegative : ∀ root, 0 ≤ T root 1)
+    (leaf : ∀ root n, n ≤ limit root → 0 < n → n < 64 → T root n ≤ C * w root)
+    (step : ∀ root n, n ≤ limit root → ∀ (hn : 64 ≤ n), T root n ≤
+      (∑ r, weight r * T root (ranks r * (n / 64))) +
+      bad * positiveWorst (T root) (n / 64) (by omega) + C * (n + w root)) :
+    ∀ root n, n ≤ limit root → 0 < n →
+      T root n ≤ 200 * C * n + 10000 * C * (n : ℝ) ^ (9983 / 10000 : ℝ) * w root :=
+  selected_uniform_bound limit w C hC hw fractional_moment_strict.le T one_nonnegative leaf step
+
+end ClosedBitRecurrence
+
+#print axioms ClosedBitRecurrence.uniform_bound
diff --git a/research/lean-bit-moment-discharge/lean/DyadicPower.lean b/research/lean-bit-moment-discharge/lean/DyadicPower.lean
new file mode 100644
index 0000000000..c4f9581ec1
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/DyadicPower.lean
@@ -0,0 +1,45 @@
+import Mathlib
+
+/-!
+Rational square certificates for binary real-power enclosures.
+Certificate proposals are untrusted: every step is proved in the kernel.
+Gareth Davidson with substantial OpenAI Codex assistance. Apache-2.0.
+-/
+
+namespace DyadicPower
+
+/-- One binary digit transforms exponent e to (e+b)/2. Nonnegativity of the
+proposed bound is essential when passing from squares to ordered reals. -/
+theorem half_step {x e b u v : ℝ} (hx : 0 < x)
+    (previous : x ^ e ≤ u) (hv : 0 ≤ v)
+    (square : u * x ^ b ≤ v ^ 2) : x ^ ((e + b) / 2) ≤ v := by
+  apply (sq_le_sq₀ (Real.rpow_nonneg hx.le _) hv).mp
+  calc
+    (x ^ ((e + b) / 2)) ^ 2 = x ^ (e + b) := by
+      rw [← Real.rpow_natCast, ← Real.rpow_mul hx.le]
+      congr 1
+      norm_num
+    _ = x ^ e * x ^ b := Real.rpow_add hx e b
+    _ ≤ u * x ^ b := mul_le_mul_of_nonneg_right previous (Real.rpow_nonneg hx.le _)
+    _ ≤ v ^ 2 := square
+
+/-- For bases below one, rounding the exponent down gives an upper bound. -/
+theorem upper_of_rounded_exponent {x q t u : ℝ} (hx : 0 < x) (hx1 : x ≤ 1)
+    (hqt : q ≤ t) (bound : x ^ q ≤ u) : x ^ t ≤ u :=
+  (Real.rpow_le_rpow_of_exponent_ge hx hx1 hqt).trans bound
+
+theorem negative_square_is_not_upper :
+    (1 : ℝ) ≤ (-1 : ℝ) ^ 2 ∧ ¬ (1 : ℝ) ^ (1 / 2 : ℝ) ≤ -1 := by
+  norm_num
+
+theorem upward_exponent_is_not_upper :
+    (1 / 64 : ℝ) ^ (130850 / 131072 : ℝ) < (1 / 64 : ℝ) ^ (9983 / 10000 : ℝ) := by
+  exact (Real.rpow_lt_rpow_left_iff_of_base_lt_one (by norm_num) (by norm_num)).mpr
+    (by norm_num)
+
+end DyadicPower
+
+#print axioms DyadicPower.half_step
+#print axioms DyadicPower.upper_of_rounded_exponent
+#print axioms DyadicPower.negative_square_is_not_upper
+#print axioms DyadicPower.upward_exponent_is_not_upper
diff --git a/research/lean-bit-moment-discharge/lean/Selected.lean b/research/lean-bit-moment-discharge/lean/Selected.lean
new file mode 100644
index 0000000000..129c0b14ec
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/Selected.lean
@@ -0,0 +1,115 @@
+import StoppedRecurrence
+
+/-!
+Literal PR2234/selected-PR589 instantiation. The fractional moment inequality
+is retained as an explicit formal hypothesis; the recurrence theorem does not
+establish the full-machine local charge or completed-child contract.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0.
+-/
+
+open scoped BigOperators
+open StoppedRecurrence
+
+namespace SelectedStoppedRecurrence
+
+def ranks : Fin 8 → ℕ := ![1, 2, 3, 4, 5, 6, 7, 42]
+def counts : Fin 8 → ℕ := ![381024, 400416, 22752, 26880, 29376, 17376, 26784, 288]
+noncomputable def weight (r : Fin 8) : ℝ := counts r / 28416
+noncomputable def bad : ℝ := 118606528512 / (10000000000000000 * 28416)
+noncomputable def exponent : ℝ := 9983 / 10000
+
+noncomputable def fractionalMoment : ℝ :=
+  (∑ r, weight r * ((ranks r : ℝ) / 64) ^ exponent) + bad * (1 / 64) ^ exponent
+
+theorem proper_ranks : ∀ r, 0 < ranks r ∧ ranks r < 64 := by
+  intro r
+  fin_cases r <;> norm_num [ranks]
+
+theorem exact_linear_moment :
+    (∑ r, weight r * ((ranks r : ℝ) / 64)) + bad * (1 / 64) =
+      2874298095721977 / 2890625000000000 := by
+  norm_num [Fin.sum_univ_succ, weight, counts, ranks, bad]
+
+theorem linear_margin :
+    (∑ r, weight r * ((ranks r : ℝ) / 64)) + bad * (1 / 64) ≤ 199 / 200 := by
+  rw [exact_linear_moment]
+  norm_num
+
+theorem selected_bound (limit : ℕ) (C w : ℝ) (hC : 0 ≤ C) (hw : 0 ≤ w)
+    (fractional_margin : fractionalMoment ≤ 9999 / 10000)
+    (T : ℕ → ℝ) (zero : T 0 ≤ 0)
+    (leaf : ∀ n, n ≤ limit → 0 < n → n < 64 → T n ≤ C * w)
+    (step : ∀ n, n ≤ limit → 64 ≤ n → T n ≤
+      (∑ r, weight r * T (ranks r * (n / 64))) + bad * worst T (n / 64) + C * (n + w)) :
+    ∀ n, n ≤ limit → T n ≤ 200 * C * n + 10000 * C * (n : ℝ) ^ (9983 / 10000 : ℝ) * w := by
+  exact stopped_bound limit 64 (by decide) ranks proper_ranks weight
+    (fun r => by unfold weight; positivity) bad C w exponent
+    (by norm_num [bad]) hC hw (by norm_num [exponent]) linear_margin
+    fractional_margin T zero leaf step
+
+noncomputable def positiveWorst (T : ℕ → ℝ) (f : ℕ) (hf : 1 ≤ f) : ℝ :=
+  (Finset.Icc 1 f).sup' (by exact ⟨1, by simp [hf]⟩) T
+
+/-- A bookkeeping extension, not a constraint on the source's width-zero cost. -/
+noncomputable def zeroed (T : ℕ → ℝ) (n : ℕ) : ℝ := if n = 0 then 0 else T n
+
+theorem worst_zeroed (T : ℕ → ℝ) (f : ℕ) (hf : 1 ≤ f) (h1 : 0 ≤ T 1) :
+    worst (zeroed T) f = positiveWorst T f hf := by
+  rw [worst_eq_positive (zeroed T) f hf (by simpa [zeroed] using h1)]
+  apply Finset.sup'_congr (by exact ⟨1, by simp [hf]⟩) rfl
+  intro j hj
+  have hj0 : j ≠ 0 := by have := (Finset.mem_Icc.mp hj).1; omega
+  simp [zeroed, hj0]
+
+/-- The source's literal positive-width fallback maximum, not a hidden
+monotonicity assumption on `T`. Only its proved majorant is monotone.
+Width zero is outside the conclusion, as in PR2234, and `T 0` is unrestricted. -/
+theorem selected_positive_bound (limit : ℕ) (C w : ℝ) (hC : 0 ≤ C) (hw : 0 ≤ w)
+    (fractional_margin : fractionalMoment ≤ 9999 / 10000)
+    (T : ℕ → ℝ) (one_nonnegative : 0 ≤ T 1)
+    (leaf : ∀ n, n ≤ limit → 0 < n → n < 64 → T n ≤ C * w)
+    (step : ∀ n, n ≤ limit → ∀ (hn : 64 ≤ n), T n ≤
+      (∑ r, weight r * T (ranks r * (n / 64))) +
+      bad * positiveWorst T (n / 64) (by omega) + C * (n + w)) :
+    ∀ n, n ≤ limit → 0 < n → T n ≤ 200 * C * n + 10000 * C * (n : ℝ) ^ (9983 / 10000 : ℝ) * w := by
+  have leaves : ∀ n, n ≤ limit → 0 < n → n < 64 → zeroed T n ≤ C * w := by
+    intro n hnlimit hn hsmall
+    simpa only [zeroed, if_neg (Nat.ne_of_gt hn)] using leaf n hnlimit hn hsmall
+  have steps : ∀ n, n ≤ limit → 64 ≤ n → zeroed T n ≤
+      (∑ r, weight r * zeroed T (ranks r * (n / 64))) +
+      bad * worst (zeroed T) (n / 64) + C * (n + w) := by
+    intro n hnlimit hn
+    have hn0 : n ≠ 0 := by omega
+    have child_pos : ∀ r, ranks r * (n / 64) ≠ 0 := by
+      intro r
+      exact Nat.ne_of_gt (Nat.mul_pos (proper_ranks r).1 (by omega))
+    rw [worst_zeroed T (n / 64) (by omega) one_nonnegative]
+    simpa only [zeroed, hn0, child_pos, if_false] using step n hnlimit hn
+  have bound := selected_bound limit C w hC hw fractional_margin (zeroed T)
+    (by simp [zeroed]) leaves steps
+  intro n hnlimit hn
+  simpa only [zeroed, if_neg (Nat.ne_of_gt hn)] using bound n hnlimit
+
+/-- A single local-charge constant serves the whole root-indexed family.
+The allowed root width/atom-width pairs may be coupled; no recurrence is
+required outside each root's descendant-width domain. -/
+theorem selected_uniform_bound {Root : Type*} (limit : Root → ℕ) (w : Root → ℝ)
+    (C : ℝ) (hC : 0 ≤ C) (hw : ∀ root, 0 ≤ w root)
+    (fractional_margin : fractionalMoment ≤ 9999 / 10000)
+    (T : Root → ℕ → ℝ) (one_nonnegative : ∀ root, 0 ≤ T root 1)
+    (leaf : ∀ root n, n ≤ limit root → 0 < n → n < 64 → T root n ≤ C * w root)
+    (step : ∀ root n, n ≤ limit root → ∀ (hn : 64 ≤ n), T root n ≤
+      (∑ r, weight r * T root (ranks r * (n / 64))) +
+      bad * positiveWorst (T root) (n / 64) (by omega) + C * (n + w root)) :
+    ∀ root n, n ≤ limit root → 0 < n →
+      T root n ≤ 200 * C * n + 10000 * C * (n : ℝ) ^ (9983 / 10000 : ℝ) * w root := by
+  intro root
+  exact selected_positive_bound (limit root) C (w root) hC (hw root) fractional_margin
+    (T root) (one_nonnegative root) (leaf root) (step root)
+
+end SelectedStoppedRecurrence
+
+#print axioms SelectedStoppedRecurrence.exact_linear_moment
+#print axioms SelectedStoppedRecurrence.selected_bound
+#print axioms SelectedStoppedRecurrence.selected_positive_bound
+#print axioms SelectedStoppedRecurrence.selected_uniform_bound
diff --git a/research/lean-bit-moment-discharge/lean/SelectedMoment.lean b/research/lean-bit-moment-discharge/lean/SelectedMoment.lean
new file mode 100644
index 0000000000..da9ffba70f
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/SelectedMoment.lean
@@ -0,0 +1,627 @@
+import DyadicPower
+import Selected
+
+/-! Generated, untrusted certificate proposals; every inequality is proved by Lean.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0. -/
+
+open scoped BigOperators
+open DyadicPower SelectedStoppedRecurrence
+
+namespace SelectedBitMoment
+
+theorem rank_1_upper : (1 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 15735950448 / 1000000000000 := by
+  have h0 : (1 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (1 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 125000000000 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 125000000000 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (1 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 353553390594 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 125000000000 / 1000000000000) (v := 353553390594 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (1 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 594603557502 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 353553390594 / 1000000000000) (v := 594603557502 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (1 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 771105412705 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 594603557502 / 1000000000000) (v := 771105412705 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (1 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 878126080188 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 771105412705 / 1000000000000) (v := 878126080188 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (1 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 117135477132 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 878126080188 / 1000000000000) (v := 117135477132 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (1 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 342250605744 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 117135477132 / 1000000000000) (v := 342250605744 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (1 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 585021884842 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 342250605744 / 1000000000000) (v := 585021884842 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (1 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 95608404185 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 585021884842 / 1000000000000) (v := 95608404185 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (1 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 38650760865 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 95608404185 / 1000000000000) (v := 38650760865 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (1 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 24574745951 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 38650760865 / 1000000000000) (v := 24574745951 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (1 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 19595417972 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 24574745951 / 1000000000000) (v := 19595417972 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (1 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 17497954333 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 19595417972 / 1000000000000) (v := 17497954333 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (1 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 16534979180 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 17497954333 / 1000000000000) (v := 16534979180 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (1 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 16073551247 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 16534979180 / 1000000000000) (v := 16073551247 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (1 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 15847688735 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 16073551247 / 1000000000000) (v := 15847688735 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (1 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 15735950448 / 1000000000000 := by
+    convert half_step (x := (1 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 15847688735 / 1000000000000) (v := 15735950448 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_2_upper : (2 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 31434808292 / 1000000000000 := by
+  have h0 : (2 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (2 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 176776695297 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 176776695297 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (2 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 420448207628 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 176776695297 / 1000000000000) (v := 420448207628 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (2 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 648419777327 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 420448207628 / 1000000000000) (v := 648419777327 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (2 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 805245165976 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 648419777327 / 1000000000000) (v := 805245165976 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (2 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 897354537503 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 805245165976 / 1000000000000) (v := 897354537503 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (2 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 167458440507 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 897354537503 / 1000000000000) (v := 167458440507 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (2 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 409216862443 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 167458440507 / 1000000000000) (v := 409216862443 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (2 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 639700603754 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 409216862443 / 1000000000000) (v := 639700603754 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (2 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 141388273444 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 639700603754 / 1000000000000) (v := 141388273444 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (2 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 66470922554 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 141388273444 / 1000000000000) (v := 66470922554 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (2 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 45576488784 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 66470922554 / 1000000000000) (v := 45576488784 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (2 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 37739439245 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 45576488784 / 1000000000000) (v := 37739439245 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (2 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 34341774509 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 37739439245 / 1000000000000) (v := 34341774509 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (2 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 32759433045 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 34341774509 / 1000000000000) (v := 32759433045 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (2 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 31995816644 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 32759433045 / 1000000000000) (v := 31995816644 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (2 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 31620709514 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 31995816644 / 1000000000000) (v := 31620709514 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (2 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 31434808292 / 1000000000000 := by
+    convert half_step (x := (2 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 31620709514 / 1000000000000) (v := 31434808292 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_3_upper : (3 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 47119696168 / 1000000000000 := by
+  have h0 : (3 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (3 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 216506350947 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 216506350947 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (3 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 465302429553 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 216506350947 / 1000000000000) (v := 465302429553 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (3 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 682130800913 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 465302429553 / 1000000000000) (v := 682130800913 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (3 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 825912102414 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 682130800913 / 1000000000000) (v := 825912102414 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (3 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 908797063384 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 825912102414 / 1000000000000) (v := 908797063384 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (3 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 206397340938 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 908797063384 / 1000000000000) (v := 206397340938 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (3 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 454309741188 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 206397340938 / 1000000000000) (v := 454309741188 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (3 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 674025030091 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 454309741188 / 1000000000000) (v := 674025030091 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (3 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 177749608398 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 674025030091 / 1000000000000) (v := 177749608398 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (3 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 91279860286 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 177749608398 / 1000000000000) (v := 91279860286 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (3 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 65412104774 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 91279860286 / 1000000000000) (v := 65412104774 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (3 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 55373210231 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 65412104774 / 1000000000000) (v := 55373210231 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (3 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 50947220038 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 55373210231 / 1000000000000) (v := 50947220038 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (3 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 48868711251 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 50947220038 / 1000000000000) (v := 48868711251 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (3 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 47861475530 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 48868711251 / 1000000000000) (v := 47861475530 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (3 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 47365669694 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 47861475530 / 1000000000000) (v := 47365669694 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (3 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 47119696168 / 1000000000000 := by
+    convert half_step (x := (3 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 47365669694 / 1000000000000) (v := 47119696168 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_4_upper : (4 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 62795518809 / 1000000000000 := by
+  have h0 : (4 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (4 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 250000000000 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 250000000000 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (4 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 500000000000 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 250000000000 / 1000000000000) (v := 500000000000 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (4 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 707106781187 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 500000000000 / 1000000000000) (v := 707106781187 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (4 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 840896415254 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 707106781187 / 1000000000000) (v := 840896415254 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (4 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 917004043205 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 840896415254 / 1000000000000) (v := 917004043205 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (4 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 239400820175 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 917004043205 / 1000000000000) (v := 239400820175 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (4 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 489286031045 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 239400820175 / 1000000000000) (v := 489286031045 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (4 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 699489836270 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 489286031045 / 1000000000000) (v := 699489836270 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (4 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 209088772456 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 699489836270 / 1000000000000) (v := 209088772456 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (4 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 114315564464 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 209088772456 / 1000000000000) (v := 114315564464 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (4 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 84526462005 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 114315564464 / 1000000000000) (v := 84526462005 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (4 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 72683587387 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 84526462005 / 1000000000000) (v := 72683587387 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (4 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 67399734508 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 72683587387 / 1000000000000) (v := 67399734508 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (4 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 64903647099 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 67399734508 / 1000000000000) (v := 64903647099 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (4 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 63690485504 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 64903647099 / 1000000000000) (v := 63690485504 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (4 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 63092434919 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 63690485504 / 1000000000000) (v := 63092434919 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (4 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 62795518809 / 1000000000000 := by
+    convert half_step (x := (4 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 63092434919 / 1000000000000) (v := 62795518809 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_5_upper : (5 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 78464604053 / 1000000000000 := by
+  have h0 : (5 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (5 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 279508497188 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 279508497188 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (5 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 528685631721 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 279508497188 / 1000000000000) (v := 528685631721 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (5 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 727107716725 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 528685631721 / 1000000000000) (v := 727107716725 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (5 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 852706113925 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 727107716725 / 1000000000000) (v := 852706113925 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (5 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 923420875834 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 852706113925 / 1000000000000) (v := 923420875834 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (5 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 268593104760 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 923420875834 / 1000000000000) (v := 268593104760 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (5 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 518259688535 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 268593104760 / 1000000000000) (v := 518259688535 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (5 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 719902554889 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 518259688535 / 1000000000000) (v := 719902554889 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (5 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 237154774569 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 719902554889 / 1000000000000) (v := 237154774569 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (5 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 136116555802 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 237154774569 / 1000000000000) (v := 136116555802 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (5 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 103121801391 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 136116555802 / 1000000000000) (v := 103121801391 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (5 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 89757399326 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 103121801391 / 1000000000000) (v := 89757399326 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (5 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 83739457978 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 89757399326 / 1000000000000) (v := 83739457978 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (5 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 80883528327 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 83739457978 / 1000000000000) (v := 80883528327 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (5 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 79492299317 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 80883528327 / 1000000000000) (v := 79492299317 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (5 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 78805684340 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 79492299317 / 1000000000000) (v := 78805684340 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (5 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 78464604053 / 1000000000000 := by
+    convert half_step (x := (5 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 78805684340 / 1000000000000) (v := 78464604053 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_6_upper : (6 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 94128322322 / 1000000000000 := by
+  have h0 : (6 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (6 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 306186217848 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 306186217848 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (6 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 553340959851 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 306186217848 / 1000000000000) (v := 553340959851 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (6 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 743868913083 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 553340959851 / 1000000000000) (v := 743868913083 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (6 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 862478355139 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 743868913083 / 1000000000000) (v := 862478355139 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (6 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 928697127776 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 862478355139 / 1000000000000) (v := 928697127776 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (6 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 295068391613 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 928697127776 / 1000000000000) (v := 295068391613 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (6 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 543201980495 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 295068391613 / 1000000000000) (v := 543201980495 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (6 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 737022374488 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 543201980495 / 1000000000000) (v := 737022374488 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (6 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 262860890222 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 737022374488 / 1000000000000) (v := 262860890222 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (6 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 156981554517 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 262860890222 / 1000000000000) (v := 156981554517 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (6 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 121313728556 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 156981554517 / 1000000000000) (v := 121313728556 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (6 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 106645028258 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 121313728556 / 1000000000000) (v := 106645028258 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (6 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 99989856482 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 106645028258 / 1000000000000) (v := 99989856482 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (6 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 96819672822 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 99989856482 / 1000000000000) (v := 96819672822 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (6 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 95272474132 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 96819672822 / 1000000000000) (v := 95272474132 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (6 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 94508171340 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 95272474132 / 1000000000000) (v := 94508171340 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (6 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 94128322322 / 1000000000000 := by
+    convert half_step (x := (6 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 94508171340 / 1000000000000) (v := 94128322322 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_7_upper : (7 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 109787578824 / 1000000000000 := by
+  have h0 : (7 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (7 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 330718913884 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 330718913884 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (7 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 575081658449 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 330718913884 / 1000000000000) (v := 575081658449 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (7 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 758341386481 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 575081658449 / 1000000000000) (v := 758341386481 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (7 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 870827989032 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 758341386481 / 1000000000000) (v := 870827989032 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (7 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 933181648466 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 870827989032 / 1000000000000) (v := 933181648466 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (7 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 319478861275 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 933181648466 / 1000000000000) (v := 319478861275 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (7 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 565224611350 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 319478861275 / 1000000000000) (v := 565224611350 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (7 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 751814213321 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 565224611350 / 1000000000000) (v := 751814213321 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (7 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 286757178781 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 751814213321 / 1000000000000) (v := 286757178781 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (7 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 177099030007 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 286757178781 / 1000000000000) (v := 177099030007 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (7 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 139176888912 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 177099030007 / 1000000000000) (v := 139176888912 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (7 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 123379383306 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 139176888912 / 1000000000000) (v := 123379383306 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (7 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 116166346457 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 123379383306 / 1000000000000) (v := 116166346457 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (7 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 112719537543 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 116166346457 / 1000000000000) (v := 112719537543 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (7 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 111034676650 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 112719537543 / 1000000000000) (v := 111034676650 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (7 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 110201713955 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 111034676650 / 1000000000000) (v := 110201713955 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (7 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 109787578824 / 1000000000000 := by
+    convert half_step (x := (7 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 110201713955 / 1000000000000) (v := 109787578824 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+theorem rank_42_upper : (42 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ 656720459372 / 1000000000000 := by
+  have h0 : (42 / 64 : ℝ) ^ (0 : ℝ) ≤ 1 := by norm_num
+  have h1 : (42 / 64 : ℝ) ^ (1 / 2 : ℝ) ≤ 810092587301 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 0) (b := 1)
+      (u := 1) (v := 810092587301 / 1000000000000)
+      (by norm_num) h0 (by norm_num) (by norm_num) using 1; norm_num
+  have h2 : (42 / 64 : ℝ) ^ (1 / 4 : ℝ) ≤ 900051435920 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 1 / 2) (b := 0)
+      (u := 810092587301 / 1000000000000) (v := 900051435920 / 1000000000000)
+      (by norm_num) h1 (by norm_num) (by norm_num) using 1; norm_num
+  have h3 : (42 / 64 : ℝ) ^ (1 / 8 : ℝ) ≤ 948710406774 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 1 / 4) (b := 0)
+      (u := 900051435920 / 1000000000000) (v := 948710406774 / 1000000000000)
+      (by norm_num) h2 (by norm_num) (by norm_num) using 1; norm_num
+  have h4 : (42 / 64 : ℝ) ^ (1 / 16 : ℝ) ≤ 974017662455 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 1 / 8) (b := 0)
+      (u := 948710406774 / 1000000000000) (v := 974017662455 / 1000000000000)
+      (by norm_num) h3 (by norm_num) (by norm_num) using 1; norm_num
+  have h5 : (42 / 64 : ℝ) ^ (1 / 32 : ℝ) ≤ 986923331600 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 1 / 16) (b := 0)
+      (u := 974017662455 / 1000000000000) (v := 986923331600 / 1000000000000)
+      (by norm_num) h4 (by norm_num) (by norm_num) using 1; norm_num
+  have h6 : (42 / 64 : ℝ) ^ (33 / 64 : ℝ) ≤ 804778501430 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 1 / 32) (b := 1)
+      (u := 986923331600 / 1000000000000) (v := 804778501430 / 1000000000000)
+      (by norm_num) h5 (by norm_num) (by norm_num) using 1; norm_num
+  have h7 : (42 / 64 : ℝ) ^ (33 / 128 : ℝ) ≤ 897094477427 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 33 / 64) (b := 0)
+      (u := 804778501430 / 1000000000000) (v := 897094477427 / 1000000000000)
+      (by norm_num) h6 (by norm_num) (by norm_num) using 1; norm_num
+  have h8 : (42 / 64 : ℝ) ^ (33 / 256 : ℝ) ≤ 947150715265 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 33 / 128) (b := 0)
+      (u := 897094477427 / 1000000000000) (v := 947150715265 / 1000000000000)
+      (by norm_num) h7 (by norm_num) (by norm_num) using 1; norm_num
+  have h9 : (42 / 64 : ℝ) ^ (289 / 512 : ℝ) ≤ 788395622066 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 33 / 256) (b := 1)
+      (u := 947150715265 / 1000000000000) (v := 788395622066 / 1000000000000)
+      (by norm_num) h8 (by norm_num) (by norm_num) using 1; norm_num
+  have h10 : (42 / 64 : ℝ) ^ (801 / 1024 : ℝ) ≤ 719294534236 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 289 / 512) (b := 1)
+      (u := 788395622066 / 1000000000000) (v := 719294534236 / 1000000000000)
+      (by norm_num) h9 (by norm_num) (by norm_num) using 1; norm_num
+  have h11 : (42 / 64 : ℝ) ^ (1825 / 2048 : ℝ) ≤ 687049516478 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 801 / 1024) (b := 1)
+      (u := 719294534236 / 1000000000000) (v := 687049516478 / 1000000000000)
+      (by norm_num) h10 (by norm_num) (by norm_num) using 1; norm_num
+  have h12 : (42 / 64 : ℝ) ^ (3873 / 4096 : ℝ) ≤ 671473190224 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 1825 / 2048) (b := 1)
+      (u := 687049516478 / 1000000000000) (v := 671473190224 / 1000000000000)
+      (by norm_num) h11 (by norm_num) (by norm_num) using 1; norm_num
+  have h13 : (42 / 64 : ℝ) ^ (7969 / 8192 : ℝ) ≤ 663817957791 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 3873 / 4096) (b := 1)
+      (u := 671473190224 / 1000000000000) (v := 663817957791 / 1000000000000)
+      (by norm_num) h12 (by norm_num) (by norm_num) using 1; norm_num
+  have h14 : (42 / 64 : ℝ) ^ (16161 / 16384 : ℝ) ≤ 660023132020 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 7969 / 8192) (b := 1)
+      (u := 663817957791 / 1000000000000) (v := 660023132020 / 1000000000000)
+      (by norm_num) h13 (by norm_num) (by norm_num) using 1; norm_num
+  have h15 : (42 / 64 : ℝ) ^ (32545 / 32768 : ℝ) ≤ 658133862059 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 16161 / 16384) (b := 1)
+      (u := 660023132020 / 1000000000000) (v := 658133862059 / 1000000000000)
+      (by norm_num) h14 (by norm_num) (by norm_num) using 1; norm_num
+  have h16 : (42 / 64 : ℝ) ^ (65313 / 65536 : ℝ) ≤ 657191256011 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 32545 / 32768) (b := 1)
+      (u := 658133862059 / 1000000000000) (v := 657191256011 / 1000000000000)
+      (by norm_num) h15 (by norm_num) (by norm_num) using 1; norm_num
+  have h17 : (42 / 64 : ℝ) ^ (130849 / 131072 : ℝ) ≤ 656720459372 / 1000000000000 := by
+    convert half_step (x := (42 / 64 : ℝ)) (e := 65313 / 65536) (b := 1)
+      (u := 657191256011 / 1000000000000) (v := 656720459372 / 1000000000000)
+      (by norm_num) h16 (by norm_num) (by norm_num) using 1; norm_num
+  exact upper_of_rounded_exponent (by norm_num) (by norm_num) (by norm_num) h17
+
+noncomputable def upper : Fin 8 → ℝ := ![15735950448 / 1000000000000, 31434808292 / 1000000000000, 47119696168 / 1000000000000, 62795518809 / 1000000000000, 78464604053 / 1000000000000, 94128322322 / 1000000000000, 109787578824 / 1000000000000, 656720459372 / 1000000000000]
+
+theorem per_rank_upper : ∀ r, ((ranks r : ℝ) / 64) ^ exponent ≤ upper r := by
+  intro r
+  fin_cases r
+  · simpa [ranks, exponent, upper] using rank_1_upper
+  · simpa [ranks, exponent, upper] using rank_2_upper
+  · simpa [ranks, exponent, upper] using rank_3_upper
+  · simpa [ranks, exponent, upper] using rank_4_upper
+  · simpa [ranks, exponent, upper] using rank_5_upper
+  · simpa [ranks, exponent, upper] using rank_6_upper
+  · simpa [ranks, exponent, upper] using rank_7_upper
+  · simpa [ranks, exponent, upper] using rank_42_upper
+
+theorem fractional_moment_upper : fractionalMoment ≤ 11290320473664709188758299 / 11291503906250000000000000 := by
+  calc
+    fractionalMoment ≤ (∑ r, weight r * upper r) + bad * upper 0 := by
+      unfold fractionalMoment
+      apply add_le_add
+      · exact Finset.sum_le_sum fun r _ => mul_le_mul_of_nonneg_left (per_rank_upper r) (by unfold weight; positivity)
+      · apply mul_le_mul_of_nonneg_left _ (by norm_num [bad])
+        simpa [exponent, upper] using rank_1_upper
+    _ = 11290320473664709188758299 / 11291503906250000000000000 := by norm_num [Fin.sum_univ_succ, weight, counts, upper, bad]
+
+theorem fractional_moment_strict : fractionalMoment < 9999 / 10000 :=
+  lt_of_le_of_lt fractional_moment_upper (by norm_num)
+
+end SelectedBitMoment
+
+#print axioms SelectedBitMoment.rank_1_upper
+#print axioms SelectedBitMoment.rank_2_upper
+#print axioms SelectedBitMoment.rank_3_upper
+#print axioms SelectedBitMoment.rank_4_upper
+#print axioms SelectedBitMoment.rank_5_upper
+#print axioms SelectedBitMoment.rank_6_upper
+#print axioms SelectedBitMoment.rank_7_upper
+#print axioms SelectedBitMoment.rank_42_upper
+#print axioms SelectedBitMoment.per_rank_upper
+#print axioms SelectedBitMoment.fractional_moment_upper
+#print axioms SelectedBitMoment.fractional_moment_strict
diff --git a/research/lean-bit-moment-discharge/lean/StoppedRecurrence.lean b/research/lean-bit-moment-discharge/lean/StoppedRecurrence.lean
new file mode 100644
index 0000000000..034da5b718
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/StoppedRecurrence.lean
@@ -0,0 +1,157 @@
+import Mathlib
+
+/-!
+Independent formal audit of PR2234's stopped-recurrence implication.
+The recurrence and uniform local charge are hypotheses, not a formal proof of
+the complete recursive machine. The numerical margins are the predecessor's.
+Gareth Davidson with substantial OpenAI Codex assistance. Apache-2.0.
+-/
+
+open scoped BigOperators
+
+namespace StoppedRecurrence
+
+noncomputable def potential (C w τ x : ℝ) : ℝ :=
+  200 * C * x + 10000 * C * x ^ τ * w
+
+/-- Including width zero makes the maximum total. For nonnegative costs with
+zero cost at width zero, it equals the source's maximum on `1..f`. -/
+noncomputable def worst (T : ℕ → ℝ) (f : ℕ) : ℝ :=
+  (Finset.range (f + 1)).sup' (by simp) T
+
+theorem potential_mono {C w τ x y : ℝ}
+    (hC : 0 ≤ C) (hw : 0 ≤ w) (hτ : 0 ≤ τ) (hx : 0 ≤ x) (hxy : x ≤ y) :
+    potential C w τ x ≤ potential C w τ y := by
+  unfold potential
+  apply add_le_add
+  · exact mul_le_mul_of_nonneg_left hxy (by positivity)
+  · exact mul_le_mul_of_nonneg_right
+      (mul_le_mul_of_nonneg_left (Real.rpow_le_rpow hx hxy hτ) (by positivity)) hw
+
+theorem potential_scale {C w τ x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
+    potential C w τ (x * y) =
+      (200 * C * y) * x + (10000 * C * y ^ τ * w) * x ^ τ := by
+  unfold potential
+  rw [Real.mul_rpow hx hy]
+  ring
+
+/-- The source's literal positive-width fallback maximum agrees with `worst`.
+The separate condition on width zero cannot silently be dropped. -/
+theorem worst_eq_positive (T : ℕ → ℝ) (f : ℕ) (hf : 1 ≤ f)
+    (hzero : T 0 ≤ T 1) :
+    worst T f = (Finset.Icc 1 f).sup' (by exact ⟨1, by simp [hf]⟩) T := by
+  apply le_antisymm
+  · apply Finset.sup'_le
+    intro j hj
+    have hjf : j ≤ f := by simpa only [Finset.mem_range, Nat.lt_succ_iff] using hj
+    by_cases hj0 : j = 0
+    · subst j
+      exact hzero.trans (Finset.le_sup' T (by simp [hf]))
+    · exact Finset.le_sup' T (by simp; omega)
+  · apply Finset.sup'_le
+    intro j hj
+    exact Finset.le_sup' T (by simpa only [Finset.mem_range, Nat.lt_succ_iff] using
+      (Finset.mem_Icc.mp hj).2)
+
+/-- Quantified recurrence implication. All recursive calls have proper width;
+the two moment margins pay separately for `C*n` and `C*w`. -/
+theorem stopped_bound {R : Type*} [Fintype R]
+    (limit m : ℕ) (hm : 1 < m) (rank : R → ℕ)
+    (hrank : ∀ r, 0 < rank r ∧ rank r < m)
+    (a : R → ℝ) (ha : ∀ r, 0 ≤ a r) (b C w τ : ℝ)
+    (hb : 0 ≤ b) (hC : 0 ≤ C) (hw : 0 ≤ w) (hτ : 0 ≤ τ)
+    (linear : (∑ r, a r * ((rank r : ℝ) / m)) + b * (1 / m) ≤ 199 / 200)
+    (power : (∑ r, a r * ((rank r : ℝ) / m) ^ τ) + b * (1 / m) ^ τ ≤ 9999 / 10000)
+    (T : ℕ → ℝ) (zero : T 0 ≤ 0)
+    (leaf : ∀ n, n ≤ limit → 0 < n → n < m → T n ≤ C * w)
+    (step : ∀ n, n ≤ limit → m ≤ n → T n ≤
+      (∑ r, a r * T (rank r * (n / m))) + b * worst T (n / m) + C * (n + w)) :
+    ∀ n, n ≤ limit → T n ≤ potential C w τ n := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | h n ih =>
+    intro hnlimit
+    by_cases hn0 : n = 0
+    · subst n
+      exact zero.trans (by unfold potential; positivity)
+    have hn : 0 < n := by omega
+    have hnreal : (1 : ℝ) ≤ n := by exact_mod_cast hn
+    have hone : 1 ≤ (n : ℝ) ^ τ := Real.one_le_rpow hnreal hτ
+    by_cases hsmall : n < m
+    · apply (leaf n hnlimit hn hsmall).trans
+      unfold potential
+      have hcw : C * w ≤ C * (n : ℝ) ^ τ * w :=
+        mul_le_mul_of_nonneg_right (by nlinarith) hw
+      have hlin : 0 ≤ 200 * C * (n : ℝ) := by positivity
+      have hpow : 0 ≤ C * (n : ℝ) ^ τ * w := by positivity
+      nlinarith
+    have hmn : m ≤ n := by omega
+    have hmpos : 0 < (m : ℝ) := by exact_mod_cast (show 0 < m by omega)
+    have hf : 0 < n / m := Nat.div_pos hmn (by omega)
+    have hfn : n / m < n := Nat.div_lt_self hn hm
+    have hfloor : (m : ℝ) * (n / m : ℕ) ≤ n := by
+      exact_mod_cast Nat.mul_div_le n m
+    have hdiv : (n / m : ℕ) ≤ (n : ℝ) / m := (le_div_iff₀ hmpos).mpr (by nlinarith)
+    let A : ℝ := 200 * C * n
+    let B : ℝ := 10000 * C * (n : ℝ) ^ τ * w
+    have hA : 0 ≤ A := by dsimp [A]; positivity
+    have hB : 0 ≤ B := by dsimp [B]; positivity
+    have scaled (k : ℕ) (hk : k < n) (x : ℝ) (hx : 0 ≤ x)
+        (hkn : (k : ℝ) ≤ x * n) : T k ≤ A * x + B * x ^ τ := by
+      calc
+        T k ≤ potential C w τ k := ih k hk (le_trans hk.le hnlimit)
+        _ ≤ potential C w τ (x * n) := potential_mono hC hw hτ (by positivity) hkn
+        _ = A * x + B * x ^ τ := potential_scale hx (by positivity)
+    have children (r : R) : T (rank r * (n / m)) ≤
+        A * ((rank r : ℝ) / m) + B * ((rank r : ℝ) / m) ^ τ := by
+      apply scaled
+      · have hi := (hrank r).2
+        have hi' := Nat.mul_div_le n m
+        nlinarith
+      · positivity
+      · push_cast
+        calc
+          (rank r : ℝ) * (n / m : ℕ) ≤ (rank r : ℝ) * ((n : ℝ) / m) :=
+            mul_le_mul_of_nonneg_left hdiv (by positivity)
+          _ = (rank r : ℝ) / m * n := by ring
+    have fallback : worst T (n / m) ≤ A * (1 / m) + B * (1 / m) ^ τ := by
+      apply Finset.sup'_le
+      intro j hj
+      have hjf : j ≤ n / m := by simpa only [Finset.mem_range, Nat.lt_succ_iff] using hj
+      apply scaled j (lt_of_le_of_lt hjf hfn) (1 / m) (by positivity)
+      calc
+        (j : ℝ) ≤ (n / m : ℕ) := by exact_mod_cast hjf
+        _ ≤ (n : ℝ) / m := hdiv
+        _ = (1 / m) * n := by ring
+    have aggregate : T n ≤
+        A * ((∑ r, a r * ((rank r : ℝ) / m)) + b * (1 / m)) +
+        B * ((∑ r, a r * ((rank r : ℝ) / m) ^ τ) + b * (1 / m) ^ τ) + C * (n + w) := by
+      calc
+        T n ≤ (∑ r, a r * T (rank r * (n / m))) + b * worst T (n / m) + C * (n + w) := step n hnlimit hmn
+        _ ≤ (∑ r, a r * (A * ((rank r : ℝ) / m) + B * ((rank r : ℝ) / m) ^ τ)) +
+            b * (A * (1 / m) + B * (1 / m) ^ τ) + C * (n + w) := by
+          exact add_le_add (add_le_add
+            (Finset.sum_le_sum fun r _ => mul_le_mul_of_nonneg_left (children r) (ha r))
+            (mul_le_mul_of_nonneg_left fallback hb)) le_rfl
+        _ = _ := by
+          have expand : (∑ r, a r * (A * ((rank r : ℝ) / m) + B * ((rank r : ℝ) / m) ^ τ)) =
+              A * (∑ r, a r * ((rank r : ℝ) / m)) +
+              B * (∑ r, a r * ((rank r : ℝ) / m) ^ τ) := by
+            rw [Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib]
+            apply Finset.sum_congr rfl
+            intro r _
+            ring
+          rw [expand]
+          ring
+    have margins : T n ≤ A * (199 / 200) + B * (9999 / 10000) + C * (n + w) :=
+      aggregate.trans (by gcongr)
+    have saved : C * w ≤ C * (n : ℝ) ^ τ * w :=
+      mul_le_mul_of_nonneg_right (by nlinarith) hw
+    dsimp [A, B] at margins
+    unfold potential
+    nlinarith
+
+end StoppedRecurrence
+
+#print axioms StoppedRecurrence.worst_eq_positive
+#print axioms StoppedRecurrence.stopped_bound
diff --git a/research/lean-bit-moment-discharge/lean/lake-manifest.json b/research/lean-bit-moment-discharge/lean/lake-manifest.json
new file mode 100644
index 0000000000..d540e2038b
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/lake-manifest.json
@@ -0,0 +1,117 @@
+{
+  "version": "1.2.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/mathlib4.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "55b7917b472489c7c56a0fa6393af05cfd536599",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "55b7917b472489c7c56a0fa6393af05cfd536599",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.33.0-rc1",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "StoppedRecurrenceAudit",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}
diff --git a/research/lean-bit-moment-discharge/lean/lakefile.toml b/research/lean-bit-moment-discharge/lean/lakefile.toml
new file mode 100644
index 0000000000..61482da7b9
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/lakefile.toml
@@ -0,0 +1,22 @@
+name = "BitMomentDischarge"
+defaultTargets = ["ClosedRecurrence"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "55b7917b472489c7c56a0fa6393af05cfd536599"
+
+[[lean_lib]]
+name = "StoppedRecurrence"
+
+[[lean_lib]]
+name = "Selected"
+
+[[lean_lib]]
+name = "DyadicPower"
+
+[[lean_lib]]
+name = "SelectedMoment"
+
+[[lean_lib]]
+name = "ClosedRecurrence"
diff --git a/research/lean-bit-moment-discharge/lean/lean-toolchain b/research/lean-bit-moment-discharge/lean/lean-toolchain
new file mode 100644
index 0000000000..fd85b262bf
--- /dev/null
+++ b/research/lean-bit-moment-discharge/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.0-rc1
diff --git a/research/lean-bit-moment-discharge/sources/ASSEMBLY.json b/research/lean-bit-moment-discharge/sources/ASSEMBLY.json
new file mode 100644
index 0000000000..5fd676df06
--- /dev/null
+++ b/research/lean-bit-moment-discharge/sources/ASSEMBLY.json
@@ -0,0 +1,345 @@
+{
+  "status": "PASS_GAUGE44_NATIVE_EXACT_GLOBAL_ASSEMBLY",
+  "kappa": "836330098538459/500000000000000000",
+  "kappa_decimal": "0.001672660197076918",
+  "complex_lower": "67018507072324140917/40000000000000000000000",
+  "complex_decimal": "0.001675462676808103522925",
+  "bit_lower": "1733427039589844234749/1000000000000000000000000",
+  "bit_decimal": "0.001733427039589844234749",
+  "binding": "complex",
+  "gain_over_pr635_percent": "2.225753072846734155686237293080565286991751430561837568524869952894006",
+  "complex_profile": {
+    "1": 349604,
+    "2": 60192,
+    "3": 62585,
+    "4": 20448,
+    "5": 11808,
+    "7": 7,
+    "8": 1152,
+    "48": 4866
+  },
+  "provider_counts": {
+    "gauge44": 144
+  },
+  "surcharge_model": {
+    "complex": false,
+    "bit": true
+  },
+  "conservative_complex_lower": "1675462673946628390003/1000000000000000000000000",
+  "conservative_complex_decimal": "0.001675462673946628390003",
+  "conservative_kappa": "104541262139063/62500000000000000",
+  "conservative_kappa_decimal": "0.001672660194225008",
+  "conservative_moments": [
+    {
+      "side": "conservative_complex",
+      "surcharge": true,
+      "endpoint": "1675462673946628390003/1000000000000000000000000",
+      "accept": true,
+      "mercator": [
+        "-9477943787127246252114078401047446902088349/3369993333393829974333376885877453834204643052817571560137951281152",
+        "-37911775148508985008456313604189787608353395/13479973333575319897333507543509815336818572211270286240551805124608"
+      ],
+      "base_two": [
+        "-14062260903435109658771/5000000000000000000000000000000000000000000000",
+        "-28124511806870219317401/10000000000000000000000000000000000000000000000"
+      ]
+    },
+    {
+      "side": "conservative_complex",
+      "surcharge": true,
+      "endpoint": "418865668486657097501/250000000000000000000000",
+      "accept": false,
+      "mercator": [
+        "785122817737487251360323365382501180303679/6739986666787659948666753771754907668409286105635143120275902562304",
+        "1570245635474974502720646730765002360607359/13479973333575319897333507543509815336818572211270286240551805124608"
+      ],
+      "base_two": [
+        "29121704837234194839/250000000000000000000000000000000000000000000",
+        "1164878193489367793701/10000000000000000000000000000000000000000000000"
+      ]
+    }
+  ],
+  "conservative_bootstrap": [
+    {
+      "exponent": "1672719936901733723941013678754606046077578825189978511794824059037242793668975202328129659991/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "2742737044894666061983645782720007294031171810021488205175940962757206331024797671870340009/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "4785575320504"
+    },
+    {
+      "exponent": "1675458078593085218312040660818153764816233104573318346297481252562039366001553167060724596064338254398640072154860452679089426701487866530027/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "4595353543171690956663719172288555376892426681653702518747437960633998446832939275403935661745601359927845139547320910573298512133469973/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "1704765476910090189"
+    },
+    {
+      "exponent": "1675462666247285054830442970288416897030906497822964321770204104752241064441971590857087666732381866167177964126563572213205210286771447648612054886738219829723627595016989839870190733879919/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "7699343335172554354248909156340703499177035678229795895247758935558028409142912333267618133832822035873436427786794789713228552351387945113261780170276372404983010160129809266120081/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "607288598888548790921228"
+    },
+    {
+      "exponent": "1675462673933728427631015964717263684197943281973496759641273321854676680565638975150449678698528843599367004823064750102366777359345125457905262786558290059054631287442458769941662955873102918023405251635883578323072818311236251497950243/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "12899962371981359820062369173666715026503240358726678145323319434361024849550321301471156400632995176935249897633222640654874542094737213441709940945368712557541230058337044126897081976594748364116421676927181688763748502049757/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "216334415105865784879411203134"
+    },
+    {
+      "exponent": "1675462673946606776597547753757284468914397348111672791536762618650746006847119006092287439220975223568432626917668165205209921472872117804273807041934415238338810525338012084376652944279070588792188733715069029648364515985850564644058847673533039191645232667825478722147025414307379271/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "21613405449570780041584457212648888327208463237381349253993152880993907712560779024776431567373082331834794790078527127882195726192958065584761661189474661987915623347055720929411207811266284930970351635484014149435355941152326466960808354767332174521277852974585692620729/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "77064807811065157671403130893305387"
+    },
+    {
+      "exponent": "1675462673946628353790543236906837018994268067942761233727427353818691210464251050376758476302106776989352719214605910694555958443797426439860448154703028630733183575665927368014487684549879669285828463034853831749901954212088671168864170425089292905036474832925101921361968931044466640582512201309590690137287164584230136330974172187/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "36212454087630489034377341929057238766272572646181308789535748949623241523697893223010647280785394089305444041556202573560139551845296971369266816424334072631985512315450120330714171536965146168250098045787911328831135829574910707094963525167074898078638031068955533359417487798690409309862712835415769863669025827813/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "27452796172306184037585992127352896661365"
+    },
+    {
+      "exponent": "1675462673946628389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "60672615155830892504866159425812143481842807745708742390039720572742681899922994299723138147627539676157163558630049165342230540303990435022760921983655619602865954469864532501692650664396192418996918742426594989159115524057826701297449314614012679279474573170653301881712099856009097193307827108038289389824500519357700940684138332222665251616554008955511446561/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "9779509468522638102470520685957791421407368732"
+    }
+  ],
+  "conservative_outer": {
+    "bit_positive": "1675462673946628389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "complex_above_bit": "60675290618504839133256162425812143481842807745708742390039720572742681899922994299723138147627539676157163558630049165342230540303990435022760921983655619602865954469864532501692650664396192418996918742426594989159115524057826701297449314614012679279474573170653301881712099856009097193307827108038289389824500519357700940684138332222665251616554008955511446561/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "complex_below_one_over32": "29574537326053371609997/1000000000000000000000000",
+    "beta_positive": "1/1000000000000000000000000",
+    "beta_below_one": "999999999999999999999999/1000000000000000000000000",
+    "leaf_saving_above_bit": "60673615155830892504866159425812143481842807745708742390039720572742681899922994299723138147627539676157163558630049165342230540303990435022760921983655619602865954469864532501692650664396192418996918742426594989159115524057826701297449314614012679279474573170653301881712099856009097193307827108038289389824500519357700940684138332222665251616554008955511446561/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_positive": "837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_below_internal": "1675462673946628389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_below_leaf": "30338483040589392880823022037615453236082270616691945382876378443563595241219107110140996331131869915084282056176876955131439112988436587462215118761287505810997954474010282595226722466243626344965957678562633098387138765110170924053735498191482281813035989136012036928176770453431377943352031841919288685815056951851742432052679341610813268107336320339423500615248383445991044488553439/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "c_positive": "837731336973314194971285679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "c_below_one": "499162268663026685805028714320771926366195018023537615453236082270616691945382876378443563595241219107110140996331131869915084282056176876955131439112988436587462215118761287505810997954474010282595226722466243626344965957678562633098387138765110170924053735498191482281813035989136012036928176770453431377943352031841919288685815056951851742432052679341610813268107336320339423500615248383445991044488553439/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_below_reservations": "1/4000000000000000000000000",
+    "lambda_above_tau": "1675462673946628389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "lambda_above_sigma": "60676966081178785761646104750521524977003674489546316577896238729934936191180604260002565404945639753162863835491901537802554383140431804973595579753115315612430931708942548846073047798441722554464417049775930592966696527139084274702460155498488621452773275721338687869032820381435926540005945395938433380727307211530592902394748507722145893915613324817179223895748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "lambda_above_internal": "1675462673946628389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "lambda_prime_above_lambda": "1675462673946628389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "compact_leaf": "30338483040589392880823022037615453236082270616691945382876378443563595241219107110140996331131869915084282056176876955131439112988436587462215118761287505810997954474010282595226722466243626344965957678562633098387138765110170924053735498191482281813035989136012036928176770453431377943352031841919288685815056951851742432052679341610813268107336320339423500615248383445991044488553439/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "compact_reservations": "1/4000000000000000000000000",
+    "lambda_prime_below_one": "837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "epsilon_positive": "499999999999999999999999500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561",
+    "epsilon_below_one": "837731336973314194971660679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561",
+    "guard_width": "837731336973314194971660679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561",
+    "K_geometry": "375837731336973314194971285679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561000000000000000000000000",
+    "K_dominates_log": "837731336973314194971284841496736660490787005176705318690283924401331592232576857638707021450726275766237447232463371304022828084819454176738475971293619589414740012677825482625589507741108478692279088531710847665316637548159833145239206200847507638579362888947282828357888064599486154554105042582557758068684896334851164745562886400180099487236006473446138583635095732339918110198019723890329294934947176248383445991044488553439/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561000000000000000000000000",
+    "record_suffix": "837731336973314194971660679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561",
+    "phase_local": "6701850695786513559772784596093252097125660840538397146037708030084487974552442208533761854762192525995250472914540281898432853691581315490818402180374563477179234181348812941948603826423036500525692031268005463250554933798221401456529234845076311170203214401606906855666636140647401896056867649408538112465220673441416143944857487737217902462867251082170445706883741489963953605891281039768391983515073103248383445991044488553439/4006701850695786513559769285433824589070439855811699076374111341835066464436936988972451491238070247143118872029350945040679325743550584984358948487096092507300302279049909699953512016364207917739238186220270050989240272338571498935212902889879118632607570116014468141745495712086911903704574585836372548976453183745264645690513479544385186060543578565267113493855141309437284611995078012932432071644091572488000000000000000000000000",
+    "phase_boundary": "1340370139157302711954156249033580840773776191179136046748634562031316425002851030572568864305994811500152849433784249354972258851113328003659612503500557636937410941421052979138990735056702309135143055051964671858337062941022253286206922941781405084147121590032393459270066471117878932397198980310498931302673677229699591534073852229069054028004398868479650622770693940136264009828870693822734668241815112848383445991044488553439/801340370139157302711953857086764917814087971162339815274822268367013292887387397794490298247614049428623774405870189008135865148710116996871789697419218501460060455809981939990702403272841583547847637244054010197848054467714299787042580577975823726521514023202893628349099142417382380740914917167274509795290636749052929138102695908877037212108715713053422698771028261887456922399015602586486414328818314497600000000000000000000000",
+    "gamma_sublinear": "1/2000000000000000000000000",
+    "cell_above_band": "999999999999999999999998499162268663026685805028839320771926366195018023537615453236082270616691945382876378443563595241219107110140996331131869915084282056176876955131439112988436587462215118761287505810997954474010282595226722466243626344965957678562633098387138765110170924053735498191482281813035989136012036928176770453431377943352031841919288685815056951851742432052679341610813268107336320339423500615248383445991044488553439/2003350925347893256779884642716912294535219927905849538187055670917533232218468494486225745619035123571559436014675472520339662871775292492179474243548046253650151139524954849976756008182103958869619093110135025494620136169285749467606451444939559316303785058007234070872747856043455951852287292918186274488226591872632322845256739772192593030271789282633556746927570654718642305997539006466216035822045786244000000000000000000000000",
+    "prime_interval_packing": "837731336973314194971660679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561",
+    "alpha_positive": "1675462673946628389942820520724810294295768981764089865454201653784639646849700479195143426209507168656096450901331501388938546028642577221607036858305183001952524893916537976814591553267098196097052366065467221320350679869597200046852067435737336714525627390755800546544852075463474117625928272129126380125332864492931876059747829448328357055183327131835325315527759412000494609582771340444338250446393737248383445991044488553439/1001675462673946628389942321358456147267609963952924769093527835458766616109234247243112872809517561785779718007337736260169831435887646246089737121774023126825075569762477424988378004091051979434809546555067512747310068084642874733803225722469779658151892529003617035436373928021727975926143646459093137244113295936316161422628369886096296515135894641316778373463785327359321152998769503233108017911022893122000000000000000000000000",
+    "alpha_below_one": "999999999999999999999999500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561/1001675462673946628389942321358456147267609963952924769093527835458766616109234247243112872809517561785779718007337736260169831435887646246089737121774023126825075569762477424988378004091051979434809546555067512747310068084642874733803225722469779658151892529003617035436373928021727975926143646459093137244113295936316161422628369886096296515135894641316778373463785327359321152998769503233108017911022893122000000000000000000000000",
+    "alpha_below_one_fourth": "248743402994540028707542759818889226522606722006467102407927757210907014380458861331583074776169883277788833050933102563653519312943268984300827243585200598704316367546702818270279909469495896662605334272701410965507166341291121483403954363181707577823447504860148458312548629929968519863909983342644157930902991119586108479597344642075745771728790333197359268050418572427829793640109604467832666227309329543251616554008955511446561/1001675462673946628389942321358456147267609963952924769093527835458766616109234247243112872809517561785779718007337736260169831435887646246089737121774023126825075569762477424988378004091051979434809546555067512747310068084642874733803225722469779658151892529003617035436373928021727975926143646459093137244113295936316161422628369886096296515135894641316778373463785327359321152998769503233108017911022893122000000000000000000000000",
+    "delta_positive": "1/8000000000000000000000000",
+    "delta_below_one_eighth": "999999999999999999999999/8000000000000000000000000",
+    "short_record_fallback": "499160865075440791612030839141788690924313551030703512359372709471704575676772232577248094260989590037124504420170767295913424395564055810616345848851484588498495175856013482386559165475957975482129857812683169917049954841730039197886969440433134408492287411163213241915241893218288769289749867046000978510649085546885466934071333612987355001884424573153735198140914060592289673183685157704266276297823882807293425672956078579891508733380331018934747653825458606878394857095709300967766342628398188061433053411250283018550645637717355055870511629895689026320730284519098577019400372566147845856229282283208382297047707332277635636080477329802927434434911917397449496552209987061104759599326402594219284685820997872598597672318472668203165761779861005463966059247505832169126857485094758726721/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "small_field_exposure": "1/1000000000000000000000000",
+    "artificial_boundary": "28053614805566292108478159785983790723483461431407074648677111636095477644882649552071365118054486140996321840904116774601777284617981690881475978151515893889871787367004960260662786368527017985630042972329166544491891330922891824082972344084135076025172661632954328838633452924534088735062149841251872424403589359177586854163813702525025392958590762464691737095285903179340238871128184299137447612134462078058254849662026866534339683/4006701850695786513559769285433824589070439855811699076374111341835066464436936988972451491238070247143118872029350945040679325743550584984358948487096092507300302279049909699953512016364207917739238186220270050989240272338571498935212902889879118632607570116014468141745495712086911903704574585836372548976453183745264645690513479544385186060543578565267113493855141309437284611995078012932432071644091572488000000000000000000000000",
+    "literal_scalar_guard": "1",
+    "row_product_gap": "23971789/25",
+    "balanced_prefix_above_kappa": "2226550473268848047591768981247454579988104071528736217216604556349070533969263077329737024694750709563249371306397463241431971338498982128353241339380412573780475242829435083727484830774531058228243510071063000960333606144278249066762170330727039178281661627209910710903733835291494167953250660523509999247681949190104130051652348636356006036022468189794675561323369113127340521818044091436187211724887657/31302358208560832137185697542451754602112811373528899034172744858086456753413570226347277275297423805805616187729304258130307232371488945190304285055438222713283611555077419530886812627845374357337798329845859773353439627645089835431350803827180614317246641531363032357386685250678999247691988951846660538878540498009880044457136558940509266097996707541149324170743291479978786031211546976034625559719465410062500000000000000",
+    "coordinate_movement_above_kappa": "2802479721620389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "compact_phase_layer_above_kappa": "35624306734570231788154108728798594051736031339477803013081126137667399160200154620152170838679606594231097051043355742994781456500265770230528816561525714168924191347486080100927263103390451405662178756363730481608964043274409663630827823678771391962677510089094069565942023177699895823264047496552930441394289130393697922745726263996753048428101923089394150591987173917373768688512206078227378833589247000553439/500837731336973314194971160679228073633804981976462384546763917729383308054617123621556436404758780892889859003668868130084915717943823123044868560887011563412537784881238712494189002045525989717404773277533756373655034042321437366901612861234889829075946264501808517718186964010863987963071823229546568622056647968158080711314184943048148257567947320658389186731892663679660576499384751616554008955511446561000000000000000000000000",
+    "bulk_exposure_above_kappa": "2802479721620389942324709381495160866743837574187856518157192254291257609960279427257318100077005700276861852372460323842836441369950834657769459696009564977239078016344380397134045530135467498307349335603807581003081257573405010840884475942173298702550685385987320720525426829346698118287900143990902806692172891961710610175499480642299059315861667777334748383445991044488553439/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "Gaussian_arithmetic_above_kappa": "56999191277951173045035090948774158019621830426153670698360529878618476286305080162517646275749213406038291015584771390112528381349855998662719933419577674877216753678648656904711117478825949564653316453045935290828166662259480854671744658853750968074181461710309212390617867996498239835615253837578626434172035842618697571241588810905770706373917617711423035980691517403396237697965429356014776066148168507753439/801340370139157302711953857086764917814087971162339815274822268367013292887387397794490298247614049428623774405870189008135865148710116996871789697419218501460060455809981939990702403272841583547847637244054010197848054467714299787042580577975823726521514023202893628349099142417382380740914917167274509795290636749052929138102695908877037212108715713053422698771028261887456922399015602586486414328818314497600000000000000000000000",
+    "scalar_work_above_kappa": "284997959740681213118432234628513507010403687350696259341340836448763298964757619281082717604491686065315026637359871626035162246412151768606091846572131922432337418544382809478405564150137929927225451884322786589166327931433573559108190900720199779930223612336604069187160212730347242634028121475186050357134667439685360488530789311268625724462618360346397813460204514587635907132133144319080346546776664584553439/4006701850695786513559769285433824589070439855811699076374111341835066464436936988972451491238070247143118872029350945040679325743550584984358948487096092507300302279049909699953512016364207917739238186220270050989240272338571498935212902889879118632607570116014468141745495712086911903704574585836372548976453183745264645690513479544385186060543578565267113493855141309437284611995078012932432071644091572488000000000000000000000000",
+    "dimension_above_kappa": "31197641791439167865040790430817093445478957607718555545815359213442279463803034330001793258671839271524120836965446451432942138934908518051127686283060759415069629784302993042893662614984060726389686500928671284874803882425973165528982802317097634749515528799364006820894976376530911463211744883444833629074710162513629954790545390249594863953655641095206681865279176709815889530111822137092714962098578681373687211724887657/31302358208560832137185697542451754602112811373528899034172744858086456753413570226347277275297423805805616187729304258130307232371488945190304285055438222713283611555077419530886812627845374357337798329845859773353439627645089835431350803827180614317246641531363032357386685250678999247691988951846660538878540498009880044457136558940509266097996707541149324170743291479978786031211546976034625559719465410062500000000000000"
+  },
+  "conservative_controls": [
+    "next_grid",
+    "zero_eta",
+    "zero_beta",
+    "unit_beta"
+  ],
+  "model_controls": [
+    "native_complex_endpoint_rejected_with_old_surcharge",
+    "omitting_bit_surcharge_would_fail_next_endpoint_rejection"
+  ],
+  "native_correction_gain": "2.85191E-12",
+  "template_sha256": "9c4c51425251389ee9a747c465814cd07c64812c15b7aeef704dad7d65395a74",
+  "input_sha256": {
+    "owner_audit": "30bafff060afcfb3644e951214d66cfaffe58242881c652e28003958b42127cc",
+    "fresh_invoice": "212cf4ee3b16081bf66f300fa18b4070d25c17210c21c78c2967892c91870d12",
+    "package:inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4",
+    "engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482",
+    "engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098",
+    "engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c"
+  },
+  "bit_supplier": {
+    "pr": 589,
+    "repository": "CrocSwap/integer-mult-bounds",
+    "commit": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46",
+    "merged_as": "b3eb785ac5b4b1ca2beea0f80db078a505626a90",
+    "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+    "git_blob_sha1": "e293ddc557742637f9f679f083a1a282d87b1b13",
+    "word": {
+      "v": 111,
+      "decoder_constant": 63,
+      "copy_ranks": [
+        7,
+        7,
+        7,
+        7,
+        7,
+        7,
+        7,
+        7,
+        7
+      ]
+    },
+    "derived_deficit": 10272,
+    "deficit_formula": "T(2Kv-L*cst), L=9 T=32 K=4 M=64",
+    "replay_scope": "Cited unchanged supplier; this assembly reprices its full profile and does not rebuild its bit circuit."
+  },
+  "moments": [
+    {
+      "side": "bit",
+      "surcharge": true,
+      "endpoint": "1733427039589844234749/1000000000000000000000000",
+      "accept": true,
+      "mercator": [
+        "-43100600330766044577088869872467188970742291/26959946667150639794667015087019630673637144422540572481103610249216",
+        "-43100600330766044577088869872467188970742289/26959946667150639794667015087019630673637144422540572481103610249216"
+      ],
+      "base_two": [
+        "-799345163337715793503/500000000000000000000000000000000000000000000",
+        "-3197378653350863173989/2000000000000000000000000000000000000000000000"
+      ]
+    },
+    {
+      "side": "bit",
+      "surcharge": true,
+      "endpoint": "6933708158359376939/4000000000000000000000",
+      "accept": false,
+      "mercator": [
+        "22502934905675809315035333485365686073718547/13479973333575319897333507543509815336818572211270286240551805124608",
+        "5625733726418952328758833371341421518429637/3369993333393829974333376885877453834204643052817571560137951281152"
+      ],
+      "base_two": [
+        "8346798366759439729359/5000000000000000000000000000000000000000000000",
+        "16693606733518879458833/10000000000000000000000000000000000000000000000"
+      ]
+    },
+    {
+      "side": "complex",
+      "surcharge": false,
+      "endpoint": "67018507072324140917/40000000000000000000000",
+      "accept": true,
+      "mercator": [
+        "-35161575700336957412970835679936878918177631/26959946667150639794667015087019630673637144422540572481103610249216",
+        "-35161575700336957412970835679936878918177629/26959946667150639794667015087019630673637144422540572481103610249216"
+      ],
+      "base_two": [
+        "-163027/125000000000000000000000000000",
+        "-260843/200000000000000000000000000000"
+      ]
+    },
+    {
+      "side": "complex",
+      "surcharge": false,
+      "endpoint": "837731338404051761463/500000000000000000000000",
+      "accept": false,
+      "mercator": [
+        "43802465867485534890178553907434323023222757/26959946667150639794667015087019630673637144422540572481103610249216",
+        "43802465867485534890178553907434323023222759/26959946667150639794667015087019630673637144422540572481103610249216"
+      ],
+      "base_two": [
+        "1624723/1000000000000000000000000000000",
+        "406181/250000000000000000000000000000"
+      ]
+    }
+  ],
+  "bootstrap": [
+    {
+      "exponent": "2676351903605968510955225199374139336419692211991205809803291212685832779316802617926399111/1600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "4388379286997125724770519885577770614671108008794190196708787314167220683197382073600889/1600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "4785575287428"
+    },
+    {
+      "exponent": "107229317213090343809558513333591284579279399862953574758040118663735837979673222607810293919010512865815663359806135729869323361652475213/64000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "294102628281657641315436797399702095132937046425241959881336264162020326777392189706080989487134184336640193864270130676638347524787/64000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "1704765459304159860"
+    },
+    {
+      "exponent": "4289184432918425945204602612810811814242177218571549743614845366342624240747502661971213062645949901457815846541829576632569723585538319837683356531863935997754461046639237713138409679/2560000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "19710319073483390538004735557012804093428450256385154633657375759252497338028786937354050098542184153458170423367430276414461680162316643468136064002245538953360762286861590321/2560000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "607288590542446415285737"
+    },
+    {
+      "exponent": "171567378103828844589295714015277247208277763194683861086506039620411038425241223225415374750246673707197993416981116984785025248834072957802186876854129419662928338294140179682651151779349930844098048754952574172587583050727264357/102400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "1320956158224012017344647641921489285316138913493960379588961574758776774584625249753326292802006583018883015214974751165927042197813123145870580337071661705859820317348848220650069155901951245047425827412416949272735643/102400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "216334411393790970429839007220"
+    },
+    {
+      "exponent": "6862695124205903501391156875228590725366338670593798130778146011247213048799329248276386353883527829505727811814785950491330293597981298780354995034957137345602662361138997814404555486275586374750298102671091066436586235588225737165500314750679738457912869234305574310420604631/4096000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "88528509632166076285068641631428606201869221853988752786951200670751723613646116472170494272188185214049508669706402018701219645004965042862654397337638861002185595444513724413625249701897328908933563413764411774262834499685249320261542087130765694425689579395369/4096000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "77064806225479172206224871399132079"
+    },
+    {
+      "exponent": "274507804968239675262983012766557017278150386312268407171634736048569145063436078292308834161068093358180970305987390168436997280846699807340390028600235262791714958423212022381294505311826715320340799973882750272976631732616603410592302985180390981719778700426281993988599893959139653519462414098149103287619172127213213373/163840000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "5933048548885638014482168417655731592828365263951430854936563921707691165838931906641819029694012609831563002719153300192659609971399764737208285041576787977618705494688173284679659200026117249727023368267383396589407697014819609018280221299573718006011400106040860346480537585901850896712380827872786786627/163840000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "27452795513701194724472919763925196307643"
+    },
+    {
+      "exponent": "10980312198729587247443638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "gap": "397624056133934612790045917604701917406215620419844115427082799655527875330373276202813015439178645161780564981523433953754464728175629739795987771170132335610054962043286727909210625262956284518441881092272459809674959821447510830927360669573314438695315588844257812872604553551784716471645774666643540006532795343845359798288152210341205493240883041/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+      "cutoff_log2": "9779509200503493187646549135972282547372018449"
+    }
+  ],
+  "outer": {
+    "bit_positive": "10980312198729587247443638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "complex_above_bit": "397641590046133342377293758884701917406215620419844115427082799655527875330373276202813015439178645161780564981523433953754464728175629739795987771170132335610054962043286727909210625262956284518441881092272459809674959821447510830927360669573314438695315588844257812872604553551784716471645774666643540006532795343845359798288152210341205493240883041/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "complex_below_one_over32": "1182981492927675859083/40000000000000000000000",
+    "beta_positive": "1/1000000000000000000000000",
+    "beta_below_one": "999999999999999999999999/1000000000000000000000000",
+    "leaf_saving_above_bit": "397630609733934612790045917604701917406215620419844115427082799655527875330373276202813015439178645161780564981523433953754464728175629739795987771170132335610054962043286727909210625262956284518441881092272459809674959821447510830927360669573314438695315588844257812872604553551784716471645774666643540006532795343845359798288152210341205493240883041/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_positive": "5490156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_below_internal": "10980312198729587247443638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_below_leaf": "198826285179166035982270402440760912569765432916163173011623993612143517821071211018606852191713992207614079677746277798232070583522833346464040131120337992175287685033872193822269702576516098972493031335510966948552961468842663143003870659826835771836826867061459333121863581460303513978010014728768218218549926026148013255604069572375258901260643232347789658794506759116959/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "c_positive": "5490156099364793623722627424664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "c_below_one": "3271309843900635206376277372575335265400775894323080760912569765432916163173011623993612143517821071211018606852191713992207614079677746277798232070583522833346464040131120337992175287685033872193822269702576516098972493031335510966948552961468842663143003870659826835771836826867061459333121863581460303513978010014728768218218549926026148013255604069572375258901260643232347789658794506759116959/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "q_below_reservations": "1/4000000000000000000000000",
+    "lambda_above_tau": "10980312198729587247443638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "lambda_above_sigma": "397652570358332071964541202523111871272873243126085230725165393439907455486257849120013359911303314788504362168507994775109302947610648216362034016705404159980315166055515557776875015207994241231713971881647196853390441379566418558467550994613492991184484661483588239558165858236195872213832902062089988221816323698070693154748145677545861647881084752847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "lambda_above_internal": "10980312198729587247443638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "lambda_prime_above_lambda": "10980312198729587247443638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "compact_leaf": "198826285179166035982270402440760912569765432916163173011623993612143517821071211018606852191713992207614079677746277798232070583522833346464040131120337992175287685033872193822269702576516098972493031335510966948552961468842663143003870659826835771836826867061459333121863581460303513978010014728768218218549926026148013255604069572375258901260643232347789658794506759116959/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "compact_reservations": "1/4000000000000000000000000",
+    "lambda_prime_below_one": "5490156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3276800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "epsilon_positive": "3276799999999999999999996723200000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041",
+    "epsilon_below_one": "5490156099364793623725085024664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041",
+    "guard_width": "5490156099364793623725085024664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041",
+    "K_geometry": "2463090156099364793623722627424664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041000000000000000000000000",
+    "K_dominates_log": "5490156099364793623722621934508635234430481954291814422695635342978159907749288576153289398342101800605386759951803828863596938929105913915760137030556844399813758100950245530658058779006258926515722472711168934899700790934191609567546011024188672367963077893134633070826316136809200493713908255366563547481323107134813242084964051983866715512614148977550767246752612371721782716464394501526273347789658794506759116959/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041000000000000000000000000",
+    "record_suffix": "5490156099364793623725085024664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041",
+    "phase_local": "43921248794918348989797397907161777428999221693545688034707277312565017696667920620868284773594603323475138794609805883410298381184881969328135642945897010974565477183107879585431044983769153569759834554675556242092249571585614840927675280742290030366935983274346782667968528067378985161860863185144438949635253004033435714555114569800830622723385661970923954937928109745287255104902847187707560347789658794506759116959/26258321248794918348989774465797317876793792845415353912699441876536670694615907008051102851857431430311851145182466288062339087362578029777614143435331817333228287678951037296062597698519729022449421842379387871208220055749315912264411576308249258694855969034721385313825305385063508325335025091348317571888175919882169854254251600591790815893955167443420997928789914854141217682729643945927064328000000000000000000000000",
+    "phase_boundary": "8784249758983669797956853749307475993964945361262557875153776083228462003942314179986003287649459073994222648636775433539028491122458147236820894680443144391935334022278042735352886167985935610222360651165259275516204972132885029398414234142883074482160755497238531607724220016572324893840790106490381439094517098297552311153834096368177907559251707234125611905996226432313108921187690446056097947789658794506759116959/5251664249758983669797954893159463575358758569083070782539888375307334138923181401610220570371486286062370229036493257612467817472515605955522828687066363466645657535790207459212519539703945804489884368475877574241644011149863182452882315261649851738971193806944277062765061077012701665067005018269663514377635183976433970850850320118358163178791033488684199585757982970828243536545928789185412865600000000000000000000000",
+    "gamma_sublinear": "1/2000000000000000000000000",
+    "cell_above_band": "6553599999999999999999990164109843900635206376278191775335265400775894323080760912569765432916163173011623993612143517821071211018606852191713992207614079677746277798232070583522833346464040131120337992175287685033872193822269702576516098972493031335510966948552961468842663143003870659826835771836826867061459333121863581460303513978010014728768218218549926026148013255604069572375258901260643232347789658794506759116959/13129160624397459174494887232898658938396896422707676956349720938268335347307953504025551425928715715155925572591233144031169543681289014888807071717665908666614143839475518648031298849259864511224710921189693935604110027874657956132205788154124629347427984517360692656912652692531754162667512545674158785944087959941084927127125800295895407946977583721710498964394957427070608841364821972963532164000000000000000000000000",
+    "prime_interval_packing": "5490156099364793623725085024664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041",
+    "alpha_positive": "10980312198729587247446887759173369833654587632030253510125869910061996734737664582541145880521030589586779907760089836655982859251359636117528066447034011053349717969829907538482771093972386732693452770134652835927207759598680642618993049555346009224959207233307797298989489269747741160592044673906260033503313092406045023866414125957718702257010079405175508345491969139373993057669887742409314347789658794506759116959/6564580312198729587247443616449329469198448211353838478174860469134167673653976752012775712964357857577962786295616572015584771840644507444403535858832954333307071919737759324015649424629932255612355460594846967802055013937328978066102894077062314673713992258680346328456326346265877081333756272837079392972043979970542463563562900147947703973488791860855249482197478713535304420682410986481766082000000000000000000000000",
+    "alpha_below_one": "6553599999999999999999996728690156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041/6564580312198729587247443616449329469198448211353838478174860469134167673653976752012775712964357857577962786295616572015584771840644507444403535858832954333307071919737759324015649424629932255612355460594846967802055013937328978066102894077062314673713992258680346328456326346265877081333756272837079392972043979970542463563562900147947703973488791860855249482197478713535304420682410986481766082000000000000000000000000",
+    "alpha_below_one_fourth": "1630164765850952809564414016353158997465957465206429366033589247373479921678756523420652782360568433804903916666144053167240210100909767224983355898261204572273418261964609923465429585063510677170395412378577089114586545724733563873906730469710232659203538857436778784815092097296721529172847023535363588209507681900229570867024310911029207291115187885808636862203877709244452112112932858878032206152210341205493240883041/6564580312198729587247443616449329469198448211353838478174860469134167673653976752012775712964357857577962786295616572015584771840644507444403535858832954333307071919737759324015649424629932255612355460594846967802055013937328978066102894077062314673713992258680346328456326346265877081333756272837079392972043979970542463563562900147947703973488791860855249482197478713535304420682410986481766082000000000000000000000000",
+    "delta_positive": "1/8000000000000000000000000",
+    "delta_below_one_eighth": "999999999999999999999999/8000000000000000000000000",
+    "short_record_fallback": "21438795909359212103616200334166424291758762958701354720819225409175913045478560967720640553831252868642841942253167261842634503755898200369741797654839235623990958395123196106347054256327521388059237907738555946116433881290788510172566978075812588267011140451521149354923953941516451675932972669173688634010916300353904340905724906488218546839456978701394526050828652398406301750429825860648483042370608582747954568848698913366833278528173238328138005355037693658990720351480360064483574940413515507656771079955155236699697879613531021952974589189172911760811581583760662741175548267502730611041487528161453816002373253929599277616955065382186662816403849986402330301408647863401260251417675068508475184504597426026825094537163396209229472942008595502577513065441407681/21510816767012797111492423242381162804669475098964257925283382785258840633029351020995463456241607827711468458133476383180668180367423921993821506302223824759380613266596689752934480034627362015190566373277194544093773869669839595327005963311717792722826009833243758849085690171444026020114452554832541754890793713567473544605082911204795036380328073169650481503264698248512485525692124320503451097497600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "small_field_exposure": "1/1000000000000000000000000",
+    "artificial_boundary": "183852169990359346791918231787649011312444723634488255975589738809965682587684973326699526516110961923459937180623299751035499065844803681645771170859812299632587468036912086617932281548765711786234360762509239914564143864527718190385744313548514975552314851432112198104074453651496454623199693415276059973921029359691768089653102262800296482965336684891718205351875279066317532744711374863634584926956631023616479722649123/26258321248794918348989774465797317876793792845415353912699441876536670694615907008051102851857431430311851145182466288062339087362578029777614143435331817333228287678951037296062597698519729022449421842379387871208220055749315912264411576308249258694855969034721385313825305385063508325335025091348317571888175919882169854254251600591790815893955167443420997928789914854141217682729643945927064328000000000000000000000000",
+    "literal_scalar_guard": "1",
+    "row_product_gap": "23971789/25",
+    "balanced_prefix_above_kappa": "1081110357609925260614972695003107315707432353068338487603991699409949621702495690156909535160235873839601108223405260050123543294943053402137660198994397070489620108165140795187785639656314293544597085375410582291108751565224554246715990585636803213137497296463685876362653172078415927035174159499690912068352607880037991076665304643497436633279437216679436871538992416375313119280028939340626181/1641145078049682396811860904112332367299612052838459619543715117283541918413494188003193928241089464394490696573904143003896192960161126861100883964708238583326767979934439831003912356157483063903088865148711741950513753484332244516525723519265578668428498064670086582114081586566469270333439068209269848243010994992635615890890725036986925993372197965213812370549369678383826105170602746620441520500000000000000000",
+    "coordinate_movement_above_kappa": "18366331166297442643638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "compact_phase_layer_above_kappa": "2162217432929694421865151766284406406750130106912571298288744311389664676321154553325443063932615265500273427465417372291961078797500186482021598196220864724502073562794321721495909271487916272123066364573090867158733602102942139828942948119826567895117657735931242412552142115993658721131807652121245405597008729738085996882098827505544799292706887688962943315453243734011269470907847537475759121116959/3282290156099364793623721808224664734599224105676919239087430234567083836826988376006387856482178928788981393147808286007792385920322253722201767929416477166653535959868879662007824712314966127806177730297423483901027506968664489033051447038531157336856996129340173164228163173132938540666878136418539696486021989985271231781781450073973851986744395930427624741098739356767652210341205493240883041000000000000000000000000",
+    "bulk_exposure_above_kappa": "18366331166297442643638409953866657622706241115298082593784379580155884572917200344472124669626723797186984560821354838219435018476566046245535271824370260204012228829867664389945037956713272090789374737043715481558118907727540190325040178552489169072639330426685561304684411155742187127395446448215283528354225333356459993467204656154640201711847789658794506759116959/6553600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "Gaussian_arithmetic_above_kappa": "3459549862061604734603119000288135185599048930594577483413534350681604222364149381513734506124898314107794757333503684352109330751431850564586790435014141209089617692592490675721252039075493424376582867023583565908064103981211604925002136822590731750882654491687665464187325922487757833574016643520874500079031859194131586174097193077741723252642212348978267561300034633661645214043882264684510538316959/5251664249758983669797954893159463575358758569083070782539888375307334138923181401610220570371486286062370229036493257612467817472515605955522828687066363466645657535790207459212519539703945804489884368475877574241644011149863182452882315261649851738971193806944277062765061077012701665067005018269663514377635183976433970850850320118358163178791033488684199585757982970828243536545928789185412865600000000000000000000000",
+    "scalar_work_above_kappa": "17297762439468648070474769496327908826654183049869310124744628103128959380156094215522176556175917499254688942593091012993690684926702934111948840982142423711356755077106292854124908226676316381747425559828839019234256124016085899282966816318741812879042619886422844681629286525091481699624245885116918174553945240058617871955413092514508912158619008722475059516999137563265653140828252688244525655116959/26258321248794918348989774465797317876793792845415353912699441876536670694615907008051102851857431430311851145182466288062339087362578029777614143435331817333228287678951037296062597698519729022449421842379387871208220055749315912264411576308249258694855969034721385313825305385063508325335025091348317571888175919882169854254251600591790815893955167443420997928789914854141217682729643945927064328000000000000000000000000",
+    "dimension_above_kappa": "1635654921950317604269246176697592893315360642164647696163717235784796569190497511406755693461406225762418838586331730835704915263244133189022659330234814818810892219059957239485707752007657731284696774507602551594083331891078337774583028045958975578287492520966716631023415709897216606029214103869146078792163164507055296177461882843051065083293106678283624262730067538295610766368389669754871598780028939340626181/1641145078049682396811860904112332367299612052838459619543715117283541918413494188003193928241089464394490696573904143003896192960161126861100883964708238583326767979934439831003912356157483063903088865148711741950513753484332244516525723519265578668428498064670086582114081586566469270333439068209269848243010994992635615890890725036986925993372197965213812370549369678383826105170602746620441520500000000000000000"
+  },
+  "controls": [
+    "next_grid",
+    "zero_eta",
+    "zero_beta",
+    "unit_beta"
+  ],
+  "scope": "Conditional native exact-complex witness after complete conservative admission, moment and outer checks; PR559 exact-cover recurrence correction only, bit bad-residue surcharge and H1-H5 retained. The new source-branch gauge and retired-basis completion, the gauge44-barch U8 local word and all 72 cold helper ends, and explicit all144 whole-owner dispatch with a two-copy remainder trade are composed with the cited unchanged merged PR589 bit supplier (PR555 punctured R439 word; derived bit deficit T(2Kv-L*cst)), replacing the PR543 supplier of PR635; This is a new T16 composition of the accepted PR799 and PR589 suppliers. All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape and analytic transfer remain assumptions. No unconditional theorem or full Lean certification."
+}
diff --git a/research/lean-bit-moment-discharge/sources/EXPECTED.json b/research/lean-bit-moment-discharge/sources/EXPECTED.json
new file mode 100644
index 0000000000..e293ddc557
--- /dev/null
+++ b/research/lean-bit-moment-discharge/sources/EXPECTED.json
@@ -0,0 +1,222 @@
+{
+ "word": {
+  "file": "tune/bitE8mut-p111-tuned.json.gz",
+  "file_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f",
+  "content_sha256": "5642fd0e35a1acc11acff8d0c08350c1617e95f310d4d35ad63a651f9eeeba0b",
+  "v": 111,
+  "R": 439,
+  "punctured": [
+   10,
+   15,
+   51,
+   53,
+   56,
+   66,
+   72,
+   89,
+   111
+  ],
+  "retained_totals": 9,
+  "copy_ranks": [
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7,
+   7
+  ],
+  "decoder_constant": 63,
+  "gates": {
+   "D": 111,
+   "A": 2075,
+   "B": 712,
+   "C": 2574
+  },
+  "local_histogram": {
+   "1": 1323,
+   "2": 1342,
+   "3": 79,
+   "4": 44,
+   "5": 102,
+   "6": 11,
+   "7": 19
+  },
+  "legality": {
+   "records": 27234,
+   "common_frame_ADDs": 24305,
+   "rank_mass": 5129
+  },
+  "five_stage_columns": 883,
+  "five_stage_payload_bits": 93,
+  "nine_stage_columns": 1327,
+  "nine_stage_payload_bits": 93,
+  "eleven_stage_columns": 1549,
+  "eleven_stage_payload_bits": 93,
+  "base_content_sha256": "d0df3c89ae84989f4045ba1681a5e2e9fcdfa38ed0301c8abf5185537155cbe3"
+ },
+ "interface": {
+  "hypotheses": {
+   "H1_no_target_feeds_z": true,
+   "H2_D_frame0_targets_from_helpers": true,
+   "H3_A_z_only_scatter_targets_B_split": true,
+   "H4_C_literal_reverse_at_full": true,
+   "H5_V_identity": true
+  },
+  "conclusion": {
+   "U_block_form": true,
+   "J_identity": true,
+   "K_equals_D": true,
+   "C_is_U_inverse": true
+  },
+  "interleaving": {
+   "z_gates_A": 2075,
+   "source_writes_A": 0,
+   "z_gates_B": 499,
+   "source_writes_B": 483,
+   "helper_writes_B": 16,
+   "sources_rewritten_B": 108,
+   "B_z_write_frame_dims": {
+    "4": 388,
+    "6": 111
+   },
+   "B_z_operand_kinds": {
+    "helper<-helper": 3,
+    "helper<-source": 13,
+    "source<-helper": 108,
+    "source<-source": 375
+   },
+   "B_z_operand_kinds_by_dim": {
+    "dim4:helper<-source": 13,
+    "dim4:source<-source": 375,
+    "dim6:helper<-helper": 3,
+    "dim6:source<-helper": 108
+   },
+   "B_z_writes_after_a_target_read_of_the_same_register": 454,
+   "B_target_reads_of_registers_rewritten_earlier_in_B": 111,
+   "target_reads_of_targets": 0,
+   "cleanup_gates": 2574
+  }
+ },
+ "nine": {
+  "pipeline": "PR #510 (PR #463 nine-stage template, 32 replicas, PR #442 hosting, PR #493 outer assembly), parameterised for v <= 120 by code/adapt9p.py",
+  "bit_lower": "1733427039589844234749/1000000000000000000000000",
+  "bit_lower_decimal": "0.001733427039589844234749",
+  "profile": {
+   "1": 381024,
+   "2": 400416,
+   "3": 22752,
+   "4": 26880,
+   "5": 29376,
+   "6": 17376,
+   "7": 26784,
+   "42": 288
+  },
+  "bit": {
+   "live": 28416,
+   "physical": 28425,
+   "maxchild": 42,
+   "rank_mass": 1808352,
+   "hosted_residuals": 126432,
+   "bank_assignments": 0,
+   "prefix_bits": 177,
+   "charged_prefix_bits": 192,
+   "coefficient_bits": 177,
+   "two_level_coefficient_bits": 393,
+   "charged_two_level_coefficient_bits": 512,
+   "row_coefficient": 18355,
+   "halving_depth": 2
+  },
+  "kappa": {
+   "pr548": {
+    "kappa": "49718254847979/31250000000000000",
+    "kappa_decimal": "0.001590984155135328",
+    "complex_lower": "796759709641153381751/500000000000000000000000",
+    "binding_component": "complex"
+   },
+   "pr544": {
+    "kappa": "397677800014309/250000000000000000",
+    "kappa_decimal": "0.001590711200057236",
+    "complex_lower": "31864911873350496687/20000000000000000000000",
+    "binding_component": "complex"
+   },
+   "pr535": {
+    "kappa": "793733736881443/500000000000000000",
+    "kappa_decimal": "0.001587467473762886",
+    "complex_lower": "1589991533606044174031/1000000000000000000000000",
+    "binding_component": "complex"
+   },
+   "pr531": {
+    "kappa": "1517760977820331/1000000000000000000",
+    "kappa_decimal": "0.001517760977820331",
+    "complex_lower": "304013615566499291631/200000000000000000000000",
+    "binding_component": "complex"
+   }
+  }
+ },
+ "eleven": {
+  "pipeline": "PR #493 (PR #445 geometry, PR #472 emitter, audit and invoice, PR #442 hosting), parameterised by PR #545's code/adapt.py",
+  "bit_lower": "855475950388791987811/500000000000000000000000",
+  "bit_lower_decimal": "0.001710951900777583975622",
+  "profile": {
+   "1": 116424,
+   "2": 121648,
+   "3": 6952,
+   "4": 7424,
+   "5": 8976,
+   "6": 4520,
+   "7": 8776,
+   "56": 2600
+  },
+  "bit": {
+   "live": 8880,
+   "physical": 8889,
+   "maxchild": 56,
+   "rank_mass": 689304,
+   "hosted_residuals": 38632,
+   "prefix_bits": 4304,
+   "charged_prefix_bits": 4352,
+   "coefficient_bits": 4304,
+   "three_level_coefficient_bits": 12966,
+   "charged_three_level_coefficient_bits": 12992,
+   "row_coefficient": 19431,
+   "halving_depth": 3
+  },
+  "emitted_program_sha256": "793b6f40c9aa4b8db57fec0ac0973e16884dae28707e482ee8f7a2349a5d5a4b",
+  "kappa": {
+   "pr548": {
+    "kappa": "49718254847979/31250000000000000",
+    "kappa_decimal": "0.001590984155135328",
+    "complex_lower": "796759709641153381751/500000000000000000000000",
+    "binding_component": "complex"
+   },
+   "pr544": {
+    "kappa": "397677800014309/250000000000000000",
+    "kappa_decimal": "0.001590711200057236",
+    "complex_lower": "31864911873350496687/20000000000000000000000",
+    "binding_component": "complex"
+   },
+   "pr535": {
+    "kappa": "793733736881443/500000000000000000",
+    "kappa_decimal": "0.001587467473762886",
+    "complex_lower": "1589991533606044174031/1000000000000000000000000",
+    "binding_component": "complex"
+   },
+   "pr531": {
+    "kappa": "1517760977820331/1000000000000000000",
+    "kappa_decimal": "0.001517760977820331",
+    "complex_lower": "304013615566499291631/200000000000000000000000",
+    "binding_component": "complex"
+   }
+  }
+ },
+ "base": {
+  "nine_bit_lower": "1733052823330162099157/1000000000000000000000000",
+  "nine_bit_lower_decimal": "0.001733052823330162099157",
+  "eleven_bit_lower": "427652201524503168379/250000000000000000000000",
+  "eleven_bit_lower_decimal": "0.001710608806098012673516",
+  "note": "PR #555's EXPECTED.json (untuned word); the tune/ pipeline is the same, with the same frozen hosting selections"
+ }
+}
diff --git a/research/lean-bit-moment-discharge/sources/GLOBAL.json b/research/lean-bit-moment-discharge/sources/GLOBAL.json
new file mode 100644
index 0000000000..1f648db9e6
--- /dev/null
+++ b/research/lean-bit-moment-discharge/sources/GLOBAL.json
@@ -0,0 +1,190 @@
+{
+  "status": "PASS_IDLE_AXIS_HOSTED_BIT_TEMPLATE",
+  "h": 8,
+  "m": 64,
+  "v": 111,
+  "R": 439,
+  "replicas": 32,
+  "live": 28416,
+  "physical": 28425,
+  "word_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f",
+  "source_records_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a",
+  "local_checks": {
+    "forward": {
+      "copies": 9,
+      "adds": 24305,
+      "records": 27234,
+      "all_columns": 661,
+      "cancellation_free_row_l1": 49347,
+      "profile": {
+        "1": 1323,
+        "2": 1342,
+        "3": 79,
+        "4": 44,
+        "5": 102,
+        "6": 11,
+        "7": 19
+      },
+      "sha256": "a778a0300bbf4b07908ee24c0d271426ba6c70568e788af2f0ac8517897cb5b4"
+    },
+    "reverse": {
+      "copies": 9,
+      "adds": 24305,
+      "records": 27234,
+      "all_columns": 661,
+      "cancellation_free_row_l1": 1113070,
+      "profile": {
+        "1": 1323,
+        "2": 1342,
+        "3": 79,
+        "4": 44,
+        "5": 102,
+        "6": 11,
+        "7": 19
+      },
+      "sha256": "98d97804744d691548b4d54868a8a0e5f500c55ab32ac4be96f3ba30e6f5bef8"
+    }
+  },
+  "scalar_stages": [
+    {
+      "stage": 0,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": false
+    },
+    {
+      "stage": 1,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": true
+    },
+    {
+      "stage": 2,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": false
+    },
+    {
+      "stage": 3,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": true
+    },
+    {
+      "stage": 4,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": false
+    },
+    {
+      "stage": 5,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": true
+    },
+    {
+      "stage": 6,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": false
+    },
+    {
+      "stage": 7,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": true
+    },
+    {
+      "stage": 8,
+      "all_columns": 4839,
+      "helper_columns": 3951,
+      "reverse": false
+    }
+  ],
+  "independent_unbanked_scalar_columns": 4839,
+  "all_scalar_columns_restored": true,
+  "geometry_sha256": "0058c491d839142aa99ef86a5ec697ce99857632228531512ea3fa74fb24d734",
+  "template_sha256": "783928654999d6f580601a988b582098720802171b6be88ea4af6198b5732992",
+  "emitted_program_sha256": "96c7ad2e744e9a503a4ef5ecd52d0f6a8899bdb5efac2e3aafa0db18adf99523",
+  "emitted_events": 7843392,
+  "local_invocations": 288,
+  "bank_assignments": 0,
+  "banks_per_stage": {
+    "0": 0,
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 0,
+    "5": 0,
+    "6": 0,
+    "7": 0,
+    "8": 0
+  },
+  "entrance_rank_total": 0,
+  "residual_bank_slots": true,
+  "padding_calls": 0,
+  "profile": {
+    "1": 381024,
+    "2": 400416,
+    "3": 22752,
+    "4": 26880,
+    "5": 29376,
+    "6": 17376,
+    "7": 26784,
+    "42": 288
+  },
+  "paid_calls": 904896,
+  "rank_mass": 1808352,
+  "deficit": 10272,
+  "maxchild": 42,
+  "halving_depth": 2,
+  "halving_integer_inequality": [
+    4096,
+    3528
+  ],
+  "local_additions": 24305,
+  "bridge_additions": 63936,
+  "copy_erase_episodes": 2592,
+  "global_prefix_bound": "117742596540718658156527847560864213734191286190080000",
+  "global_prefix_bits": 177,
+  "charged_prefix_bits": 192,
+  "omitted_bridge_shears_rejected": [
+    0,
+    1,
+    2,
+    3,
+    4,
+    5,
+    6,
+    7,
+    8,
+    9,
+    10,
+    11,
+    12,
+    13,
+    14,
+    15,
+    16,
+    17
+  ],
+  "scope": "Complete source-bound finite cover template. Local and unbanked global F2 columns are replayed; arbitrary physical bank dirt follows by injective owner routes and the all-column local theorem. Astronomical cover enumeration and all-size compiler interfaces remain explicit inherited assumptions. Additional PR442 idle-data hosting interface is assumed; every hosting window and coordinate ownership is audited.",
+  "seconds": 4.661764542004676,
+  "parent_template_sha256": "cf82d086340e6d59df65eb252d8bbb052754d940cd145dc8fa32164bbeff76e6",
+  "banks_per_stage_hosted": {
+    "0": 0,
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 0,
+    "5": 0,
+    "6": 0,
+    "7": 0,
+    "8": 0
+  },
+  "hosted_residuals_per_replica": 3951,
+  "hosted_residuals": 126432,
+  "hosted_coordinates_per_replica": 31608,
+  "saved_idle_cost_proxy": 13174.7497998684,
+  "additional_interface": "PR442 idle-data hosting during untouched windows"
+}
diff --git a/research/lean-bit-moment-discharge/test_package.py b/research/lean-bit-moment-discharge/test_package.py
new file mode 100644
index 0000000000..874990a054
--- /dev/null
+++ b/research/lean-bit-moment-discharge/test_package.py
@@ -0,0 +1,179 @@
+"""Failure controls for source binding and the two explicitly distinct replay modes.
+
+No Lean execution is inferred from these standard-library tests.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0.
+"""
+from pathlib import Path
+import copy
+from fractions import Fraction as Q
+import hashlib
+import json
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+
+HERE = Path(__file__).resolve().parent
+sys.path.insert(0, str(HERE))
+import certificate
+import finite
+import verify
+
+
+def writable_copy(root):
+    """Fault controls mutate their temporary copy, including from read-only exports."""
+    shutil.copytree(HERE, root, copy_function=shutil.copyfile)
+    root.chmod(0o755)
+    for path in root.rglob("*"):
+        if path.is_dir():
+            path.chmod(0o755)
+
+
+class Controls(unittest.TestCase):
+    def test_each_pinned_source(self):
+        pins = verify.check_sources()
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary) / "source"
+            writable_copy(root)
+            for name in pins["files"]:
+                with self.subTest(source=name):
+                    path = root / name
+                    old = path.read_bytes()
+                    path.write_bytes(old + b"\n")
+                    with self.assertRaisesRegex(ValueError, "source bytes changed"):
+                        verify.check_sources(root)
+                    path.write_bytes(old)
+            verify.check_sources(root)
+
+    def test_proof_escape_even_with_rebound_hash(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary) / "source"
+            writable_copy(root)
+            path = root / "lean/StoppedRecurrence.lean"
+            old = path.read_text()
+            pins = verify.read(root / "PROOF-SOURCES.json")
+            for escape in ("axiom injected : False", "example : False := by sorry",
+                           "example : False := by admit"):
+                with self.subTest(escape=escape):
+                    path.write_text(old + "\n" + escape + "\n")
+                    pins["files"]["lean/StoppedRecurrence.lean"] = hashlib.sha256(path.read_bytes()).hexdigest()
+                    (root / "PROOF-SOURCES.json").write_text(json.dumps(pins))
+                    with self.assertRaisesRegex(ValueError, "unapproved proof escape"):
+                        verify.check_sources(root)
+
+    def test_axiom_report_coverage_and_trust(self):
+        targets = verify.check_sources()["axiom_targets"]
+        lines = ["'" + name + "' depends on axioms: [propext, Classical.choice, Quot.sound]"
+                 for name in targets]
+        good = "\n".join(lines)
+        self.assertEqual(set(verify.parse_axioms(good, targets)), set(targets))
+        for bad in ("\n".join(lines[:-1]), good + "\n" + lines[0],
+                    good.replace("Quot.sound", "sorryAx", 1),
+                    good.replace("Quot.sound", "untrustedAxiom", 1),
+                    good + "\n'extra' depends on axioms: []"):
+            with self.subTest(report=bad[-100:]):
+                with self.assertRaises(ValueError):
+                    verify.parse_axioms(bad, targets)
+
+    def test_strict_receipt_types(self):
+        self.assertNotEqual(verify.encoded({"n": 1}), verify.encoded({"n": True}))
+        self.assertNotEqual(verify.encoded({"n": 1}), verify.encoded({"n": 1.0}))
+        with tempfile.TemporaryDirectory() as temporary:
+            path = Path(temporary) / "bad.json"
+            for raw in ('{"n": 1, "n": 1}', '{"n": NaN}', '{"n": Infinity}'):
+                path.write_text(raw)
+                with self.assertRaises(ValueError):
+                    verify.read(path)
+
+    def test_corrupt_dyadic_certificates(self):
+        original = verify.read(HERE / "DYADIC.json")
+        counts = certificate.profile()
+        mutations = {
+            "small_square": lambda d: d["rows"][0]["upper_numerators"].__setitem__(0, 124999999999),
+            "negative_square": lambda d: d["rows"][0]["upper_numerators"].__setitem__(0, -125000000000),
+            "short_chain": lambda d: d["rows"][0]["upper_numerators"].pop(),
+            "reversed_chain": lambda d: d["rows"][0]["upper_numerators"].reverse(),
+            "omitted_rank": lambda d: d["rows"].pop(),
+            "wrong_count": lambda d: d["rows"][0].__setitem__("count", 381025),
+            "upward_exponent": lambda d: d.__setitem__("numerator", 130850),
+            "float_grid": lambda d: d.__setitem__("grid", float(10**12)),
+            "boolean_bound": lambda d: d["rows"][0]["upper_numerators"].__setitem__(0, True),
+            "boolean_rank": lambda d: d["rows"][0].__setitem__("rank", True),
+        }
+        for name, mutate in mutations.items():
+            with self.subTest(mutation=name):
+                data = copy.deepcopy(original)
+                mutate(data)
+                with self.assertRaises(ValueError):
+                    certificate.check(data, counts)
+
+    def test_proposal_domain_and_unit_endpoint(self):
+        for x, p, k, d in [(Q(0), 1, 3, 100), (Q(2), 1, 3, 100),
+                           (Q(1, 2), 8, 3, 100), (Q(1, 2), -1, 3, 100),
+                           (Q(1, 2), 1, 0, 100), (Q(1, 2), 1, 3, 0)]:
+            with self.subTest(parameters=(x,p,k,d)):
+                with self.assertRaises(ValueError):
+                    certificate.propose_chain(x,p,k,d)
+        self.assertEqual(certificate.propose_chain(Q(1, 2), 0, 3, 100), [100]*3)
+
+    def test_generated_lean_binding_and_fallback(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary) / "source"
+            writable_copy(root)
+            path = root / "lean/SelectedMoment.lean"
+            old = path.read_text()
+            path.write_text(old.replace("15735950448", "15735950449"))
+            with self.assertRaisesRegex(ValueError, "Lean/certificate semantic binding"):
+                finite.replay(root)
+            path.write_text(old)
+            path = root / "lean/Selected.lean"
+            path.write_text(path.read_text().replace("118606528512 /", "0 /"))
+            with self.assertRaisesRegex(ValueError, "formal scalar binding"):
+                finite.replay(root)
+
+    def test_lean_profile_semantic_binding(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary) / "source"
+            writable_copy(root)
+            path = root / "lean/Selected.lean"
+            path.write_text(path.read_text().replace("381024, 400416", "381025, 400416"))
+            with self.assertRaisesRegex(ValueError, "formal profile binding"):
+                finite.replay(root)
+
+    def test_receipt_drift_is_rejected_end_to_end(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary) / "source"
+            writable_copy(root)
+            path = root / "FINITE.json"
+            value = verify.read(path)
+            value["calibration"]["cases"] -= 1
+            path.write_text(json.dumps(value))
+            result = subprocess.run([sys.executable, "-I", "-O", "-B", str(root / "verify.py")],
+                                    cwd=temporary, capture_output=True, text=True, timeout=90)
+            self.assertNotEqual(result.returncode, 0)
+            self.assertIn("finite receipt differs", result.stderr)
+
+    def test_existing_output_is_preserved(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            out = Path(temporary) / "keep.json"
+            out.write_bytes(b"preserve existing evidence\n")
+            result = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py"),
+                                     "--out", str(out)], cwd=temporary, capture_output=True,
+                                    text=True, timeout=15)
+            self.assertNotEqual(result.returncode, 0)
+            self.assertIn("output already exists", result.stderr)
+            self.assertEqual(out.read_bytes(), b"preserve existing evidence\n")
+
+    def test_kernel_mode_requires_explicit_environment(self):
+        for arguments in (["--lake", "/missing/lake"], ["--fetch-cache"],
+                          ["--lake", "/missing/lake", "--work-dir", "/missing/work"]):
+            with self.subTest(arguments=arguments):
+                result = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py"),
+                                         *arguments], capture_output=True, text=True, timeout=15)
+                self.assertNotEqual(result.returncode, 0)
+                self.assertNotIn("PASS_", result.stdout)
+
+
+if __name__ == "__main__":
+    unittest.main(verbosity=2)
diff --git a/research/lean-bit-moment-discharge/verify.py b/research/lean-bit-moment-discharge/verify.py
new file mode 100644
index 0000000000..84a1f09639
--- /dev/null
+++ b/research/lean-bit-moment-discharge/verify.py
@@ -0,0 +1,195 @@
+"""Source/finite replay, or an explicitly requested fresh Lean kernel build.
+
+The default command never claims Lean ran. Kernel mode requires --lake,
+--work-dir and either --packages (an existing pinned cache) or --fetch-cache.
+Gareth Davidson with OpenAI Codex assistance. Apache-2.0.
+"""
+from pathlib import Path
+import argparse
+import hashlib
+import json
+import os
+import re
+import shutil
+import subprocess
+import sys
+
+HERE = Path(__file__).resolve().parent
+sys.path.insert(0, str(HERE))
+from finite import replay
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def unique(items):
+    out = {}
+    for key, value in items:
+        need(key not in out, "duplicate JSON key")
+        out[key] = value
+    return out
+
+
+def read(path):
+    def reject(value):
+        raise ValueError("nonfinite JSON: " + value)
+    return json.loads(Path(path).read_bytes(), object_pairs_hook=unique, parse_constant=reject)
+
+
+def encoded(value):
+    return json.dumps(value, sort_keys=True, separators=(",", ":"))
+
+
+def lean_code(source):
+    """Remove nested Lean comments; retain newlines and actual code tokens."""
+    output, depth, i = [], 0, 0
+    while i < len(source):
+        if source.startswith("/-", i):
+            depth += 1
+            i += 2
+        elif depth and source.startswith("-/", i):
+            depth -= 1
+            i += 2
+        elif not depth and source.startswith("--", i):
+            end = source.find("\n", i)
+            i = len(source) if end < 0 else end
+        else:
+            output.append(source[i] if not depth or source[i] == "\n" else " ")
+            i += 1
+    need(depth == 0, "unterminated Lean comment")
+    return "".join(output)
+
+
+def check_sources(root=HERE):
+    pins = read(root / "PROOF-SOURCES.json")
+    need(pins["schema"] == "bit-moment-discharge-proof-sources/1", "source schema")
+    for name, expected in pins["files"].items():
+        path = Path(name)
+        need(not path.is_absolute() and ".." not in path.parts, "relative source path")
+        raw = (root / path).read_bytes()
+        need(hashlib.sha256(raw).hexdigest() == expected, "source bytes changed: " + name)
+        if path.suffix == ".lean":
+            code = lean_code(raw.decode())
+            need(not re.search(r"\b(axiom|sorry|admit|native_decide|unsafe|run_tac|elab|macro|syntax)\b", code),
+                 "unapproved proof escape in " + name)
+    manifest = read(root / "lean/lake-manifest.json")
+    actual = {p["name"]: {"rev": p["rev"], "url": p["url"]} for p in manifest["packages"]}
+    need(encoded(actual) == encoded(pins["dependencies"]), "dependency pins")
+    need((root / "lean/lean-toolchain").read_text().strip() == pins["toolchain"], "toolchain pin")
+    need(len(pins["axiom_targets"]) == len(set(pins["axiom_targets"])), "distinct theorem targets")
+    return pins
+
+
+def parse_axioms(output, targets):
+    found = {}
+    for name, raw in re.findall(r"'([^']+)' depends on axioms:\s*\[([^\]]*)\]", output):
+        need(name not in found, "duplicate axiom report")
+        axioms = sorted(x.strip() for x in raw.split(",") if x.strip())
+        need(set(axioms) <= {"propext", "Classical.choice", "Quot.sound"},
+             "unexpected axiom: " + name)
+        found[name] = axioms
+    need(set(found) == set(targets), "missing or extra theorem axiom report")
+    need("sorryAx" not in output, "unchecked proof reported")
+    return found
+
+
+def kernel_build(args, pins):
+    lake = args.lake.resolve()
+    need(lake.is_file(), "Lake executable missing")
+    lean = lake.with_name("lean")
+    version = subprocess.check_output([str(lean), "--version"], text=True)
+    need(pins["lean_version"] in version and pins["lean_commit"] in version, "wrong Lean version")
+    work = args.work_dir.resolve()
+    need(not work.exists(), "build directory already exists")
+    shutil.copytree(HERE / "lean", work)
+    env = dict(os.environ, PATH=str(lake.parent) + os.pathsep + os.environ.get("PATH", ""),
+               LEAN_NUM_THREADS="4")
+    # No previously built local proof objects are copied; only library packages
+    # may be reused, and every Git dependency is checked below.
+    def run(command, label, timeout=180):
+        result = subprocess.run(command, cwd=work, env=env, capture_output=True, text=True, timeout=timeout)
+        output = result.stdout + result.stderr
+        (work / (label + ".log")).write_text(output)
+        need(result.returncode == 0, label + " failed; inspect " + str(work / (label + ".log")))
+        return output
+
+    if args.packages:
+        packages = args.packages.resolve()
+        need(packages.is_dir(), "package cache missing")
+        (work / ".lake").mkdir()
+        (work / ".lake/packages").symlink_to(packages, target_is_directory=True)
+    else:
+        run([str(lake), "exe", "cache", "get"], "cache", timeout=600)
+        packages = work / ".lake/packages"
+    for name, dependency in pins["dependencies"].items():
+        path = packages / name
+        actual = subprocess.check_output(["git", "-C", str(path), "rev-parse", "HEAD"], text=True).strip()
+        need(actual == dependency["rev"], "dependency head: " + name)
+        need(subprocess.run(["git", "-C", str(path), "diff", "--quiet", "HEAD", "--"],
+                            capture_output=True).returncode == 0, "modified dependency source: " + name)
+    run([str(lake), "build"], "kernel-build")
+    probe = "import ClosedRecurrence\n" + "\n".join("#print axioms " + n for n in pins["axiom_targets"]) + "\n"
+    (work / "AxiomProbe.lean").write_text(probe)
+    output = run([str(lake), "env", "lean", "AxiomProbe.lean"], "axioms")
+    axioms = parse_axioms(output, pins["axiom_targets"])
+    # Two corrupted certificate proposals reach the real arithmetic prover.
+    # They are not rejected merely because their source hash changed.
+    generated = (work / "SelectedMoment.lean").read_text().split("theorem rank_2_upper")[0]
+    generated = generated.replace("SelectedBitMoment", "RejectedBitMoment") + "end RejectedBitMoment\n"
+    literal = "125000000000 / 1000000000000"
+    need(generated.count(literal) == 3, "expected first square certificate")
+    controls = {
+        "small_square": generated.replace(literal, "124999999999 / 1000000000000"),
+        "negative_square": generated.replace(literal, "(-125000000000) / 1000000000000"),
+        "upward_exponent": "import DyadicPower\nexample : (1 / 64 : ℝ) ^ (9983 / 10000 : ℝ) ≤ (1 / 64 : ℝ) ^ (130850 / 131072 : ℝ) := by\n  exact le_refl ((1 / 64 : ℝ) ^ (9983 / 10000 : ℝ))\n",
+    }
+    rejected = []
+    for key, source in controls.items():
+        path = work / ("Reject_" + key + ".lean")
+        path.write_text(source)
+        result = subprocess.run([str(lake), "env", "lean", path.name], cwd=work, env=env,
+                                capture_output=True, text=True, timeout=90)
+        output = result.stdout + result.stderr
+        (work / ("reject_" + key + ".log")).write_text(output)
+        need(result.returncode != 0 and "error:" in output
+             and any(term in output for term in ("unsolved goals", "Type mismatch", "Application type mismatch"))
+             and not any(term in output for term in ("Unknown", "unknown", "object file", "failed to synthesize")),
+             "invalid negative control: " + key)
+        rejected.append(key)
+    return {"kernel_checked": True, "lean_version": version.strip(),
+            "axioms": axioms, "rejected_invalid_proofs": rejected,
+            "dependencies": pins["dependencies"]}
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--lake", type=Path)
+    parser.add_argument("--work-dir", type=Path)
+    group = parser.add_mutually_exclusive_group()
+    group.add_argument("--packages", type=Path)
+    group.add_argument("--fetch-cache", action="store_true")
+    parser.add_argument("--out", type=Path)
+    args = parser.parse_args()
+    need(args.out is None or not args.out.exists(), "output already exists")
+    need(bool(args.lake) == bool(args.work_dir), "--lake and --work-dir are paired")
+    need(not args.lake or args.packages or args.fetch_cache, "kernel mode needs --packages or --fetch-cache")
+    need(args.lake or not (args.packages or args.fetch_cache), "cache options require kernel mode")
+    pins = check_sources()
+    finite = replay()
+    need(encoded(finite) == encoded(read(HERE / "FINITE.json")), "finite receipt differs")
+    result = {"finite": finite, "proof_source_hashes": pins["files"], "kernel_checked": False}
+    if args.lake:
+        result.update(kernel_build(args, pins))
+    if args.out:
+        with args.out.open("x") as handle:
+            json.dump(result, handle, sort_keys=True, indent=2)
+            handle.write("\n")
+    print("PASS_BIT_MOMENT_DISCHARGE_KERNEL" if result["kernel_checked"] else
+          "PASS_BIT_MOMENT_SOURCES_AND_FINITE_ONLY", "square_steps=136 calibration_cases=4774",
+          "kernel_checked=" + str(result["kernel_checked"]).lower())
+
+
+if __name__ == "__main__":
+    main()