Bound the selected #4470 BIT-stage stock on both sides: every single-cover-level width overdraws, fit from log2 e = 52182660963735 (no new κ)

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<e/2` high digits" "for sufficiently large
+  `e`". The parameters file states that "any larger explicit integer bound is
+  safe" for D.
+* `notes/three-stage-cover-rows.tex` (a #4470 proof supplement) says that
+  `S_old` is the "inherited old-leaf reserve" with a "logarithmic reserve" and
+  that "small widths use the retained supplier directly".
+
+Write `n = ceil(e/w)`, `G = |GL_N(F_q)|` and `c_B = ceil(log_q B)`. The
+**parent stock** is the part that the cover recursion takes from the borrowed
+row:
+
+    k_par = D*(N^2*(w-1) + ceil(log_q(B*G))).
+
+The **inner (old-leaf) stock** is `k_old = ceil(log_q S_old) + 1`. The
+prescription borrows `k = k_par + k_old` digits from the original chunk of
+`e` radix-q digits. It is feasible exactly when `k < e/2`.
+
+## 1. Lemma (two-sided parent envelope)
+
+For every integer `N >= 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.

research/selected-bit-stage-stock-band/README.md

@@ -0,0 +1,157 @@
+# Selected BIT stage: two-sided parent stock and the exact fit band
+
+**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
+
+    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)),
+
+high digits, and needs `k < e/2` "for sufficiently large `e`".
+
+## 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
+
+`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 -B scripts/research_package.py --package research/selected-bit-stage-stock-band
+```
+
+`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
+
+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
+
+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.

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
+ }
+}