From 382ce09ec0a4a4afe76d6c398cf344f2aa58b0cd Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:53:32 -0700 Subject: [PATCH 1/4] Scaffold selected BIT-stage stock band package with exact source pins --- .../selected-bit-stage-stock-band/README.md | 35 ++++++++ .../SOURCES.json | 54 ++++++++++++ .../selected-bit-stage-stock-band/TASK.json | 82 +++++++++++++++++++ .../selected-bit-stage-stock-band/VERIFY.json | 26 ++++++ .../selected-bit-stage-stock-band/verify.py | 3 + 5 files changed, 200 insertions(+) create mode 100644 research/selected-bit-stage-stock-band/README.md create mode 100644 research/selected-bit-stage-stock-band/SOURCES.json create mode 100644 research/selected-bit-stage-stock-band/TASK.json create mode 100644 research/selected-bit-stage-stock-band/VERIFY.json create mode 100644 research/selected-bit-stage-stock-band/verify.py diff --git a/research/selected-bit-stage-stock-band/README.md b/research/selected-bit-stage-stock-band/README.md new file mode 100644 index 0000000000..235afd6a1a --- /dev/null +++ b/research/selected-bit-stage-stock-band/README.md @@ -0,0 +1,35 @@ +# selected-bit-stage-stock-band + +**Draft; no new bound claimed.** + +## Scope and evidence + +Original card: `selected-stock-envelope`. Complete [TASK.json](TASK.json), including any scope +change and its connection to the bottleneck. Explain the result and limitations here. +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue are historical provenance, so later priority +updates do not invalidate this package. Explicit --source files are live inputs +and must match their pins. Full Git history is needed to resolve provenance. + +## Reproduce + +After completing the verifier and marking VERIFY.json ready, from repo root: + +```sh +python3 scripts/research_package.py --package research/selected-bit-stage-stock-band --check-only +python3.12 scripts/research_package.py --package research/selected-bit-stage-stock-band +``` + +Declare all external inputs and pinned dependencies in VERIFY.json. The generic +hook is bounded; native/Lean or long replays need an explicit dedicated workflow. + +## Open next questions + +Complete the structured `open_questions` list in TASK.json and explain it here: +the question, why it matters, a feasible first step and any blocker. If no next +question is justified, say so rather than inventing one. + +## Credit + +Prepared by JoyboyBrian. Retain predecessor attribution and source-specific notices. +New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. diff --git a/research/selected-bit-stage-stock-band/SOURCES.json b/research/selected-bit-stage-stock-band/SOURCES.json new file mode 100644 index 0000000000..32fe3baebe --- /dev/null +++ b/research/selected-bit-stage-stock-band/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "notes/three-stage-cover-rows.tex", + "usage": "input", + "git_blob": "590da4b892a08b9d5182fb3d8a983c6239dd27db", + "sha256": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8" + }, + { + "path": "research/joint-helper-lattice/PROOF.md", + "usage": "input", + "git_blob": "e41106031da41fade7a7419c17a32c1bd9aa103b", + "sha256": "43ef4251cc300f1b18cbe8cdb060f96f95748e6797d2478b4c04b79a8373ef91" + }, + { + "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "usage": "input", + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "input", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + } + ] +} diff --git a/research/selected-bit-stage-stock-band/TASK.json b/research/selected-bit-stage-stock-band/TASK.json new file mode 100644 index 0000000000..db13404de6 --- /dev/null +++ b/research/selected-bit-stage-stock-band/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md", + "research/stock-margin-chain/README.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "scope_change_reason": null, + "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "budget_minutes": 150, + "stop_rule": "TODO", + "outcome": "in-progress", + "evidence": "TODO", + "author": "JoyboyBrian", + "ai_assistance": "TODO: disclose tools used", + "open_questions": [ + { + "question": "TODO", + "why_it_matters": "TODO", + "first_step": "TODO", + "blocked_by": "TODO" + } + ] +} diff --git a/research/selected-bit-stage-stock-band/VERIFY.json b/research/selected-bit-stage-stock-band/VERIFY.json new file mode 100644 index 0000000000..d9d39c3275 --- /dev/null +++ b/research/selected-bit-stage-stock-band/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "draft", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "notes/three-stage-cover-rows.tex", + "research/joint-helper-lattice/PROOF.md", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/query-thinned-controllers/PROOF.md", + "research/query-thinned-controllers/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "TODO: identity, positive fixture and failure controls" + } + ] +} diff --git a/research/selected-bit-stage-stock-band/verify.py b/research/selected-bit-stage-stock-band/verify.py new file mode 100644 index 0000000000..56d0fa1e0e --- /dev/null +++ b/research/selected-bit-stage-stock-band/verify.py @@ -0,0 +1,3 @@ +#!/usr/bin/env python3 +"""Replace this draft with a scoped verifier and meaningful controls.""" +raise SystemExit("DRAFT: no research result has been verified") From a9172f35827139fdb0ab9283769b16ef771bdddd Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:55:31 -0700 Subject: [PATCH 2/4] Prove two-sided parent stock envelope and exact fit band for the selected BIT stage --- .../selected-bit-stage-stock-band/PROOF.md | 166 ++++++++++++++++++ 1 file changed, 166 insertions(+) create mode 100644 research/selected-bit-stage-stock-band/PROOF.md diff --git a/research/selected-bit-stage-stock-band/PROOF.md b/research/selected-bit-stage-stock-band/PROOF.md new file mode 100644 index 0000000000..50ba408ec7 --- /dev/null +++ b/research/selected-bit-stage-stock-band/PROOF.md @@ -0,0 +1,166 @@ +# Proof: two-sided parent stock and the exact fit band of the selected BIT stage + +This is a scoped written proof about the selected record #4470 at base +`cef4b52f2a59009865bf8eabde1be3f159063703`. It is not a complete +multiplication theorem. Every claim below concerns the **source reserve +prescription** of the delayed-cover BIT producer. It makes no claim about +every possible implementation of the BIT supplier. + +## 0. The selected stage and its source prescription + +The selected BIT side has one ordinary conversion stage. The delayed-cover +producer (uniform saving `C1 = 69/20000` after cover) is stopped at atom width +`w = ceil(e^delta)` and uses the retained old ordinary supplier +(`a_old = 384599/10^10`) at its leaves. The resulting ordinary saving is + + (1-delta)*C1 + delta*a_old = 0.0034363538396, delta = 1/250. + +Source bindings, all byte-pinned in `SOURCES.json`: + +* `research/query-thinned-controllers/RESULT.json`: `ordinary_BIT.atom = 1/250`, + `bit_strictification.uniform_N = 2^25986965159937` (so `H1 = log2 N = + 25986965159937`), and the prime rule `odd q > 2^26*N^5`. +* `research/query-thinned-controllers/PROOF.md` §4 changes the atom to 0.004. + It substitutes the compiled constants into "the delayed-cover stock formulas" + with `w=ceil(e^0.004)`. +* `research/joint-helper-lattice/PROOF.md` (#4470) retains that BIT stage with + atom exponent 0.004. +* `research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md` §8 and + `BIT-ALLSIZE-PARAMETERS.json` `stock` define the reserve: + + W(w) = B*|GL_N(F_q)|*q^(N^2*(w-1)), + S(e,w) = W(w)^D * S_old, D = D_N(ceil(e/w)) = floor(log_N ceil(e/w)), + k <= D*(N^2*(w-1) + ceil(log_q(B*|GL_N(F_q)|))) + ceil(log_q S_old) + 1, + + The source text says to "borrow `k= 1`, odd prime `q`, integer `B >= 1` and integers +`e, w >= 1`, + + D*N^2*w <= k_par <= D*(N^2*w + c_B). + +*Proof.* `G = q^(N^2) * prod_{j=1..N} (1 - q^(-j))`. The product is below one +and at least `1 - sum_{j>=1} q^(-j) = 1 - 1/(q-1) >= 1/2 > 1/q` for `q >= 3`. +Hence `q^(N^2-1) < G < q^(N^2)`. + +Then `B*G > q^(N^2-1)` gives `ceil(log_q(BG)) >= N^2`. Since `B <= q^(c_B)`, +`B*G < q^(N^2+c_B)` gives `ceil(log_q(BG)) <= N^2 + c_B`. Multiply +`N^2(w-1) + [N^2, N^2+c_B]` by `D >= 0`. ∎ + +The lower bound is the high-matrix lift together with one full low chart per +live level. It does not use `S_old`, `B` or the size of `q` beyond `q >= 3`. + +## 2. Lemma (depth classification) + +Let `N >= 2` and keep the notation above. Since `n = ceil(e/w)` we have +`(n-1)*w < e <= n*w`. + +(a) `D = 0` iff `n < N`. Then `k_par = 0`, and the producer runs no cover + level. + +(b) If `D >= 1` and `n <= 2*D*N^2`, then `k_par >= e/2`, so the prescription + is infeasible whatever `S_old` is. In particular: + * Every `D = 1` width (`N <= n < N^2`) has `k_par >= N^2*w > (N^2-1)*w >= n*w >= e`. + The prescription asks for more digits than the chunk has. + * Every `D = 2` width with `n <= 4N^2` is infeasible. + + *Proof.* `k_par >= D*N^2*w >= (n/2)*w >= e/2`. + +(c) If `c_B <= N^2` and `n >= 8*D*N^2 + 1`, then `k_par < e/4`. + + *Proof.* `k_par <= D*(N^2*w + N^2) <= 2*D*N^2*w`, and + `e > (n-1)*w >= 8*D*N^2*w >= 4*k_par`. For `D = 0` we have `k_par = 0 < e/4`. + +(d) If `N >= 64`, every `D >= 3` width satisfies `n >= N^D >= 8*D*N^2 + 1`. + + *Proof.* `N^(D-2) >= 64^(D-2) >= 8D+1`. This holds at `D=3` (`64 >= 25`), + and `64*(8D+1) >= 8(D+1)+1` gives the induction step. + +So for `N >= 64` and `c_B <= N^2`: +* the prescription is infeasible for all `N <= n <= 4N^2`; +* it is feasible on the parent side (`k_par < e/4`) for all `n >= 16N^2+1`; +* the undetermined window is `4N^2 < n <= 16N^2`, all of which lies at `D = 2`. + +## 3. Theorem (selected width bands) + +Take the selected values `N = 2^H1`, `H1 = 25986965159937` and `delta = 1/250`. +Put `t = log2 e` (a real number, since `e` is an integer width). + +1. **No parent stock.** If `(249/250)*t <= H1 - 1`, i.e. `t <= 26091330481863`, + then `D = 0` and `k_par = 0`. Here `n <= e^(1-delta) + 1 <= N/2 + 1 < N`. +2. **Infeasible band.** If `H1 + 1 <= (249/250)*t <= 2*H1 + 1`, i.e. + `26091330481866 <= t <= 52182660963729` after integer rounding of the + endpoints inward, then `k_par >= e/2`. The source reserve cannot be borrowed + at any such width, for any `B >= 1`, any odd prime `q`, any `S_old >= 1` and + any admissible larger depth `D' >= D`. + + *Proof.* `w <= e^delta + 1 <= 2*e^delta`, so + `n >= e/w >= e^(1-delta)/2 >= 2^H1 = N`. Also `w >= e^delta`, so + `n <= e^(1-delta) + 1 <= 2^(2H1+1) + 1 <= 4N^2`. Now apply 2(b). A larger + `D'` only increases the lower envelope `D'*N^2*w`. +3. **Fit.** If `(249/250)*t >= 2*H1 + 6`, i.e. `t >= 52182660963735`, and + `c_B <= N^2`, then `k_par < e/4`. If in addition `k_old <= e/4`, the full + prescription borrows `k < e/2` digits. + + *Proof.* `n >= e^(1-delta)/2 >= 2^(2H1+5) = 32N^2 >= 16N^2 + 1`. Since + `n >= N^2`, `D >= 2`. If `D = 2`, apply 2(c). If `D >= 3`, apply 2(d) + and then 2(c). + +Therefore the least width from which the source's stated reserve fits lies +strictly between `t = 52182660963729` and `t = 52182660963735`. The proved +sufficient guard and the proved obstruction are six bits of `log2 e` apart. +The predecessor estimate "`log2 e ≈ 2 log2 N/(1-δ) = 5.2183·10^13`" (#4612) +is thus correct to within this window. The new content is the matching +**lower** side and the band below it. + +The band is wide. The rank-N uniform word first becomes applicable at +`t ≈ 2.609·10^13`, but its stock fits only from `t ≈ 5.218·10^13`. For about +`2.609·10^13` bits of `log2 e`, the selected producer must not be run as +prescribed. That includes **every** width at which it would execute exactly one +cover level. In that band the conversion must call the retained supplier +directly, as `three-stage-cover-rows.tex` permits for small widths. This is a +fixed threshold, so the exponent `0.0034363538396` is unaffected. The finding is +a precise domain statement, not a counterexample to the selected κ. + +## 4. Hypotheses on the two remaining factors + +* `c_B <= N^2`, i.e. `B <= q^(N^2)`. It is needed only on the fit side. It + holds if the chosen prime exceeds `B`, which the finite prime-avoidance rule + permits because only finitely many primes are excluded. It also follows from + the inherited nested-width bound `log2 B < N^2` used in + `research/lockstep-live-role-audit/constant_c.py` (#4436 realization). That + bound is cited, not re-derived here. +* `k_old <= e/4`. It is needed only on the fit side. The source calls `S_old` + a logarithmic reserve. Under any envelope + `log_q S_old <= sigma_old*(1 + log2 e)` it holds at `t >= 52182660963735` + whenever `sigma_old <= 2^(t-3)/(1+t)`. For example the lockstep-live-role + audit's assumed `log2 S_old <= 2^64 * e^delta * log2 e` is far inside this + range. The numerical value of `S_old` is **not** derived here. The + infeasibility statements need only `S_old >= 1`. + +## 5. What is not claimed + +* No new κ, supplier admission, frontier change or implementation of the BIT + word. The word of rank `2^25986965159937` is not materialized. +* Infeasibility is a statement about the source prescription `W(w)^D S_old` + (and any larger admissible depth). It does not prove that another cover + design could not run in the band. +* The outer reserve constant `C`, the complex row stock, tape, precision and + analytic premises remain inherited. From fd207148aadf1817f5ac7f25dd875d1e71266c5d Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 20:58:37 -0700 Subject: [PATCH 3/4] Add exact verifier, reduced-rank oracle, controls and receipt for the BIT-stage stock band --- .../selected-bit-stage-stock-band/RESULT.json | 38 ++ .../selected-bit-stage-stock-band/verify.py | 328 +++++++++++++++++- 2 files changed, 364 insertions(+), 2 deletions(-) create mode 100644 research/selected-bit-stage-stock-band/RESULT.json diff --git a/research/selected-bit-stage-stock-band/RESULT.json b/research/selected-bit-stage-stock-band/RESULT.json new file mode 100644 index 0000000000..b60342825f --- /dev/null +++ b/research/selected-bit-stage-stock-band/RESULT.json @@ -0,0 +1,38 @@ +{ + "H1": 25986965159937, + "band_width_log2e": 26091330481864, + "controls_rejected": [ + "feasible_single_level", + "fit_one_bit_early", + "no_high_matrix_lift", + "rank_off_by_one", + "roles_above_q_to_N2", + "stale_atom_3_over_1000", + "tampered_bridge" + ], + "delta": "1/250", + "first_fit_witness": 52182660963750, + "fit_min_log2e": 52182660963735, + "infeasible_max_log2e": 52182660963729, + "infeasible_min_log2e": 26091330481866, + "last_infeasible_witness": 52182660963500, + "lemma_2d_depths_checked": 397, + "models": { + "D0": 1512, + "D1_over_chunk": 5040, + "fit_2c": 164556, + "infeasible_2b": 46368, + "instances": 432000 + }, + "no_parent_stock_max_log2e": 26091330481863, + "old_leaf_log_coefficient_allowance_log2_at_fit": 52182660963686, + "reduced_rank_oracle_witnesses": 869, + "status": "PASS_SELECTED_BIT_STAGE_STOCK_BAND", + "window_bits": 6, + "witness_counts": { + "D0": 10, + "fits": 23, + "infeasible": 50, + "undetermined": 0 + } +} diff --git a/research/selected-bit-stage-stock-band/verify.py b/research/selected-bit-stage-stock-band/verify.py index 56d0fa1e0e..925f55a8ae 100644 --- a/research/selected-bit-stage-stock-band/verify.py +++ b/research/selected-bit-stage-stock-band/verify.py @@ -1,3 +1,327 @@ #!/usr/bin/env python3 -"""Replace this draft with a scoped verifier and meaningful controls.""" -raise SystemExit("DRAFT: no research result has been verified") +"""Two-sided parent stock envelope and exact fit band for the selected #4470 BIT stage. + +Checks PROOF.md: source bindings, exhaustive small-rank models of the source +borrowed-digit formula, exact witnesses at the selected rank N=2^H1, and +rejection controls. Standard library only. Apache-2.0. +JoyboyBrian, with substantial assistance from Anthropic Claude (Claude Code). +""" +import argparse +import hashlib +import json +from fractions import Fraction as Q +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DELTA = Q(1, 250) + +BRIDGE = 'research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md' +PARAMS = 'research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json' +QT_RESULT = 'research/query-thinned-controllers/RESULT.json' +QT_PROOF = 'research/query-thinned-controllers/PROOF.md' +JH_PROOF = 'research/joint-helper-lattice/PROOF.md' +ROWS = 'notes/three-stage-cover-rows.tex' +SELECTED = 'certificates/selected-result.json' + +STOCK = { + 'borrowed_digits': 'k <= D_N(ceil(e/w))*(N^2*(w-1)+ceil(log_q(B*|GL_N(F_q)|)))+ceil(log_q S_old)+1', + 'depth_bound': 'D_N(n)=floor(log_N n) for rank<=floor(n/N) children; any larger explicit integer bound is safe.', + 'reserve': 'S(e,w)=W(w)^D_N(ceil(e/w))*S_old(e,w)', + 'role_divisor': 'W(w)=B*|GL_N(F_q)|*q^(N^2*(w-1))', +} +PHRASES = { + BRIDGE: ['A safe reserve is `W(w)^D * S_old`', 'For sufficiently large `e`, borrow `k ordinary and delta < 1 - ordinary, 'adapter and stock exponent gaps') + stock = json.loads(data[PARAMS])['stock'] + for key, text in STOCK.items(): + need(stock[key] == text, 'stock formula ' + key) + for path, phrases in PHRASES.items(): + text = data[path].decode('utf-8') + for phrase in phrases: + need(phrase in text, 'source sentence in ' + path) + return H1, delta + + +# ---------------------------------------------------------------- source formula, exact integers +def ilog(N, n): + """floor(log_N n) for n >= 1.""" + D, p = 0, N + while p <= n: + D, p = D + 1, p * N + return D + + +def ceil_log(q, x): + c, p = 0, 1 + while p < x: + c, p = c + 1, p * q + return c + + +def gl_order(N, q): + out = 1 + for i in range(N): + out *= q**N - q**i + return out + + +def det_mod(m, q): + m = [row[:] for row in m] + n, det = len(m), 1 + for c in range(n): + piv = next((r for r in range(c, n) if m[r][c] % q), None) + if piv is None: + return 0 + if piv != c: + m[c], m[piv], det = m[piv], m[c], -det + det = det * m[c][c] % q + inv = pow(m[c][c], -1, q) + for r in range(c + 1, n): + f = m[r][c] * inv % q + m[r] = [(a - f * b) % q for a, b in zip(m[r], m[c])] + return det % q + + +def brute_gl(N, q): + from itertools import product + return sum(1 for e in product(range(q), repeat=N * N) + if det_mod([list(e[i * N:(i + 1) * N]) for i in range(N)], q)) + + +def k_parent(N, chart_digits, e, w, lift=True): + """Source parent stock D*(N^2(w-1)+ceil(log_q(B|GL_N(F_q)|))); chart_digits is the ceiling.""" + n = -(-e // w) + D = ilog(N, n) + lift_digits = N * N * (w - 1) if lift else 0 + return D * (lift_digits + chart_digits), D, n + + +def model_checks(lift=True, roles=None, E=2000, W=6, envelope=True, role_hypothesis=True): + """Lemmas 1 and 2(a)-(c) on every (N,q,B,w,e) of a finite grid.""" + for N, q in ((2, 3), (2, 5), (3, 3)): + need(brute_gl(N, q) == gl_order(N, q), 'GL order formula') + counts = {'instances': 0, 'D0': 0, 'D1_over_chunk': 0, 'infeasible_2b': 0, 'fit_2c': 0} + for N in (2, 3, 4): + for q in (3, 5, 7): + G = gl_order(N, q) + need(q**(N * N - 1) < G < q**(N * N), 'GL order brackets') + for B in (roles or (1, 2, 1000, q**(N * N))): + cB, chart = ceil_log(q, B), ceil_log(q, B * G) + for w in range(1, W + 1): + for e in range(1, E + 1): + k, D, n = k_parent(N, chart, e, w, lift) + counts['instances'] += 1 + need((n - 1) * w < e <= n * w, 'atom count') + if envelope: + need(D * N * N * w <= k <= D * (N * N * w + cB), 'two-sided envelope') + if D == 0: + need(n < N and k == 0, 'D=0 has no parent stock') + counts['D0'] += 1 + if D == 1: + need(k > e, 'every D=1 width overdraws the chunk') + counts['D1_over_chunk'] += 1 + if D >= 1 and n <= 2 * D * N * N: + need(2 * k >= e, 'infeasible for n <= 2DN^2') + counts['infeasible_2b'] += 1 + if (cB <= N * N or not role_hypothesis) and n >= 8 * D * N * N + 1: + need(4 * k < e, 'parent fit for n >= 8DN^2+1') + counts['fit_2c'] += 1 + need(all(counts.values()), 'every lemma branch is exercised') + return counts + + +def high_depth_check(N=64, top=400): + need(all(N**(D - 2) >= 8 * D + 1 for D in range(3, top)), 'Lemma 2(d)') + return top - 3 + + +# ---------------------------------------------------------------- selected scale +def bands(H1, delta): + s = 1 - delta + floor = lambda x: x.numerator // x.denominator + ceil = lambda x: -((-x.numerator) // x.denominator) + return {'no_parent_stock_max_log2e': floor(Q(H1 - 1) / s), + 'infeasible_min_log2e': ceil(Q(H1 + 1) / s), + 'infeasible_max_log2e': floor(Q(2 * H1 + 1) / s), + 'fit_min_log2e': ceil(Q(2 * H1 + 6) / s)} + + +def fit_derivation(H1, slack): + """Theorem 3.3 step: (1-delta)t >= 2H1+slack gives n >= 2^(2H1+slack-1) >= 16N^2+1. + + In log2 units with N=2^H1 this is 2^(slack-1) >= 16 + 2^(-2H1).""" + return Q(2)**(slack - 1) >= 16 + Q(1, 2**min(2 * H1, 4096)) + + +def witness(H1, t, a=250): + """Exact parent stock at e=2^t, a|t, atom 1/a: returns (D, infeasible, fits) for c_B <= N^2.""" + need(t % a == 0, 'witness exponent') + u = t // a # w = 2^u, n = 2^(t-u) exactly + D = (t - u) // H1 # floor(log_N n) + if D == 0: + return 0, False, True + x = t - 1 - 2 * H1 - u # lower D*N^2*w >= 2^(t-1) <=> D >= 2^x + infeasible = x <= 0 or (x < 64 and D >= 2**x) + y = t - 2 - 2 * H1 - u # upper D*N^2*(w+1) < 2^(t-2) <=> D < 2^y (u huge) + fits = y > 0 and (y >= 64 or D < 2**y) + need(not (infeasible and fits), 'witness consistency') + return D, infeasible, fits + + +def oracle_checks(): + """Materialize e=2^t at reduced ranks N=2^H1 and atoms 1/a; compare witness() with big integers.""" + compared = 0 + for H1, a, top in ((2000, 250, 16000), (3, 2, 400), (5, 3, 600), (6, 4, 900), (7, 5, 900)): + N = 2**H1 + b = bands(H1, Q(1, a)) + for t in range(a, top + 1, a): + e, w = 2**t, 2**(t // a) + n = -(-e // w) + D = ilog(N, n) + low, high = D * N * N * w, D * (N * N * w + N * N) + got = witness(H1, t, a) + need(got == (D, D >= 1 and 2 * low >= e, D == 0 or 4 * high < e), 'witness oracle at t=%d' % t) + if b['infeasible_min_log2e'] <= t <= b['infeasible_max_log2e']: + need(got[1], 'reduced-rank band is infeasible') + if t >= b['fit_min_log2e'] and H1 >= 6: + need(got[2], 'reduced-rank fit') + compared += 1 + return compared + + +def selected_checks(H1, delta): + b = bands(H1, delta) + need(delta == Q(1, 250), 'selected atom') + need(fit_derivation(H1, 6) and not fit_derivation(H1, 5), 'fit slack 6 is the least integer this derivation admits') + need(2 + Q(1, 2**4096) <= 4, 'band top: n <= 2^(2H1+1)+1 <= 4N^2') + span = lambda lo, hi: range(lo - lo % 250 + 250, hi - hi % 250 + 1, 250) + lo, hi, fit, z = b['infeasible_min_log2e'], b['infeasible_max_log2e'], b['fit_min_log2e'], b['no_parent_stock_max_log2e'] + seen = {'D0': 0, 'infeasible': 0, 'fits': 0, 'undetermined': 0} + for t in list(span(z - 2500, z)): + D, bad, ok = witness(H1, t) + need(D == 0, 'no parent stock below the band') + seen['D0'] += 1 + edges = [*span(lo - 1, lo + 2500), *span(hi - 2500, hi), *span(H1 * 3 // 2, H1 * 3 // 2 + 2500)] + for t in edges: + D, bad, ok = witness(H1, t) + need(1 <= D <= 2 and bad, 'infeasible band witness at t=%d' % t) + seen['infeasible'] += 1 + last_bad, first_ok = None, None + for t in span(hi - 5000, fit + 5000): + D, bad, ok = witness(H1, t) + if t >= fit: + need(ok, 'fit witness at t=%d' % t) + if bad: + last_bad = t + if ok and first_ok is None: + first_ok = t + seen['fits' if ok else 'infeasible' if bad else 'undetermined'] += 1 + need(last_bad is not None and first_ok is not None and last_bad < first_ok, 'single transition') + need(hi < first_ok and last_bad <= hi + 250 and first_ok <= fit + 250, 'transition inside the proved window') + for t in (3 * H1 * 250 // 249 + 250, 10**15, 10**18): + t -= t % 250 + D, bad, ok = witness(H1, t) + need(D >= 3 and ok, 'D>=3 witness fits') + seen['fits'] += 1 + sigma_old_log2 = fit - 3 - (1 + fit).bit_length() + return dict(b, witness_counts=seen, last_infeasible_witness=last_bad, first_fit_witness=first_ok, + band_width_log2e=hi - lo + 1, window_bits=fit - hi, + old_leaf_log_coefficient_allowance_log2_at_fit=sigma_old_log2) + + +def run(override=None, lift=True): + data = load_sources(override) + H1, delta = bind(data) + result = {'status': 'PASS_SELECTED_BIT_STAGE_STOCK_BAND', 'H1': H1, 'delta': str(delta), + 'models': model_checks(lift=lift), 'lemma_2d_depths_checked': high_depth_check(), + 'reduced_rank_oracle_witnesses': oracle_checks()} + result.update(selected_checks(H1, delta)) + return result + + +def controls(): + """Every control must be rejected.""" + rejected = {} + def expect_fail(name, thunk): + try: + thunk() + except ValueError as exc: + rejected[name] = str(exc) + return + raise SystemExit('FAIL: control accepted: ' + name) + expect_fail('tampered_bridge', lambda: load_sources({BRIDGE: lambda raw: raw.replace(b'k Date: Thu, 22 Oct 2026 20:59:35 -0700 Subject: [PATCH 4/4] Document selected BIT-stage stock band result, metadata and open questions --- .../selected-bit-stage-stock-band/README.md | 160 +++++++++++++++--- .../selected-bit-stage-stock-band/TASK.json | 36 ++-- .../selected-bit-stage-stock-band/VERIFY.json | 22 ++- 3 files changed, 184 insertions(+), 34 deletions(-) diff --git a/research/selected-bit-stage-stock-band/README.md b/research/selected-bit-stage-stock-band/README.md index 235afd6a1a..78f06e0376 100644 --- a/research/selected-bit-stage-stock-band/README.md +++ b/research/selected-bit-stage-stock-band/README.md @@ -1,35 +1,157 @@ -# selected-bit-stage-stock-band +# Selected BIT stage: two-sided parent stock and the exact fit band -**Draft; no new bound claimed.** +**Scoped written proof with exact finite checks; no new κ.** The subject is +the current selected record #4470 (κ = 60403/20000000, base +`cef4b52f2a59009865bf8eabde1be3f159063703`). We look at its one ordinary-BIT +bootstrap stage: the delayed-cover BIT producer of uniform rank +`N = 2^H1`, `H1 = 25986965159937`, stopped at atom width `w = ceil(e^(1/250))` +with old ordinary leaves. That stage gives the ordinary saving +`0.0034363538396`. Its source stock prescription (DELAYED-COVER-BRIDGE §8, +`BIT-ALLSIZE-PARAMETERS.json` `stock`) borrows -## Scope and evidence + k = D*(N^2*(w-1) + ceil(log_q(B*|GL_N(F_q)|))) + ceil(log_q S_old) + 1, + D = floor(log_N ceil(e/w)), -Original card: `selected-stock-envelope`. Complete [TASK.json](TASK.json), including any scope -change and its connection to the bottleneck. Explain the result and limitations here. -Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). -The selected record and catalogue are historical provenance, so later priority -updates do not invalidate this package. Explicit --source files are live inputs -and must match their pins. Full Git history is needed to resolve provenance. +high digits, and needs `k < e/2` "for sufficiently large `e`". -## Reproduce +## Result + +Write `k_par` for the parent (cover) part and `n = ceil(e/w)`. +[PROOF.md](PROOF.md) proves: + +1. **Two-sided envelope.** `D*N^2*w <= k_par <= D*(N^2*w + ceil(log_q B))` + for every `N >= 1`, odd prime `q`, `B >= 1` and `e, w >= 1`. +2. **Depth classification** (`N >= 64`; the fit side also needs `c_B <= N^2`): + * `D = 0` has no parent stock. + * Every `D = 1` width overdraws the chunk: `k_par > e`. + * Every width with `n <= 4N^2` is infeasible. + * Every width with `n >= 16N^2+1` has `k_par < e/4`. This includes all + widths with `D >= 3`. +3. **Selected bands**, with `t = log2 e`: + + | `t` (bits) | parent stock | status of the source prescription | + |---|---|---| + | `<= 26091330481863` | `D = 0`, `k_par = 0` | no cover level runs | + | `26091330481866 ..= 52182660963729` | `k_par >= e/2` | **infeasible** for every `B`, `q`, `S_old` and every larger admissible depth | + | `>= 52182660963735` | `k_par < e/4` | fits, given `c_B <= N^2` and `k_old <= e/4` | + +So the least width at which the stated reserve can be borrowed lies in a +six-bit window of `log2 e`. #4612's estimate `≈ 5.2183·10^13` is confirmed, +and now has a matching lower side. The uniform word becomes applicable at +`t ≈ 2.609·10^13` (`n >= N`), but its stock fits only from `t ≈ 5.218·10^13`. +That leaves a band of `26091330481864` bits in which the producer must not be +run as prescribed, including **every** single-cover-level width. There the +conversion has to call the retained old supplier directly, which +`three-stage-cover-rows.tex` allows for small widths. + +The threshold is fixed, so the exponent and κ are unchanged. This is a domain +statement about the source's "sufficiently large `e`", not a counterexample. +The infeasibility side uses only the high-matrix lift and one full low chart +per level. It needs no hypothesis about `S_old`, `B` or the prime beyond +`q >= 3`. + +**Separating parent stock from inner borrowing.** The band's lower side does +not depend on the old-leaf factor at all. On the fit side, `S_old` (called the +"inherited old-leaf … logarithmic reserve" in the source) only has to obey +`log_q S_old <= sigma_old*(1+log2 e)` with +`log2 sigma_old <= 52182660963686` at the fit point. Its numerical value is +**not** derived here. + +## Evidence and checks -After completing the verifier and marking VERIFY.json ready, from repo root: +`verify.py` (stdlib, about 0.4 s) does the following: + +* **Source binding.** It authenticates all seven pinned inputs. It reads `H1`, + the atom `1/250`, the prime rule and the stage saving from + `query-thinned-controllers/RESULT.json`. It requires the exact stock formula + strings and the cited source sentences. +* **Small-rank models.** It checks Lemmas 1 and 2(a)–(c) exhaustively on + 432,000 instances (`N ∈ {2,3,4}`, `q ∈ {3,5,7}`, four role counts, + `w <= 6`, `e <= 2000`), using exact `|GL_N(F_q)|`. Three of these orders are + confirmed by brute-force enumeration. It also checks Lemma 2(d) for + `D = 3..399` at `N = 64`. +* **Selected-rank witnesses.** It evaluates exact witnesses at `e = 2^t`, + `250 | t`, for the selected `N`, using integer exponent arithmetic. They + cover the bands, the D=1 band, `D >= 3`, and every multiple of 250 within + 5000 bits of the transition. The last infeasible witness + (`52182660963500`) and the first fitting one (`52182660963750`) bracket the + proved window. +* **Reduced-rank oracle.** The witness shortcut is compared with fully + materialized big integers at reduced ranks (`H1 ∈ {3,5,6,7,2000}`, several + atoms), over 869 widths. +* **Rejection controls**, all of which must fail: + * a tampered bridge byte; + * omitting the high-matrix lift (the D=1 overdraw then fails); + * role count above `q^(N^2)`; + * the stale atom `3/1000`; + * a rank off by one; + * a fit slack one bit too small; + * claiming a single-cover-level width fits. + + The stored [RESULT.json](RESULT.json) receipt must match exactly. + +Mutation tests were done on the author's side: a doubled D=1 inequality, fit +slack 5, a tighter fit lemma, a shifted documented threshold and off-by-one +witness exponents. Each one makes the verifier fail. + +## Reproduce ```sh +python3.12 -I -W error -B research/selected-bit-stage-stock-band/verify.py +python3.12 -I -O -W error -B research/selected-bit-stage-stock-band/verify.py python3 scripts/research_package.py --package research/selected-bit-stage-stock-band --check-only -python3.12 scripts/research_package.py --package research/selected-bit-stage-stock-band +python3.12 -B scripts/research_package.py --package research/selected-bit-stage-stock-band ``` -Declare all external inputs and pinned dependencies in VERIFY.json. The generic -hook is bounded; native/Lean or long replays need an explicit dedicated workflow. +`verify.py --write NEW_PATH` writes a fresh receipt and never overwrites one. + +## Limits + +* No supplier replay, no Lean, and no selected-frontier or κ change. The + rank-`2^25986965159937` word is not materialized. +* Infeasibility concerns the source prescription `W(w)^D S_old` (and any + larger admissible depth). A different cover design is not excluded. +* The two fit-side hypotheses are not derived. `c_B <= N^2` holds if the prime + is also chosen above `B`, and follows from the inherited nested-width bound + used by `lockstep-live-role-audit`. The old-leaf stock value is the other + hypothesis. +* The outer reserve constant `C`, the complex row stock, and the tape, + precision and analytic premises are all inherited. ## Open next questions -Complete the structured `open_questions` list in TASK.json and explain it here: -the question, why it matters, a feasible first step and any blocker. If no next -question is justified, say so rather than inventing one. +1. **Derive the old-leaf reserve `S_old` numerically from the retained + completed-leaf contract.** It is the last factor of the selected stage's + stock that is not numerically derived. It also replaces the + `log2 A_old <= 64` assumption in `lockstep-live-role-audit`. As a first + step, trace which old-supplier calls (weighted leaves, peeled atoms, cover + routes) run while the parent rows are borrowed. Then decide whether the + PR185 wording "no *external* extra stock" makes `S_old = 1` admissible. + The blocker is that the old supplier's own reserve formula is outside the + pinned #4470 notes. +2. **Should the source text name the band?** The bridge says "for sufficiently + large `e`". A precise statement would say that the stage runs only from + `log2 e >= 52182660963735` and calls the retained supplier directly below + that. As a first step, a maintainer should decide whether to record the + threshold beside the #4470 review. This needs a maintainer decision; the + pinned sources are left unchanged here. +3. **Close the six-bit window.** The exact least fitting width depends on + `c_B` and the precise `S_old`. As a first step, fix `B` (from the compiler + realization) and redo Lemma 2(c) with the exact chart digits. This is + blocked on the same two factors. ## Credit -Prepared by JoyboyBrian. Retain predecessor attribution and source-specific notices. -New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. +zxv: #4359 and the delayed-cover bridge, stock formula and finite compiler. +Cinna Davis and zxv: the #4440/#4470 chain, including the atom change to +`0.004`. Mark (Matarener): #4612, the δ-generic upper envelope and the +`5.2183·10^13` estimate, and `lockstep-live-role-audit`, the outer `C` and the +`A_old` assumption. The `three-stage-cover-rows` authors and the PR185 +completed-leaf lineage retain their attribution. Earlier +selected-stock-envelope packages (`selected-bootstrap-stock-audit`, +`stock-margin-chain`, `selected-stock-sharp-integer`) concern the historical +#1094 chain. They are cited for context only. + +Prepared by JoyboyBrian with substantial assistance from Anthropic Claude +(Claude Code, Opus 5.5). No independent human or proof-assistant review is +claimed. Apache-2.0. diff --git a/research/selected-bit-stage-stock-band/TASK.json b/research/selected-bit-stage-stock-band/TASK.json index db13404de6..03014babd2 100644 --- a/research/selected-bit-stage-stock-band/TASK.json +++ b/research/selected-bit-stage-stock-band/TASK.json @@ -61,22 +61,34 @@ } ] }, - "scope_status": "unchanged", - "actual_scope": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", - "scope_change_reason": null, - "bottleneck_link": "TODO: explain the causal connection or label this as a side result", + "scope_status": "refined", + "actual_scope": "At the current selected #4470 record, the one ordinary-BIT bootstrap stage (delayed-cover producer, N=2^25986965159937, atom 1/250, old ordinary leaves): a two-sided parent stock envelope D*N^2*w <= k_par <= D*(N^2*w+ceil(log_q B)), a depth classification of feasibility, and exact selected log2-width bands in which the source reserve W(w)^D*S_old is infeasible or fits.", + "scope_change_reason": "The card starting points concern the historical #1094 seven-stage chain; #4470 replaces it with one delayed-cover BIT conversion. #4612 already supplies the upper O(w log e) envelope with an illustrative threshold and lockstep-live-role-audit the outer constant C, so this package takes the uncovered matching lower side and the exact width domain of the selected stage, keeping the old-leaf factor S_old as an explicit hypothesis.", + "bottleneck_link": "Binds the selected stage stock coefficients (N^2 per digit-level, depth floor(log_N n)) and the width domain of the source sufficiently-large-e clause; it is an implementation-obligation audit with no kappa effect.", "budget_minutes": 150, - "stop_rule": "TODO", - "outcome": "in-progress", - "evidence": "TODO", + "stop_rule": "Finish the two-sided envelope, the depth classification and exact selected bands with finite checks and controls; stop before deriving S_old numerically, changing source text, or any supplier, caller or frontier work.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py (source binding, 432000 exhaustive small-rank instances, selected-rank exact witnesses, 869 reduced-rank big-integer oracle widths, 7 rejection controls); RESULT.json receipt.", "author": "JoyboyBrian", - "ai_assistance": "TODO: disclose tools used", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", "open_questions": [ { - "question": "TODO", - "why_it_matters": "TODO", - "first_step": "TODO", - "blocked_by": "TODO" + "question": "What numerical old-leaf reserve S_old does the retained completed-leaf contract supply at the selected BIT stage; is S_old=1 admissible?", + "why_it_matters": "It is the last non-numerical factor of the selected stage stock and replaces the log2 A_old<=64 assumption in lockstep-live-role-audit.", + "first_step": "Trace which old-supplier calls (weighted leaves, peeled atoms, cover routes) run while parent rows are borrowed, and test the PR185 no-external-stock wording against them.", + "blocked_by": "The old supplier reserve formula is outside the pinned #4470 notes." + }, + { + "question": "Should the selected source state the BIT stage domain log2 e >= 52182660963735 instead of sufficiently large e?", + "why_it_matters": "Every single-cover-level width is infeasible; the stage must call the retained supplier directly over a 2.6e13-bit band.", + "first_step": "Maintainer decides whether to record the threshold next to the #4470 review.", + "blocked_by": "Maintainer decision; pinned sources are not edited here." + }, + { + "question": "Where exactly in the six-bit window does the selected prescription first fit?", + "why_it_matters": "Turns a sufficient/obstruction pair into an exact threshold.", + "first_step": "Fix B from the compiler realization and recompute Lemma 2(c) with exact chart digits.", + "blocked_by": "Numerical B and S_old." } ] } diff --git a/research/selected-bit-stage-stock-band/VERIFY.json b/research/selected-bit-stage-stock-band/VERIFY.json index d9d39c3275..cfd34f3603 100644 --- a/research/selected-bit-stage-stock-band/VERIFY.json +++ b/research/selected-bit-stage-stock-band/VERIFY.json @@ -1,6 +1,6 @@ { "schema_version": 1, - "status": "draft", + "status": "ready", "python": "3.12", "requirements": [], "inputs": [ @@ -16,11 +16,27 @@ { "argv": [ "{python}", + "-I", + "-W", + "error", "-B", "{package}/verify.py" ], - "timeout_seconds": 120, - "checks": "TODO: identity, positive fixture and failure controls" + "timeout_seconds": 60, + "checks": "Source hashes and sentences, exhaustive small-rank lemmas, selected-rank exact witnesses, reduced-rank big-integer oracle, seven rejection controls and exact receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same acceptance with optimization enabled (no assert-based checks)." } ] }