From 30b1ee55a07ca658f454fba35b85e71dc288134c Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 11:18:28 -0400 Subject: [PATCH 1/2] Research: bootstrap cutoffs need only a stock constant (repair (b) of #1956) Restated ordinary-bootstrap cutoff lemma: the time bound holds for all widths with lower-order tolls absorbed by max(2, 2/(e ln2 delta)), so the cutoff only serves the borrowed-stock fit. All 14 recorded cutoffs of the selected #1094 receipt satisfy the fit-only rule with exact headroom 6,562,783+ bits. Co-Authored-By: Claude Opus 5.5 --- .../README.md | 160 ++++++++++ .../RESULT.json | 109 +++++++ .../SOURCES.json | 48 +++ .../TASK.json | 66 ++++ .../VERIFY.json | 24 ++ .../verify.py | 292 ++++++++++++++++++ 6 files changed, 699 insertions(+) create mode 100644 research/bootstrap-cutoff-time-space-split/README.md create mode 100644 research/bootstrap-cutoff-time-space-split/RESULT.json create mode 100644 research/bootstrap-cutoff-time-space-split/SOURCES.json create mode 100644 research/bootstrap-cutoff-time-space-split/TASK.json create mode 100644 research/bootstrap-cutoff-time-space-split/VERIFY.json create mode 100644 research/bootstrap-cutoff-time-space-split/verify.py diff --git a/research/bootstrap-cutoff-time-space-split/README.md b/research/bootstrap-cutoff-time-space-split/README.md new file mode 100644 index 0000000000..c093680511 --- /dev/null +++ b/research/bootstrap-cutoff-time-space-split/README.md @@ -0,0 +1,160 @@ +# Bootstrap cutoffs: the time constant needs no cutoff (repair (b)) + +**A scoped proof repair for one finite lemma. The numerical κ, the certificate, the suppliers and the frontier are +unchanged. No new bound is claimed.** + +PR #1956 ([`bootstrap-cutoff-carry`](https://github.com/CrocSwap/integer-mult-bounds/pull/1956)) showed that the 14 +recorded bootstrap cutoffs of the selected #1094 receipt (`research/community-frontier1094-audit/ASSEMBLY.json`) +are not valid instances of the cutoff lemma **as written** in +[PR387's PROOF](../bootstrap-depth-audit/sources/pr387/PROOF.md) and +[FINITE_BIT_ACCOUNTING](../five-stage-source527-banks/proof/FINITE_BIT_ACCOUNTING.md). That lemma's C must +dominate the "previous ordinary constants". The carried time constant `C_old·2^(L·Δa)` is about twice too large +for every stage after the first. PR #1956 left open whether a restated lemma ("repair (b)") makes the recorded +numbers valid. This package answers that question for the time constant: yes. The cutoff has only one real job, +to make the borrowed stock fit. A previous time constant never needs to enter it. What remains is a space +obligation with a large exact margin. + +## The two jobs of the 1/16 condition + +At a bootstrap stage, write `a = a_(j-1)`, `a' = a_j = (1−s)s + s·a`, and let δ be the minimum of the four gaps +`s−a'` (atom), `1−a'−s` (borrowing), `1−a'−s(1−a)` (remainder) and `1−s` (stock). The lemma takes +`e ≥ e0 = 2^L` so that `C(1+log2 e)e^(−δ) ≤ 1/16`, and says "every lower-order toll is covered **and the +borrowed high part fits**." These are different requirements. + +**Fit (space).** The stopped construction at width e borrows `k = ⌈log_q S(e,w)⌉` high digits, where +`w = ⌈e^s⌉` and `log_q S(e,w) = O(w log e)`. S counts the row divisors over the recursion depth times the +inherited old-leaf reserve. The construction is defined only when `k < e/2` +([`three-stage-cover-rows.tex`](../five-stage-source527-banks/proof/three-stage-cover-rows.tex), "Borrowing and +restoring the stock": "For sufficiently large e, k **Absorption bound.** For `δ > 0` and all `t ≥ 0`, +> `(1+t)·2^(−δt) ≤ M(δ) := max(2, 2/(ℯ·ln2·δ))`, where ℯ = exp(1) (e is reserved for the width). +> +> *Proof.* If t ≤ 1, the left side is at most 2. If t ≥ 1, then `1+t ≤ 2t`, and `exp(y) ≥ ℯ·y` gives +> `2^(δt) ≥ ℯ·ln2·δt`. Hence the left side is at most `2/(ℯ·ln2·δ)`. + +## Restated lemma + +*Retained hypotheses, which are not re-proved here.* (H1) `A_(j−1)` is a completed ordinary algorithm at every +width `e ≥ 1`, with `T_(j−1)(e) ≤ C_(j−1)·V·e^(1−a)`. (H2) Whenever `k(e) < e/2`, the stopped construction is a +completed ordinary algorithm at width e with + + T(e)/V ≤ K·[e^(1−s) + e^(1−a') + e^s(1+log2 e) + w^(1−a)]. + +Here K is finite and does not depend on e or on the cutoff. K is built from fresh coefficients (multiplicities, +the weighted-induction factor `1+1/(1−μ_1)+1/(1−μ_τ)`, scalar/wrapper/padding counts, the stock coefficient +inside the high-part exchange) and from `C_(j−1)`, which enters through the ordinary leaves, the remainder, the +routing and the high-part exchange. This is the retained stopped-leaf estimate of PR387 with its O-constant +written as K. (H3) `log_q S(e,w) ≤ σ·w·(1+log2 e)`, where σ is a *stock* coefficient. It is built from the +per-level row stock, the depth factor and the old algorithm's logarithmic row-reserve coefficient. It contains +no time constant. + +**Lemma (repair (b)).** Let `ℓ ≥ log2(8σ)` and `L ≥ max(2, 36/δ², 2(4+ℓ)/δ)`, and set `e0 = 2^L`. Let `A_j` +run the stopped construction for `e ≥ e0` and `A_(j−1)` below e0. Then: + +1. `A_j` is defined (the stock fits) for every `e ≥ e0`. +2. `T_j(e) ≤ C_j·V·e^(1−a')` for all `e ≥ 1`, where + `C_j = max(K·(4+M(δ)), C_(j−1)·2^(L·(a'−a)))`. +3. L depends only on δ and σ. The time constants `C_(j−1)`, K and `C_j` never enter it. + +*Proof.* (1) Put `t = log2 e ≥ L`. As in the original lemma, `log2(1+t) ≤ 3√t ≤ δt/2` and +`log2(8σ)+4 ≤ δt/2`, so `8σ(1+t)e^(−δ) ≤ 1/16`. Since `δ ≤ 1−s` and `w ≤ 2e^s`, +`k ≤ 2σe^s(1+t)+1 ≤ (e/4)·8σ(1+t)e^(−(1−s)) + 1 ≤ e/64 + 1 < e/2` for `e ≥ 4`. +(2) For `e ≥ e0`, apply (H2) term by term. `e^(1−s) ≤ e^(1−a')` because `s > a'`. +`e^s(1+t) = e^(1−a')·(1+t)2^(−(1−a'−s)t) ≤ M(δ)·e^(1−a')` by the absorption bound, since `1−a'−s ≥ δ` and M is +decreasing. `w^(1−a) ≤ 2e^(s(1−a)) ≤ 2e^(1−a')` because of the remainder gap. For `1 ≤ e < e0`, +`T_(j−1)(e) ≤ C_(j−1)e^(1−a)·e^(a'−a) ≤ C_(j−1)2^(L(a'−a))·e^(1−a')`. (3) follows from the definition of L. ∎ + +The original lemma's next constant `C_large + C_old·2^(L(a_(j+1)−a_j))` dominates this `C_j`, with +`C_large = K(4+M(δ))`. The induction stays sequential: `σ → L → C_j → (σ_(j+1), next stage)`. + +**Consequence for the selected receipt.** Read with C = 8σ (a space constant) instead of a constant that +dominates the previous time constant, the receipt's formula `max(⌈36/δ²⌉, ⌈2(4+512)/δ⌉)` is an instance of +the restated lemma whenever `8σ_j ≤ 2^512`. In fact each recorded cutoff supports much more. The verifier +computes the exact largest `ℓ` each one admits (`stock_headroom_log2`). It is 6,562,783 bits at stage 1 and +grows by about 1/s per stage, to about 3·10^23 bits at stage 7. Every one of the 14 recorded cutoffs is +therefore a valid fit cutoff for any stock coefficient below 2^6,562,783. The carried time constant stays +finite and does not feed back into L. Under the receipt's own assumption that fresh time constants are below +2^512, the verifier's explicit chain bounds `log2 C_7` by a 27-digit integer. On the other side, the carried +factor alone gives `log2 C_(j−1) ≥ L_(j−1)·Δa_(j−1)`, which already exceeds the stage-j headroom for every +j = 2..7. This reproduces PR #1956's finding from the other side: the lemma *as written* fails exactly at +stages 2–7. + +So, under (H1)–(H3), only the proof text needs to change. The recorded cutoff numbers are valid as they stand. + +## Remaining obligations (not discharged here) + +- **(H3) and the stock coefficient.** The stock coefficient must contain no time constant. Each `σ_j` must + satisfy `log2(8σ_j) ≤ stock_headroom_log2[j]`, which is a margin of millions of bits or more. This rests on + the retained complete-row contract: the old supplier's row reserve is logarithmic, and that bound has the same + shape at every stage, so the below-cutoff branch does not multiply it by `2^(LΔa)`. This package does not + re-derive that contract or compute the actual σ_j. +- **(H2) form.** The retained stopped-leaf estimate is taken with its O-constant K independent of the cutoff, as + PR387 and the weighted induction of FINITE_BIT_ACCOUNTING state it. If any other "sufficiently large e" + condition hides in the inherited primitives (PR185 lineage), it is a further fit condition. It needs its own + coefficient checked against the headroom, and it may not contain a time constant. +- Other lineages (T37's 1024-bit receipts, open PRs #1424, #1586 and #1724) use the same formula. The argument + applies to them verbatim, but their headrooms are not computed here. +- Every other inherited all-size, precision, hosting and analytic obligation of the selected record. + +## Reproduce + +```sh +python3 -B research/bootstrap-cutoff-time-space-split/verify.py +python3 scripts/research_package.py --package research/bootstrap-cutoff-time-space-split --check-only +python3.12 scripts/research_package.py --package research/bootstrap-cutoff-time-space-split +``` + +Expected: `PASS_BOOTSTRAP_TIME_SPACE_SPLIT recorded=14 fit_only_valid=14 written_rule_fails=12 +time_constant_finite=2 controls_rejected=7`, in well under a second, using the standard library only. + +The verifier checks every input against [SOURCES.json](SOURCES.json). It binds the lemma text, the fit statement +in `three-stage-cover-rows.tex` and the assembler formula in the pinned `upstream1087.tar.gz`. It then checks the +following, all in exact rationals: + +- the 14 cutoffs reproduce from the receipt's chain; +- δ never exceeds the stock gap; +- each cutoff satisfies the fit-only rule with the exact headroom (`ℓ` passes and `ℓ+1` fails); +- certified rational lower bounds `ln2 > 693/1000` and `ℯ > 2718/1000`, from series partial sums with tail + bounds; +- the `3√t` step, from `9(ln2)²/2 ≥ 1`; +- the explicit time-constant chain. + +A floating-point check at the true maximizer `t* = 1/(δ ln2) − 1` and on a grid confirms that `M(δ)` dominates +the actual supremum. It is a sanity check, not a certificate. The verifier compares its summary with +[RESULT.json](RESULT.json). + +Seven controls must be rejected: + +1. a recorded cutoff minus one; +2. a stock coefficient one bit above the headroom; +3. `M(δ)/4` in place of `M(δ)`; +4. the false lower bound `ln2 > 0.6932`; +5. the false lower bound `ℯ > 2.719`; +6. the carried time constant put into the fit rule (the lemma as written, at stage 2); +7. a tampered gap. + +## Open next questions + +1. **Compute σ_j for the selected lineage.** Is `log2(8σ_j)` below the recorded headroom at every stage? We + expect it to be far below. *First step:* collect the per-level row stock (`14400w+1`, depth factor, the + `57,604` new contribution in FINITE_BIT_ACCOUNTING) and the old-leaf reserve coefficient from the PR185/#384 + complete-row contract. *Blocked by:* the reserve coefficient is stated only as "logarithmic" in the retained + sources. +2. **Adopt the wording.** If maintainers accept the restated lemma, the proof texts (PR387 PROOF, + FINITE_BIT_ACCOUNTING and their successors) could say "C dominates the stage's stock/fit constants" + instead of "previous ordinary constants". PR #1956's corrected chain would then be needed only by readers who + keep the original wording. *Blocked by:* maintainer decision. Frozen packages are not edited here. + +## Credit + +The cutoff lemma, its 1/16 inequality chain and the next-constant rule are from rohanarun's PR387 PROOF and +eumemic's five-stage bank proof. The borrowing/fit construction is from the retained +`three-stage-cover-rows.tex`. The chain and the 512 allowance are from the frozen PR1087 assembler (Jeremy +Kothe's package and its credited lineage) and Rohan Arun's PR1094 selected receipt. The receipt binding and the +question come from PR #1956 (`bootstrap-cutoff-carry`, same author). Prepared by Josie Elliston with Claude Code +(Claude Opus 5.5) assistance. Apache-2.0. diff --git a/research/bootstrap-cutoff-time-space-split/RESULT.json b/research/bootstrap-cutoff-time-space-split/RESULT.json new file mode 100644 index 0000000000..b4cf2572cc --- /dev/null +++ b/research/bootstrap-cutoff-time-space-split/RESULT.json @@ -0,0 +1,109 @@ +{ + "bootstrap": { + "cutoff_digits": [ + 13, + 19, + 24, + 30, + 35, + 41, + 46 + ], + "stock_headroom_log2": [ + 6562783, + 3917000013, + 2337861697120, + 1395352895343721, + 832816459989422004, + 497066554520932088547, + 296674203132883528250615 + ], + "m_bar_log2_ceil": [ + 19, + 28, + 38, + 47, + 56, + 65, + 74 + ], + "time_log2C_digits": [ + 3, + 10, + 13, + 16, + 19, + 21, + 24, + 27 + ], + "time_log2C_final_sha256": "4ab13a5ce9894525117996ad288c630b28f2938c234e0755046aa4a692cd18cf", + "written_rule_holds": [ + true, + false, + false, + false, + false, + false, + false + ] + }, + "conservative_bootstrap": { + "cutoff_digits": [ + 13, + 19, + 24, + 30, + 35, + 41, + 46 + ], + "stock_headroom_log2": [ + 6562783, + 3917000033, + 2337861713185, + 1395352907315128, + 832816468556900243, + 497066560483357858654, + 296674207198239164557594 + ], + "m_bar_log2_ceil": [ + 19, + 28, + 38, + 47, + 56, + 65, + 74 + ], + "time_log2C_digits": [ + 3, + 10, + 13, + 16, + 19, + 21, + 24, + 27 + ], + "time_log2C_final_sha256": "4714d46e06668e81d1a0028a780e99e9c3901872170d5b77e50cd0243645518c", + "written_rule_holds": [ + true, + false, + false, + false, + false, + false, + false + ] + }, + "controls_rejected": [ + "recorded_cutoff_minus_one", + "stock_coefficient_above_headroom", + "absorption_constant_quartered", + "ln2_lower_bound_too_high", + "e_lower_bound_too_high", + "carried_time_constant_in_fit", + "tampered_gap" + ] +} diff --git a/research/bootstrap-cutoff-time-space-split/SOURCES.json b/research/bootstrap-cutoff-time-space-split/SOURCES.json new file mode 100644 index 0000000000..cc1adb8640 --- /dev/null +++ b/research/bootstrap-cutoff-time-space-split/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bootstrap-depth-audit/sources/pr387/PROOF.md", + "usage": "input", + "git_blob": "915d08efd81fa304e1974e26d8212803e03e6623", + "sha256": "15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "usage": "input", + "git_blob": "2970ef79b0441e937449bed30f68f2e0558186ba", + "sha256": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86" + }, + { + "path": "research/five-stage-source527-banks/proof/FINITE_BIT_ACCOUNTING.md", + "usage": "input", + "git_blob": "42a585d742660f9ed44ebd3ca2a9d1e0832bb0be", + "sha256": "602923520af184670170bf159fde7b4c72e79a72570eddd7746b7c97bc51fc5b" + }, + { + "path": "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + } + ] +} diff --git a/research/bootstrap-cutoff-time-space-split/TASK.json b/research/bootstrap-cutoff-time-space-split/TASK.json new file mode 100644 index 0000000000..eb00d896f8 --- /dev/null +++ b/research/bootstrap-cutoff-time-space-split/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Repair (b) of PR1956: restate the PR387 / FINITE_BIT_ACCOUNTING ordinary-bootstrap cutoff lemma so the cutoff's constant is a stock/fit (space) coefficient only, prove that the stage time bound holds for all widths with the carried constant C_old*2^(L*Delta a) absorbed into the next time constant, and check the selected #1094 receipt's 14 recorded cutoffs against the restated rule.", + "scope_change_reason": "Refined from the card's general all-size implication to one lemma (the finite bootstrap cutoff) on one certificate; chooser nonce bff97872294a70402bf5bd4940f9436f drew complex-mechanisms, overridden by donor/coordinator preference for PR1956's open question 1 (complex-mechanisms already had several sessions in this run and the rank-shape card returned 153 overlap matches).", + "bottleneck_link": "Side result for reliability: the cutoffs are part of the selected record's finite all-size bootstrap witness; kappa does not depend on them. This shows the recorded witness is valid under a restated lemma, so only proof text (not numbers) needs to change, subject to a stock-coefficient obligation with a large margin.", + "budget_minutes": 60, + "stop_rule": "Stop after the restated lemma with proof, the exact fit-only check and headroom of all 14 recorded cutoffs, and controls; do not compute the actual stock coefficients sigma_j or other lineages.", + "outcome": "completed", + "evidence": "README proof of the restated lemma (absorption bound sup (1+t)2^(-delta t) <= max(2, 2/(e ln2 delta)); time bound for all e>=1 with C_j = max(K(4+M), C_(j-1)2^(L Delta a)); fit k=2^L with C=8 sigma). verify.py (stdlib, exact Fractions): 14 recorded cutoffs reproduce and satisfy the fit-only rule; exact stock headroom 6,562,783 bits at stage 1 rising to ~3e23 at stage 7; certified ln2>693/1000, e>2718/1000; carried factor 2^(L Delta a) alone exceeds the stage 2-7 headroom (the lemma as written fails there, matching PR1956); explicit finite time-constant chain (27-digit log2 C_7 under 512-bit fresh constants); 7 rejected controls; RESULT.json pinned.", + "author": "Josie Elliston", + "ai_assistance": "Claude Code (Claude Opus 5.5) wrote the proof note and verifier under the author's direction; arithmetic is exact and self-checked.", + "open_questions": [ + { + "question": "Is log2(8 sigma_j) below the recorded stock headroom at every stage of the selected lineage, i.e. does the old-leaf reserve coefficient contain no time constant?", + "why_it_matters": "It is the only remaining obligation for the recorded cutoffs under the restated lemma.", + "first_step": "Collect the per-level row stock (14400w+1, depth factor, 57,604 new contribution in FINITE_BIT_ACCOUNTING) and the old-leaf reserve coefficient from the PR185/#384 complete-row contract.", + "blocked_by": "The reserve coefficient is stated only as 'logarithmic' in the retained sources." + }, + { + "question": "Should the proof texts adopt the restated wording ('C dominates the stage's stock/fit constants') instead of 'previous ordinary constants'?", + "why_it_matters": "Decides whether PR1956's corrected cutoff chain or this restatement is the record's repair; it affects every lineage using the same formula (T37, #1424, #1586, #1724).", + "first_step": "Maintainer review of this package and PR1956 together.", + "blocked_by": "Maintainer decision; frozen packages are not edited here." + } + ] +} diff --git a/research/bootstrap-cutoff-time-space-split/VERIFY.json b/research/bootstrap-cutoff-time-space-split/VERIFY.json new file mode 100644 index 0000000000..be89fc4b4f --- /dev/null +++ b/research/bootstrap-cutoff-time-space-split/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bootstrap-depth-audit/sources/pr387/PROOF.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz", + "research/five-stage-source527-banks/proof/FINITE_BIT_ACCOUNTING.md", + "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "exact fit-only check and stock headroom of 14 recorded bootstrap cutoffs; certified absorption constant; lemma-as-written failure at stages 2-7; finite time-constant chain; 7 rejected controls; RESULT.json equality" + } + ] +} diff --git a/research/bootstrap-cutoff-time-space-split/verify.py b/research/bootstrap-cutoff-time-space-split/verify.py new file mode 100644 index 0000000000..afea0fc177 --- /dev/null +++ b/research/bootstrap-cutoff-time-space-split/verify.py @@ -0,0 +1,292 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check the time/space split of the ordinary-bootstrap cutoff (repair (b)). + +PR387 PROOF and five-stage FINITE_BIT_ACCOUNTING choose, per bootstrap stage, + + L = ceil(max(1, 36/delta^2, 2*(4+ceil(log2 C))/delta)), + +with C dominating "previous ordinary constants" too. The README proves a +restated lemma: the time bound needs no cutoff, because every lower-order toll +is at most M(delta) * e^(1-a_j) for all e >= 1, so the cutoff only has to make +the borrowed stock fit (k < e/2). The fit constant is a stock/reserve +coefficient. The carried time constant C_old*2^(L*Delta a) only enters the next +stage's time constant. This verifier checks, with exact rationals: + +1. the 14 recorded cutoffs reproduce from the pinned receipt and formula; +2. each satisfies the restated (fit-only) rule with a stock coefficient below + 2^512, and the exact headroom (largest log2 stock coefficient it supports); +3. the absorption constant M(delta) = max(2, 2/(e*ln2*delta)) from certified + rational enclosures of e and ln 2, plus the 3*sqrt(t) step of the lemma; +4. an explicit finite time-constant chain under the receipt's 512-bit + assumption on fresh constants; the carried factor 2^(L*Delta a) alone exceeds + every stage-2..7 headroom (so the lemma as written fails there, as PR1956 + found), while the cutoffs are unaffected. + +Standard library only. The chain and receipt binding follow PR1956 +(research/bootstrap-cutoff-carry). Prepared by Josie Elliston with Claude Code +(Claude Opus 5.5) assistance. +""" +import hashlib +import io +import json +import math +import sys +import tarfile +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' +FBA = 'research/five-stage-source527-banks/proof/FINITE_BIT_ACCOUNTING.md' +ROWS = 'research/five-stage-source527-banks/proof/three-stage-cover-rows.tex' +PR387 = 'research/bootstrap-depth-audit/sources/pr387/PROOF.md' +TARBALL = 'research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz' +ALLOWANCE = 512 # ceil(log2 C) hard-coded by the selected assembler +A0 = Q(384599, 10**10) # completed ordinary starting saving +ETA = BETA = Q(1, 10**24) +BRANCHES = (('bootstrap', 'complex_lower'), + ('conservative_bootstrap', 'conservative_complex_lower')) +LN2_LO = Q(693, 1000) # claimed rational lower bounds, certified below +E_LO = Q(2718, 1000) + + +class AuditError(Exception): + pass + + +def require(ok, msg): + if not ok: + raise AuditError(msg) + + +def ceil(x): + return -(-x.numerator // x.denominator) + + +def floor(x): + return x.numerator // x.denominator + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def load_sources(): + sources = json.loads((HERE / 'SOURCES.json').read_text()) + data = {} + for f in sources['files']: + if f['usage'] != 'input': + continue + raw = (ROOT / f['path']).read_bytes() + require(sha256(raw) == f['sha256'], f"source pin {f['path']}") + data[f['path']] = raw + require(set(data) == {ASSEMBLY, FBA, ROWS, PR387, TARBALL}, 'input set') + return data + + +def bind_text(data): + """The lemma as written, the fit condition it serves, and the assembler formula.""" + fba, pr387 = data[FBA].decode(), data[PR387].decode() + for text in (fba, pr387): + require('previous ordinary constants' in text, 'C dominates the previous constant') + require('36/delta^2' in text, 'quadratic cutoff term') + require('borrowed high part fits' in fba, 'the cutoff also serves the fit') + require('C_large+C_old*2^(L*(a_(j+1)-a_j))' in fba, 'next-constant rule (FBA)') + require('1-c (for row fitting)' in fba, 'stock gap among the minimum') + require('- stock: 1-s.' in pr387, 'stock gap among the minimum (PR387)') + rows = data[ROWS].decode() + for needle in (r'\log_qS(e,w)=O(w\log e)', 'For sufficiently large $e$, $kn} 2^-k/(n+1) + require(lo <= hi and ln2_lo <= lo, 'ln2 lower bound') + elo, f = Q(0), 1 + for k in range(0, 25): + f = f * k if k else 1 + elo += Q(1, f) + require(e_lo <= elo, 'e lower bound') + # log2(1+t) <= 3 sqrt(t) for t >= 0: 2^(3u) >= 1 + (3u ln2)^2/2 >= 1 + u^2. + require(9 * ln2_lo**2 / 2 >= 1, '3*sqrt(t) step') + return dict(ln2=(lo, hi)) + + +def clog2(x): + """Least integer n with 2^n >= x, for a positive rational x.""" + n = x.numerator.bit_length() - x.denominator.bit_length() + while Q(2)**n < x: + n += 1 + while Q(2)**(n - 1) >= x: + n -= 1 + return n + + +def m_bar(delta): + """sup_{t>=0} (1+t) 2^(-delta t) <= max(2, 2/(e ln2 delta)); proof in README.""" + return max(Q(2), 2 / (E_LO * LN2_LO * delta)) + + +def float_sanity(delta, bound): + """Not a certificate: the proved bound dominates the true sup at its maximizer.""" + d, ln2 = float(delta), math.log(2) + ts = [0.0, 1.0, max(0.0, 1 / (d * ln2) - 1)] + [10.0**k for k in range(0, 16)] + for t in ts: + require(math.log1p(t) - d * t * ln2 <= math.log(float(bound)) + 1e-12, f'sup bound at t={t}') + + +def chain(bit, complex_): + s = min(bit, (1 - BETA) * complex_) - Q(1, 10**27) + require(0 < s < Q(1, 2), 'common saving below 1/2') + a, rows = A0, [] + for _ in range(7): + old, a = a, (1 - s) * s + s * a + gaps = (s - a, 1 - a - s, 1 - a - s * (1 - old), 1 - s) + require(all(g > 0 for g in gaps), 'positive gaps') + rows.append(dict(old=old, new=a, gap=min(gaps), stock=1 - s)) + return s, rows + + +def recorded_cutoff(gap, ell): + return max(ceil(36 / gap**2), ceil(2 * (4 + ell) / gap)) + + +def fit_ok(L, gap, ell): + """Restated rule: e >= 2^L makes C(1+log2 e)e^-gap <= 1/16 for log2 C <= ell.""" + return L >= 2 and L * gap**2 >= 36 and L * gap >= 2 * (4 + ell) + + +def audit_branch(record, name, side): + s, rows = chain(Q(record['bit_lower']), Q(record[side])) + rec = record[name] + require(len(rec) == 7, f'{name}: seven stages') + out = [] + for i, (row, item) in enumerate(zip(rows, rec)): + require(Q(item['exponent']) == row['new'] and Q(item['gap']) == row['gap'], f'{name}[{i}] chain') + L = int(item['cutoff_log2']) + require(L == recorded_cutoff(row['gap'], ALLOWANCE), f'{name}[{i}] recorded formula') + require(row['gap'] <= row['stock'], f'{name}[{i}] stock gap covered by delta') + require(fit_ok(L, row['gap'], ALLOWANCE), f'{name}[{i}] fit-only rule') + headroom = floor(L * row['gap'] / 2) - 4 + require(fit_ok(L, row['gap'], headroom) and not fit_ok(L, row['gap'], headroom + 1), + f'{name}[{i}] exact headroom') + out.append(dict(L=L, gap=row['gap'], dA=row['new'] - row['old'], headroom=headroom)) + return out + + +def time_chain(stages, fresh=ALLOWANCE): + """Upper bounds on log2 C_j when fresh time constants and multiplicities are < 2^fresh. + + C_j <= max(K_j (4 + M), C_(j-1) 2^(L Delta a)), K_j <= 2^fresh + 2^fresh C_(j-1). + """ + ell, out = fresh, [] + for st in stages: + M = m_bar(st['gap']) + k = max(fresh, fresh + ell) + 1 + large = k + clog2(4 + M) + carry = ell + ceil(st['L'] * st['dA']) + out.append(dict(prev=ell, large=large, carry=carry)) + ell = max(large, carry) + 1 + out.append(dict(prev=ell)) + return out + + +def summarize(record): + result = {} + for name, side in BRANCHES: + stages = audit_branch(record, name, side) + tc = time_chain(stages) + for st in stages: + float_sanity(st['gap'], m_bar(st['gap'])) + # The lemma as written puts the previous time constant into C. Stage 1: C_0 < 2^512 + # (receipt). Later stages: log2 C_old >= L_(i-1)*Delta a_(i-1) (C_old >= 1, carry alone). + written = [fit_ok(stages[0]['L'], stages[0]['gap'], ALLOWANCE)] + written += [not (prev['L'] * prev['dA'] > st['headroom']) for prev, st in zip(stages, stages[1:])] + require(written[0] and not any(written[1:]), f'{name}: written rule fails exactly at stages 2-7') + result[name] = dict( + cutoff_digits=[len(str(st['L'])) for st in stages], + stock_headroom_log2=[st['headroom'] for st in stages], + m_bar_log2_ceil=[clog2(m_bar(st['gap'])) for st in stages], + time_log2C_digits=[len(str(x['prev'])) for x in tc], + time_log2C_final_sha256=sha256(str(tc[-1]['prev']).encode()), + written_rule_holds=written, + ) + return result + + +def controls(record): + rejected = [] + + def expect(name, fn): + try: + fn() + except AuditError: + rejected.append(name) + else: + raise SystemExit(f'control accepted: {name}') + + def tampered(): + r = json.loads(json.dumps(record)) + r['bootstrap'][4]['cutoff_log2'] = str(int(r['bootstrap'][4]['cutoff_log2']) - 1) + audit_branch(r, 'bootstrap', 'complex_lower') + expect('recorded_cutoff_minus_one', tampered) + + def over_headroom(): + st = audit_branch(record, 'conservative_bootstrap', 'conservative_complex_lower')[2] + require(fit_ok(st['L'], st['gap'], st['headroom'] + 1), 'stock coefficient above headroom') + expect('stock_coefficient_above_headroom', over_headroom) + + def quarter_bound(): + st = audit_branch(record, 'bootstrap', 'complex_lower')[6] + float_sanity(st['gap'], m_bar(st['gap']) / 4) + expect('absorption_constant_quartered', quarter_bound) + + expect('ln2_lower_bound_too_high', lambda: certify_constants(ln2_lo=Q(6932, 10000))) + expect('e_lower_bound_too_high', lambda: certify_constants(e_lo=Q(2719, 1000))) + + def written_rule(): + stages = audit_branch(record, 'bootstrap', 'complex_lower') + carry = floor(stages[0]['L'] * stages[0]['dA']) + require(fit_ok(stages[1]['L'], stages[1]['gap'], carry), 'carried time constant in C') + expect('carried_time_constant_in_fit', written_rule) + + def tampered_gap(): + r = json.loads(json.dumps(record)) + r['bootstrap'][0]['gap'] = str(Q(r['bootstrap'][0]['gap']) * 2) + audit_branch(r, 'bootstrap', 'complex_lower') + expect('tampered_gap', tampered_gap) + return rejected + + +def main(): + data = load_sources() + bind_text(data) + certify_constants() + record = json.loads(data[ASSEMBLY]) + result = summarize(record) + result['controls_rejected'] = controls(record) + expected_path = HERE / 'RESULT.json' + if '--write' in sys.argv: + expected_path.write_text(json.dumps(result, indent=1) + '\n') + require(json.loads(expected_path.read_text()) == result, 'RESULT.json matches') + fails = sum(not x for b, _ in BRANCHES for x in result[b]['written_rule_holds']) + print(f'PASS_BOOTSTRAP_TIME_SPACE_SPLIT recorded=14 fit_only_valid=14 written_rule_fails={fails} ' + f'time_constant_finite=2 controls_rejected={len(result["controls_rejected"])}') + + +if __name__ == '__main__': + try: + main() + except AuditError as e: + raise SystemExit(f'FAIL: {e}') From c9819a94f9c630f8b42ff5c3027965c4ba451653 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 11:19:41 -0400 Subject: [PATCH 2/2] Narrow receipt claim and qualify H2 after independent review Co-Authored-By: Claude Opus 5.5 --- .../README.md | 29 ++++++++++++------- .../TASK.json | 2 +- .../verify.py | 5 ++-- 3 files changed, 23 insertions(+), 13 deletions(-) diff --git a/research/bootstrap-cutoff-time-space-split/README.md b/research/bootstrap-cutoff-time-space-split/README.md index c093680511..59986cb4b0 100644 --- a/research/bootstrap-cutoff-time-space-split/README.md +++ b/research/bootstrap-cutoff-time-space-split/README.md @@ -10,9 +10,11 @@ are not valid instances of the cutoff lemma **as written** in [FINITE_BIT_ACCOUNTING](../five-stage-source527-banks/proof/FINITE_BIT_ACCOUNTING.md). That lemma's C must dominate the "previous ordinary constants". The carried time constant `C_old·2^(L·Δa)` is about twice too large for every stage after the first. PR #1956 left open whether a restated lemma ("repair (b)") makes the recorded -numbers valid. This package answers that question for the time constant: yes. The cutoff has only one real job, -to make the borrowed stock fit. A previous time constant never needs to enter it. What remains is a space -obligation with a large exact margin. +numbers valid. This package answers that question for the time constant: yes, under hypotheses (H1)–(H3) +below, which are read from the retained sources but not re-proved. Under them the cutoff has only one job, to +make the borrowed stock fit, and no previous time constant needs to enter it. The recorded cutoffs then reduce +to a space obligation with a large exact margin. That obligation is **not** discharged, because the actual +stock coefficients σ_j are not computed here. ## The two jobs of the 1/16 condition @@ -49,7 +51,9 @@ Here K is finite and does not depend on e or on the cutoff. K is built from fres the weighted-induction factor `1+1/(1−μ_1)+1/(1−μ_τ)`, scalar/wrapper/padding counts, the stock coefficient inside the high-part exchange) and from `C_(j−1)`, which enters through the ordinary leaves, the remainder, the routing and the high-part exchange. This is the retained stopped-leaf estimate of PR387 with its O-constant -written as K. (H3) `log_q S(e,w) ≤ σ·w·(1+log2 e)`, where σ is a *stock* coefficient. It is built from the +written as K. The sources state it asymptotically ("for large e", `k = o(e)`). Its quantifier "whenever +`k < e/2`" and the independence of K from the cutoff are a reading of those sources, not a quotation. +(H3) `log_q S(e,w) ≤ σ·w·(1+log2 e)`, where σ is a *stock* coefficient. It is built from the per-level row stock, the depth factor and the old algorithm's logarithmic row-reserve coefficient. It contains no time constant. @@ -74,17 +78,21 @@ The original lemma's next constant `C_large + C_old·2^(L(a_(j+1)−a_j))` domin **Consequence for the selected receipt.** Read with C = 8σ (a space constant) instead of a constant that dominates the previous time constant, the receipt's formula `max(⌈36/δ²⌉, ⌈2(4+512)/δ⌉)` is an instance of -the restated lemma whenever `8σ_j ≤ 2^512`. In fact each recorded cutoff supports much more. The verifier +the restated lemma whenever `8σ_j ≤ 2^512`, that is, whenever `σ_j ≤ 2^509`. In fact each recorded cutoff supports much more. The verifier computes the exact largest `ℓ` each one admits (`stock_headroom_log2`). It is 6,562,783 bits at stage 1 and grows by about 1/s per stage, to about 3·10^23 bits at stage 7. Every one of the 14 recorded cutoffs is -therefore a valid fit cutoff for any stock coefficient below 2^6,562,783. The carried time constant stays +therefore a valid fit cutoff for any stock coefficient `σ_j ≤ 2^(H_j−3)`, where `H_j` is that stage's headroom. +At stage 1 this means `σ_1 ≤ 2^6,562,780`. The carried time constant stays finite and does not feed back into L. Under the receipt's own assumption that fresh time constants are below -2^512, the verifier's explicit chain bounds `log2 C_7` by a 27-digit integer. On the other side, the carried +2^512, the verifier's explicit chain bounds `log2 C_7` by a 27-digit integer. That chain also assumes +`K_j ≤ 2^512 + 2^512·C_(j−1)`, which is a modeling assumption stronger than (H2)'s finite K. It only illustrates +finiteness and plays no role in the cutoffs. On the other side, the carried factor alone gives `log2 C_(j−1) ≥ L_(j−1)·Δa_(j−1)`, which already exceeds the stage-j headroom for every j = 2..7. This reproduces PR #1956's finding from the other side: the lemma *as written* fails exactly at stages 2–7. -So, under (H1)–(H3), only the proof text needs to change. The recorded cutoff numbers are valid as they stand. +So, under (H1)–(H3), the recorded cutoff numbers are valid exactly when every `σ_j ≤ 2^(H_j−3)`. If that holds, +only the proof text needs to change. The condition is plausible by a wide margin, but it is not verified here. ## Remaining obligations (not discharged here) @@ -114,7 +122,7 @@ time_constant_finite=2 controls_rejected=7`, in well under a second, using the s The verifier checks every input against [SOURCES.json](SOURCES.json). It binds the lemma text, the fit statement in `three-stage-cover-rows.tex` and the assembler formula in the pinned `upstream1087.tar.gz`. It then checks the -following, all in exact rationals: +following in exact rational arithmetic: - the 14 cutoffs reproduce from the receipt's chain; - δ never exceeds the stock gap; @@ -124,7 +132,8 @@ following, all in exact rationals: - the `3√t` step, from `9(ln2)²/2 ≥ 1`; - the explicit time-constant chain. -A floating-point check at the true maximizer `t* = 1/(δ ln2) − 1` and on a grid confirms that `M(δ)` dominates +The `ℯ` bound needs only a positive partial sum. The quartered-M control (control 3 below) uses the same +floating-point check. A floating-point check at the true maximizer `t* = 1/(δ ln2) − 1` and on a grid confirms that `M(δ)` dominates the actual supremum. It is a sanity check, not a certificate. The verifier compares its summary with [RESULT.json](RESULT.json). diff --git a/research/bootstrap-cutoff-time-space-split/TASK.json b/research/bootstrap-cutoff-time-space-split/TASK.json index eb00d896f8..9ae3cf06b0 100644 --- a/research/bootstrap-cutoff-time-space-split/TASK.json +++ b/research/bootstrap-cutoff-time-space-split/TASK.json @@ -42,7 +42,7 @@ "scope_status": "refined", "actual_scope": "Repair (b) of PR1956: restate the PR387 / FINITE_BIT_ACCOUNTING ordinary-bootstrap cutoff lemma so the cutoff's constant is a stock/fit (space) coefficient only, prove that the stage time bound holds for all widths with the carried constant C_old*2^(L*Delta a) absorbed into the next time constant, and check the selected #1094 receipt's 14 recorded cutoffs against the restated rule.", "scope_change_reason": "Refined from the card's general all-size implication to one lemma (the finite bootstrap cutoff) on one certificate; chooser nonce bff97872294a70402bf5bd4940f9436f drew complex-mechanisms, overridden by donor/coordinator preference for PR1956's open question 1 (complex-mechanisms already had several sessions in this run and the rank-shape card returned 153 overlap matches).", - "bottleneck_link": "Side result for reliability: the cutoffs are part of the selected record's finite all-size bootstrap witness; kappa does not depend on them. This shows the recorded witness is valid under a restated lemma, so only proof text (not numbers) needs to change, subject to a stock-coefficient obligation with a large margin.", + "bottleneck_link": "Side result for reliability: the cutoffs are part of the selected record's finite all-size bootstrap witness; kappa does not depend on them. Under hypotheses H1-H3 read from the retained sources, the recorded cutoffs are valid exactly when each stock coefficient sigma_j <= 2^(headroom_j-3); that condition is plausible by a wide margin but not verified, so this reduces PR1956's failure to an uncomputed space obligation.", "budget_minutes": 60, "stop_rule": "Stop after the restated lemma with proof, the exact fit-only check and headroom of all 14 recorded cutoffs, and controls; do not compute the actual stock coefficients sigma_j or other lineages.", "outcome": "completed", diff --git a/research/bootstrap-cutoff-time-space-split/verify.py b/research/bootstrap-cutoff-time-space-split/verify.py index afea0fc177..ef9a7a4462 100644 --- a/research/bootstrap-cutoff-time-space-split/verify.py +++ b/research/bootstrap-cutoff-time-space-split/verify.py @@ -11,13 +11,14 @@ is at most M(delta) * e^(1-a_j) for all e >= 1, so the cutoff only has to make the borrowed stock fit (k < e/2). The fit constant is a stock/reserve coefficient. The carried time constant C_old*2^(L*Delta a) only enters the next -stage's time constant. This verifier checks, with exact rationals: +stage's time constant. This verifier checks, in exact rationals except where noted: 1. the 14 recorded cutoffs reproduce from the pinned receipt and formula; 2. each satisfies the restated (fit-only) rule with a stock coefficient below 2^512, and the exact headroom (largest log2 stock coefficient it supports); 3. the absorption constant M(delta) = max(2, 2/(e*ln2*delta)) from certified - rational enclosures of e and ln 2, plus the 3*sqrt(t) step of the lemma; + rational lower bounds on e and ln 2, plus the 3*sqrt(t) step of the lemma + (a floating-point check of M at its maximizer is a sanity check only); 4. an explicit finite time-constant chain under the receipt's 512-bit assumption on fresh constants; the carried factor 2^(L*Delta a) alone exceeds every stage-2..7 headroom (so the lemma as written fails there, as PR1956