diff --git a/research/bit-stock-band-threshold/PROOF.md b/research/bit-stock-band-threshold/PROOF.md new file mode 100644 index 0000000000..ccfbdcbb24 --- /dev/null +++ b/research/bit-stock-band-threshold/PROOF.md @@ -0,0 +1,233 @@ +# Proof: the six-bit window of the selected BIT stage's stock fit closes + +Scoped written proof with exact finite checks. No new kappa, supplier admission or +frontier change. Every claim concerns the **source reserve prescription** of the +delayed-cover BIT producer at the one ordinary-BIT stage that PR #4954 analyses. It +says nothing about other implementations of that supplier. + +## 0. Setting, hypotheses and what is cited + +The stage has rank `N = 2^H1` with `H1 = 25986965159937` and atom exponent `1/250` +(pinned in `research/query-thinned-controllers/RESULT.json`). For an integer width +`e >= 1` the source prescription (DELAYED-COVER-BRIDGE section 8, +`BIT-ALLSIZE-PARAMETERS.json` `stock`) is + + w = ceil(e^(1/250)), n = ceil(e/w), D = floor(log_N n), + cG = ceil(log_q(B*|GL_N(F_q)|)), + k = D*(N^2*(w-1) + cG) + k_old, k_old = ceil(log_q S_old) + 1, + +with `q` an odd prime and `B >= 1` an integer. It borrows `k` high digits and **fits** +exactly when `k < e/2`, that is `2k < e`. Write `k_par = D*(N^2*(w-1) + cG)`, +`c_B = ceil(log_q B)`, `t = log2 e` and `A = 250`. + +Two hypotheses are used on the fit side only. + +* **(HB)** `c_B <= N^2`. This is the hypothesis of #4954. The open PR #7101 derives + `c_B <= 2^(H1+13) <= N^2` from the inherited nested-width bound. That derivation is + cited and not replayed here. +* **(Hold)** `k_old <= N^2`. PR #4970 shows `S_old = 1`, so `k_old = 1`, and gives + the conservative fallback `k_old <= 103`. Both readings satisfy (Hold). Neither is + re-derived here. + +The infeasibility statements need none of these: only `B >= 1`, `q >= 3` and +`k_old >= 0`. + +Constants, all exact rationals: + + t* = 250*(2*H1 + 2)/249 = 500*(H1 + 1)/249 = 52182660963730.923694779116465863... + t** = 250*(2*H1 + 3)/249 = t* + 250/249 = 52182660963731.927710843373493975... + tau = 2^(-2*10^11). + +## 1. Lemma 1 (chart envelope; PR #4954 Lemma 1) + +For every `N >= 1`, odd prime `q` and `B >= 1`: `N^2 <= cG <= N^2 + c_B`. + +*Proof.* `|GL_N(F_q)| = q^(N^2) * prod_{j=1..N}(1 - q^(-j))`. The product is below +one and at least `1 - 1/(q-1) >= 1/2 > 1/q`, so `q^(N^2-1) < |GL| < q^(N^2)`. Then +`B*|GL| > q^(N^2-1)` gives `cG >= N^2`, and `B <= q^(c_B)` gives +`B*|GL| < q^(N^2+c_B)`, so `cG <= N^2 + c_B`. QED + +Write `delta_B = cG - N^2`, so `0 <= delta_B <= c_B`. + +## 2. Lemma 2 (exact criterion at depth two; new) + +If `D = 2`, that is `N^2 <= n < N^3`, then `k = 2*N^2*w + 2*delta_B + k_old` and + + the prescription fits if and only if e > 4*N^2*w + 4*delta_B + 2*k_old. + +Hence: + +* **(a)** if `e <= 4*N^2*w`, it does not fit, for every `B`, `q` and `S_old`; +* **(b)** under (HB) and (Hold), if `e > 4*N^2*w + 6*N^2`, it fits. + +*Proof.* `k = 2*(N^2*(w-1) + N^2 + delta_B) + k_old`, so `2k = 4*N^2*w + 4*delta_B ++ 2*k_old`, and `2k < e` is the displayed inequality. For (a), `2k >= 4*N^2*w >= e`. +For (b), `4*delta_B + 2*k_old <= 4*N^2 + 2*N^2`. QED + +## 3. Lemma 3 (other depths; PR #4954 Lemma 2) + +* **(a)** If `D = 1` it does not fit, for every `B`, `q`, `S_old`. Here `n <= N^2 - 1`, + so `e <= n*w < N^2*w <= k_par`. +* **(b)** If `D >= 3`, `N >= 64`, (HB) and (Hold), it fits, with `k_par < e/4`. + +*Proof of (b).* `N^(D-2) >= 64^(D-2) >= 8*D + 1` for `D >= 3` (true at `D = 3`, and +`64*(8D+1) >= 8(D+1) + 1` gives the step), so `n >= N^D >= 8*D*N^2 + 1`. Then +`e > (n-1)*w >= 8*D*N^2*w`. By Lemma 1 and (HB), `k_par <= D*(N^2*w + N^2) <= +2*D*N^2*w`, so `4*k_par < e`. Also `e > 8*D*N^2 >= 24*N^2` gives `k_old <= N^2 < e/4`. +Hence `k < e/2`. QED + +## 4. Lemma 4 (from `log2 e` to integer comparisons; new) + +Let `e` be an integer width with `t/250 >= 2*10^11 + 3`, and put `rho = e^(-1/250) = +2^(-t/250)`. By definition `e^(1/250) <= w < e^(1/250) + 1 = e^(1/250)*(1 + rho)`. Write +`u = e^(249/250)/(4*N^2) = 2^(249*(t - t*)/250)`, which uses `249*t*/250 = 2*H1 + 2`. + +* **(a)** If `t <= t*`, then `e <= 4*N^2*w`. +* **(b)** If `t >= t* + tau`, then `e > 4*N^2*w + 6*N^2`. +* **(c)** If `t >= t*`, then `n >= 2*N^2`, so `D >= 2`. +* **(d)** If `t <= t**`, then `e <= 8*N^2*w`. If `t >= t** + tau`, then + `8*N^2*w + 8*N^2 < e`. +* **(e)** For `e = 2^t` with integer `t`, `D >= k` if `249*t - 250*k*H1 >= 1`, and + `D < k` if `249*t - 250*k*H1 <= -1`. + +*Proof.* (a) `u <= 1` gives `e^(249/250) <= 4*N^2`, so `e <= 4*N^2*e^(1/250) <= +4*N^2*w`. + +(b) Since `w < e^(1/250) + 1`, `4*N^2*w + 6*N^2 < 4*N^2*e^(1/250) + 10*N^2`. This is at +most `e` when `e^(249/250) >= 4*N^2 + 10*N^2*rho`, that is when `u >= 1 + 2.5*rho` +(multiply by `e^(1/250)` and use `e^(1/250)*rho = 1`). Now `t >= t* + tau` gives `u >= +2^(249*tau/250) >= 1 + 0.69*tau`, using `2^x >= 1 + x*ln 2`. The number `t*/250` is at +least `2*10^11 + 3`, so `4*rho <= 2^(-2*10^11 - 1) <= tau`. Hence `0.69*tau >= 2.5*rho`. + +(c) `n >= e/w >= e^(249/250)/(1 + rho) >= 4*N^2/2`. + +(d) The same two steps with `8*N^2` for `4*N^2`: `e^(249/250) <= 8*N^2` gives `e <= +8*N^2*w`; and `8*N^2*(w + 1) < 8*N^2*e^(1/250) + 16*N^2 <= e` when `u' >= 1 + 2*rho` +for `u' = e^(249/250)/(8*N^2)`, which `t >= t** + tau` gives as above. + +(e) `e/w <= n <= e/w + 1`, with `e^(249/250)/(1 + rho) <= e/w <= e^(249/250)`. If +`249*t - 250*k*H1 >= 1` then `e^(249/250) >= N^k*2^(1/250)`, so `n >= N^k*2^(1/250)/(1 + rho) +>= N^k`. If it is at most `-1` then `n <= N^k*2^(-1/250) + 1 < N^k`, because `N^k >= 370`. +QED + +## 5. Theorem (the window closes) + +For the selected `N`, `A = 250`: + +* **(T1)** Every integer width `e` with `D >= 1` and `log2 e <= t*` fails to fit, for + every `B >= 1`, odd prime `q` and `S_old >= 1`, and for every larger admissible depth. +* **(T2)** Under (HB) and (Hold), every integer width with `log2 e >= t* + tau` fits. +* **(T3)** Consequently the least width `e_fit` such that every width `e >= e_fit` fits + satisfies `t* < log2 e_fit <= t* + 2*tau`. The window left by #4954 had `log2 e` between + `52182660963729` and `52182660963735`; it now has width at most `2*2^(-2*10^11)` around + `t* = 500*(H1 + 1)/249 = 52182660963730.9236947791...`, independent of `B` and of + `S_old` within (HB) and (Hold). +* **(T4)** For widths `e = 2^t` with integer `t`: every `t` from `26091330481865` + (the first with depth at least one; #4954 states `...866` conservatively) through `52182660963730` does not fit, and every + `t >= 52182660963731` fits under (HB) and (Hold). +* **(T5)** The sufficient guard `k_par < e/4` that #4954 used fails for `D >= 1` and + `log2 e <= t**` and holds for `log2 e >= t** + tau` under (HB); at integer `t` the + threshold is `52182660963732` (it fails at `52182660963731`). + +*Proof.* (T1): if `D = 1`, Lemma 3(a). If `D >= 2`, then `k_par >= D*N^2*w >= +2*N^2*w` by Lemma 1, and `t <= t*` gives `e <= 4*N^2*w` by Lemma 4(a), so `2k >= e`. +A larger depth only increases `k_par`. + +(T2): by Lemma 4(c), `D >= 2`. If `D = 2`, Lemma 4(b) and Lemma 2(b). If `D >= 3`, +Lemma 3(b) (`N = 2^H1 >= 64`). + +(T3): widths with `t* - 1 <= log2 e <= t*` have `D >= 2` (the argument of Lemma 4(c) +loses one bit: `n >= 4*N^2*2^(-1)/(1 + rho) >= N^2`), so they fail by (T1); hence +`e_fit > 2^(t*)`. By (T2) every integer `e >= 2^(t* + tau)` fits, so `e_fit <= +ceil(2^(t* + tau))`, and `log2 ceil(x) <= log2 x + 1.45/x` with `x = 2^(t* + tau)` far +below `tau`. + +(T4): `t = 52182660963730` is below `t*` by `0.9237`; `t = 52182660963731` is above it +by `0.0763 >> tau`. For the integer `t` the verifier makes the same decision with exact +integers: `e = 2^t` satisfies `(A-1)*t <= A*(2*H1 + 2)` (infeasible), or +`(e - 10*N^2)^A >= (4*N^2)^A * e` (fit), because the ratio of the two sides is +`2^((A-1)*t - A*(2*H1+2)) * (1 - 10*N^2/e)^A` with exponent margin at least `1` and +`10*N^2/e <= 1/1000`, where `(1000/999)^250 < 2`. The depth at `e = 2^t` follows from +Lemma 4(e), since `249*t - 250*k*H1` is never zero for the `t` used. + +(T5): same as (T1), (T2) with Lemma 4(d); at depth one `k_par > e`; depth three and +beyond by Lemma 3(b). QED + +## 6. What the verifier checks + +`verify.py` (standard library, about two seconds) does the following. + +1. **Sources.** It authenticates the six pinned inputs by SHA-256, reads `H1` and the + atom `1/250` from the selected-stage result, matches the four stock-formula strings + of the parameters file, and requires the cited sentences of the bridge, #4954's proof + and README, and #4970's README (including the open "six-bit window" question). +2. **Lemma 1.** The `GL` order bounds and `N^2 <= cG <= N^2 + c_B` for 170 cases over + `N` in 2..5 and `B = q^j, q^j + 1`. +3. **Lemma 2.** All 336,636 depth-two instances in `N in {2,3,4,5}`, `q in {3,5,7}`, + `k_old in {1,2,5}` and every width of depth two: the source formula's fit decision + equals `e > 4*N^2*w + 4*delta_B + 2*k_old` in each. +4. **Lemma 3(b).** `N^(D-2) >= 8*D + 1` for `D = 3..399` at `N = 64`. +5. **Lemma 4 in exact integers.** For `N in {8,16,32}` and atom denominators `A in + {2,3,4,5}` it scans the widths around (and, up to 150000, all below) the two edges + `e^(A-1) <= (4*N^2)^A` and `(e - 10*N^2)^A >= (4*N^2)^A * e`. On every width the + best reading of the formula (`delta_B = 0`, `k_old = 1`) fails below the first edge and + the worst reading (`delta_B = N^2`, `k_old = N^2`) fits above the second. The scans + are exhaustive from `e = 1` where marked in `RESULT.json` (`e_lo = 1`); the others + are windowed 300 widths below the first edge and above the second. +6. **Exact transition at large rank.** For `N = 2^h` with `(h, A)` in `(40,2)`, `(41,3)`, + `(51,5)`, `(59,11)`, `(100,2)`, `(101,3)` it computes, with exact big integers and block + by block in `w`, the least width from which every width of depth two fits. It does so + for the best reading (`delta_B = 0`, `k_old = 1`) and the worst reading (`delta_B = N^2`, + `k_old = N^2`), and checks that both lie in the bracket between the two edges. The best + reading sits `4*N^2` to `8*N^2` above the infeasible edge and the worst `10*N^2` to + `18*N^2`, a relative offset of order `1/w`. This is the regime of the selected stage, in + which `w` is huge, at ranks small enough to evaluate. +7. **Selected rank.** Exact integer comparisons give `t*`, `t**`, the integer split at + `52182660963730 | 52182660963731` (and `52182660963731 | 52182660963732` for the + guard), the depth-one onset `t = 26091330481865`, the margin + `t*/250 >= 2*10^11 + 3`, and a table of `t = 52182660963724 .. + 52182660963738` with the depth and both decisions. +8. **Controls.** Ten rejection controls: a tampered selected rank; an off-by-one, a + dropped-chart-excess and a factor-two version of the depth-two criterion; an inflated + infeasible edge in the translation scans and in the large-rank check, and a deflated fit + edge in the translation scans; a shifted rank that + must change the table; a fit claim at `52182660963730` and an infeasible claim at + `52182660963731`. Each must be rejected. Every check raises, so `python -O` does not + skip it. + +The stored `RESULT.json` is the exact receipt that `verify.py --write` regenerates. + +## 7. What is not claimed + +* No new kappa, supplier admission, frontier change, or materialisation of the rank + `2^25986965159937` word. The decision is arithmetic in the exponent of `2`. +* The result is for the **source prescription** with the exact depth + `D = floor(log_N ceil(e/w))`. The parameters file allows "any larger explicit integer + bound"; the infeasible side holds for it, the fit side as stated does not. +* (HB) and (Hold) are cited hypotheses. The derivation of `c_B <= N^2` in #7101 and of + `S_old = 1` in #4970 are not replayed here. +* The remaining window around `t*` has width at most `2^(-2*10^11)` in `log2 e`. Its + exact resolution depends on the realised `B`, the chart excess and the ceiling in + `w`; this package does not decide it. +* The sources pinned here are the #4470 stage of #4954. #7101 states that the same + rank is retained by the later `frontier6030` BIT stage; that statement is not + checked here, and nothing is claimed about the current selected record beyond the + shared parameters used above. +* The tail steps of Lemma 4 are real-analysis inequalities proved above. The verifier + checks their integer constants and runs the same chain exactly at small parameters; it + does not evaluate `2^(5*10^13)`-sized numbers. + +## Open next questions + +1. **Larger admissible depth.** The parameters file allows any larger explicit bound + `D' >= D`. Replacing `D` by `D'` in Lemma 2 moves the first edge to + `250*(2*H1 + log2(2*D'))/249`. Which bound does the compiled prescription use, and + where does the fit start for it? *First step:* read the depth bound in the compiled + stock formula. *Blocked by:* the bound is not pinned in the sources used here. +2. **Exact remaining window.** Can the last `2^(-2*10^11)`-wide window be decided? + *First step:* fix `q` and `B` from the compiler realisation and find the block of + `w = ceil(e^(1/250))` that contains `4*N^2*w`. *Blocked by:* `B` is not materialised. +3. **Current selected record.** Does the later `frontier6030`/`frontier7000` BIT stage use + the same rank, atom exponent and stock formula, so that `t*` applies to it as stated? + *First step:* compare its stage record with `query-thinned-controllers/RESULT.json`. + *Blocked by:* the comparison needs that stage's source bindings, not attempted here. diff --git a/research/bit-stock-band-threshold/README.md b/research/bit-stock-band-threshold/README.md new file mode 100644 index 0000000000..5a21f6421e --- /dev/null +++ b/research/bit-stock-band-threshold/README.md @@ -0,0 +1,113 @@ +# The six-bit fit window of the selected BIT stage closes at log2 e = 500(H1+1)/249 + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exact finite checks. No new kappa, supplier +admission or frontier change.** It answers open question 3 of +[PR #4954](https://github.com/CrocSwap/integer-mult-bounds/pull/4954) ("Close the +six-bit window"), which is also the first open question of the open PR #7101. + +## Result + +At the one ordinary-BIT stage that #4954 analyses (rank `N = 2^H1`, `H1 = 25986965159937`, +atom exponent `1/250`), the source prescription borrows + +```text +k = D*(N^2*(w-1) + ceil(log_q(B*|GL_N(F_q)|))) + k_old, w = ceil(e^(1/250)), +D = floor(log_N ceil(e/w)), and it fits exactly when k < e/2. +``` + +#4954 proved that it does not fit for `log2 e <= 52182660963729` and that its stricter +guard `k_par < e/4` holds from `log2 e = 52182660963735`, leaving a six-bit window. With +`S_old = 1` from [PR #4970](https://github.com/CrocSwap/integer-mult-bounds/pull/4970) +the window closes. + +At depth two the criterion is exact: the prescription fits iff +`e > 4*N^2*w + 4*delta_B + 2*k_old`, where `delta_B` is the chart excess in `[0, c_B]`. +With `t* = 500*(H1+1)/249 = 52182660963730.9236947791...`: + +| statement | range of `log2 e` | hypotheses | +|---|---|---| +| does not fit (depth at least one) | `<= t*` | none beyond `B >= 1`, `q >= 3` | +| fits | `>= t* + 2^(-2*10^11)` | `c_B <= N^2` and `k_old <= N^2` | + +So the least width from which every larger width fits has `log2` in +`(t*, t* + 2*2^(-2*10^11)]`, whatever `B` and `S_old` are within those bounds. + +At the integer widths `e = 2^t`, which are the ones #4954 tabulated: + +| `t` | 52182660963729 | ...730 | ...731 | ...732 | ...734 | ...735 | +|---|---|---|---|---|---|---| +| `k < e/2` (this package) | no | no | **fits** | fits | fits | fits | +| `k_par < e/4` guard | no | no | no | **holds** | holds | holds | +| #4954 (proved) | no | open | open | open | open | fits | + +The fit entries assume `c_B <= N^2` and `k_old <= N^2`; the `no` entries assume nothing +beyond `B >= 1` and `q >= 3`. The guard of #4954 therefore moves from `52182660963735` to `52182660963732`, which +answers the question of #7101 for the `e/4` form, and with `S_old = 1` the guard is not +needed at all: the stated reserve fits from `52182660963731`. Below the threshold the +conversion has to call the retained supplier directly, as #4954 already said; only the +location of the threshold is new. + +## Evidence + +`PROOF.md` proves the criterion, the translation from `log2 e` to integer comparisons +(Lemma 4) and the theorem. `verify.py` (standard library, about two seconds) authenticates the +pinned sources, checks 170 envelope cases and 336,636 depth-two instances of the +source formula against the criterion, scans the exact-integer translation chain on twelve +`(N, A)` pairs, computes the exact least fitting width with big integers at six ranks +between `2^40` and `2^101` (it lies `4N^2` to `18N^2` above the infeasible edge, a relative +offset of order `1/w`), evaluates exact exponent arithmetic at the selected rank, and runs ten +rejection controls. It matches the stored `RESULT.json`, which `verify.py --write` +regenerates. + +## Reproduce + +From the repository root, with CPython 3.12: + +```sh +python3.12 -I -W error -B research/bit-stock-band-threshold/verify.py +python3.12 -I -O -W error -B research/bit-stock-band-threshold/verify.py +python3.12 -B scripts/research_package.py --package research/bit-stock-band-threshold +``` + +Each verifier run prints `PASS_BIT_STOCK_BAND_THRESHOLD`. No Lean, Docker or selected +cold replay is run. + +## Limitations + +* The result is for the **source prescription** with the exact depth + `D = floor(log_N ceil(e/w))`. The parameters file allows a larger explicit depth bound; + the infeasible side holds for it and the fit side as stated does not. +* `c_B <= N^2` (#4954; derived for this stage in the open #7101) and `k_old <= N^2` + (#4970, `k_old = 1` or at most 103) are cited hypotheses, not replayed. +* A window of width at most `2*2^(-2*10^11)` in `log2 e` remains around `t*`. Its exact + resolution depends on the realised `B` and on the ceiling in `w`. +* The sources pinned here are the #4470 stage of #4954. #7101 states that the same rank + is retained by the later `frontier6030` stage. That statement is not checked here. +* The decision is arithmetic in the exponent of `2`. No rank-`2^25986965159937` word is + built, and the work claims no multiplication bound. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +1. **Compiled depth bound.** Which depth bound does the compiled prescription use, and + where does the fit start if it exceeds `floor(log_N ceil(e/w))`? First step: read it + in the compiled stock formula; the first edge moves to `250*(2*H1 + log2(2*D'))/249`. + Blocked by: that bound is not pinned in the sources used here. +2. **Last window.** Can the window of width `2*2^(-2*10^11)` be decided exactly? First + step: fix `q` and `B` from the compiler realisation. Blocked by: `B` is not + materialised. +3. **Current selected record.** Does the later `frontier6030`/`frontier7000` BIT stage use + the same rank, atom and stock formula? First step: compare its stage record with + `research/query-thinned-controllers/RESULT.json`. Blocked by: the later stage's source + bindings are not pinned here. + +## Credit + +JoyboyBrian: PR #4954, the stock formula analysis, Lemmas 1 and 2 re-proved here, the band +and the open question. James Reed: PR #4970, `S_old = 1`. unpaidmoon: the open PR #7101, +the bound `c_B <= 2^(H1+13)` (cited, not replayed). Mark (Matarener): the nested-width +bound used there. The source stock formula is DELAYED-COVER-BRIDGE section 8 and the +selected-stage parameters are those of `research/query-thinned-controllers`. diff --git a/research/bit-stock-band-threshold/RESULT.json b/research/bit-stock-band-threshold/RESULT.json new file mode 100644 index 0000000000..b200a61cb3 --- /dev/null +++ b/research/bit-stock-band-threshold/RESULT.json @@ -0,0 +1,332 @@ +{ + "H1": 25986965159937, + "atom_denominator": 250, + "controls": { + "deflated_fit_edge_rejected": true, + "factor_two_criterion_rejected": true, + "fit_below_threshold_rejected": true, + "ignored_chart_excess_rejected": true, + "infeasible_above_threshold_rejected": true, + "inflated_infeasible_edge_rejected": true, + "inflated_large_rank_edge_rejected": true, + "off_by_one_criterion_rejected": true, + "shifted_rank_changes_table": true, + "tampered_selected_rank_rejected": true + }, + "deeper_depth_checks": 397, + "depth_one_onset_t": 26091330481865, + "depth_two_instances": 336636, + "envelope_cases": 170, + "large_rank_transitions": { + "columns": [ + "h", + "A", + "best_minus_edge_milli_N2", + "worst_minus_edge_milli_N2", + "fit_edge_minus_edge_milli_N2" + ], + "rows": [ + [ + 40, + 2, + 8000, + 18000, + 19999 + ], + [ + 41, + 3, + 4000, + 14000, + 14999 + ], + [ + 51, + 5, + 4000, + 10000, + 12499 + ], + [ + 59, + 11, + 4000, + 10000, + 10999 + ], + [ + 100, + 2, + 8000, + 18000, + 19999 + ], + [ + 101, + 3, + 4000, + 14000, + 14999 + ] + ] + }, + "schema": "bit-stock-band-threshold/1", + "selected_table": [ + { + "depth": 1, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963724 + }, + { + "depth": 1, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963725 + }, + { + "depth": 1, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963726 + }, + { + "depth": 1, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963727 + }, + { + "depth": 1, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963728 + }, + { + "depth": 2, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963729 + }, + { + "depth": 2, + "k_lt_e_over_2": "infeasible", + "k_par_lt_e_over_4": "fails", + "t": 52182660963730 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "fails", + "t": 52182660963731 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963732 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963733 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963734 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963735 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963736 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963737 + }, + { + "depth": 2, + "k_lt_e_over_2": "fits", + "k_par_lt_e_over_4": "holds", + "t": 52182660963738 + } + ], + "sources": { + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/selected-bit-stage-stock-band/PROOF.md": "b93430458a861ae26d41a544f25b6bf3b89ca3693793e27b51e2a49c4e80d507", + "research/selected-bit-stage-stock-band/README.md": "b2bf296410af55bd83cfed8cdb385074737d511528985dbe1bc221ddf6da94c8", + "research/selected-old-leaf-reserve/README.md": "f6d288a36fe18f50eb6d7ecc5ce367e7b3e22d8ab1aecd8c07f2c9090a9dc05f" + }, + "t_star_k_lt_e_over_2": { + "decimal": "52182660963730.923694779116465863453815261044", + "floor": 52182660963730, + "fraction": "500*(H1+1)/249" + }, + "t_star_k_par_lt_e_over_4": { + "decimal": "52182660963731.927710843373493975903614457831", + "floor": 52182660963731, + "fraction": "250*(2*H1+3)/249" + }, + "tau_log2_exponent": -200000000000, + "translation_scans": { + "columns": [ + "N", + "A", + "e_lo", + "e_hi", + "e_inf_edge", + "e_fit_edge", + "n_inf", + "n_fit", + "n_gap" + ], + "rows": [ + [ + 8, + 2, + 1, + 67110, + 65536, + 66810, + 65480, + 301, + 1273 + ], + [ + 8, + 3, + 1, + 5325, + 4096, + 5025, + 4074, + 301, + 928 + ], + [ + 8, + 4, + 1, + 2740, + 1625, + 2440, + 1606, + 301, + 814 + ], + [ + 8, + 5, + 1, + 2085, + 1024, + 1785, + 1010, + 301, + 760 + ], + [ + 16, + 2, + 1048276, + 1053990, + 1048576, + 1053690, + 301, + 301, + 5113 + ], + [ + 16, + 3, + 1, + 36840, + 32768, + 36540, + 32697, + 301, + 3771 + ], + [ + 16, + 4, + 1, + 13923, + 10321, + 13623, + 10276, + 301, + 3301 + ], + [ + 16, + 5, + 1, + 9168, + 5792, + 8868, + 5749, + 301, + 3075 + ], + [ + 32, + 2, + 16776916, + 16797990, + 16777216, + 16797690, + 301, + 301, + 20473 + ], + [ + 32, + 3, + 261844, + 277662, + 262144, + 277362, + 301, + 301, + 15217 + ], + [ + 32, + 4, + 1, + 79185, + 65536, + 78885, + 65412, + 301, + 13348 + ], + [ + 32, + 5, + 1, + 45483, + 32768, + 45183, + 32675, + 301, + 12414 + ] + ] + } +} diff --git a/research/bit-stock-band-threshold/SOURCES.json b/research/bit-stock-band-threshold/SOURCES.json new file mode 100644 index 0000000000..b433c117de --- /dev/null +++ b/research/bit-stock-band-threshold/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "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/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/selected-bit-stage-stock-band/PROOF.md", + "usage": "input", + "git_blob": "50ba408ec79d7fbed1b5e4d0e24366eb152ad006", + "sha256": "b93430458a861ae26d41a544f25b6bf3b89ca3693793e27b51e2a49c4e80d507" + }, + { + "path": "research/selected-bit-stage-stock-band/README.md", + "usage": "input", + "git_blob": "78f06e0376537a2a0a003d6e06bb5ac81e272a13", + "sha256": "b2bf296410af55bd83cfed8cdb385074737d511528985dbe1bc221ddf6da94c8" + }, + { + "path": "research/selected-old-leaf-reserve/README.md", + "usage": "input", + "git_blob": "366a377aa15a6814bc2a4a80b85b8d889eb33499", + "sha256": "f6d288a36fe18f50eb6d7ecc5ce367e7b3e22d8ab1aecd8c07f2c9090a9dc05f" + } + ] +} diff --git a/research/bit-stock-band-threshold/TASK.json b/research/bit-stock-band-threshold/TASK.json new file mode 100644 index 0000000000..15c2c97904 --- /dev/null +++ b/research/bit-stock-band-threshold/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "refined", + "actual_scope": "At the one ordinary-BIT stage of PR #4954 (rank N = 2^25986965159937, atom exponent 1/250), decide exactly where the source borrowed-digit prescription k < e/2 fits, between the proved-infeasible log2 e = 52182660963729 and the proved-fit log2 e = 52182660963735. Use the old-leaf reserve of PR #4970 (k_old = 1, fallback 103) and the hypothesis c_B <= N^2 of #4954, both cited and not replayed.", + "scope_change_reason": "The card asks for an explicit uniform stock envelope at one stage. This package stays at the stage and envelope of PR #4954 and settles one explicit remaining question there, open question 3 of #4954 'Close the six-bit window', which is also the first open question of PR #7101. It does not derive a new reserve coefficient.", + "bottleneck_link": "Side result on one inherited implementation obligation of the selected BIT stage: the width domain on which its source stock prescription can be borrowed. It changes no kappa, supplier admission, stock coefficient or frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact depth-two criterion, its translation to log2 e, the integer decisions at the window and at the e/4 guard, and the verifier. Do not decide the remaining window of width 2^(-2*10^11) or read the compiled depth bound.", + "outcome": "completed", + "evidence": "PROOF.md proves: at depth two the prescription fits iff e > 4*N^2*w + 4*delta_B + 2*k_old; every width of depth at least one with log2 e <= t* = 500*(H1+1)/249 = 52182660963730.9236947791 fails to fit; under c_B <= N^2 and k_old <= N^2 every width with log2 e >= t* + 2^(-2*10^11) fits; so the six-bit window of #4954 closes to a window of width at most 2*2^(-2*10^11) in log2 e, independent of B and of S_old within the hypotheses. At e = 2^t the split is t <= 52182660963730 infeasible and t >= 52182660963731 fitting; the e/4 guard of #4954 holds from t = 52182660963732 (it fails at ...731). verify.py authenticates the pinned sources, checks 170 envelope cases and 336,636 depth-two instances of the source formula against the criterion, scans the exact-integer translation chain on twelve (N, A) pairs, computes the exact least fitting width with big integers at six ranks from 2^40 to 2^101, evaluates exact exponent arithmetic at the selected rank, and runs ten rejection controls. It prints PASS_BIT_STOCK_BAND_THRESHOLD and matches the stored RESULT.json. CPython 3.12, standard library only.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which depth bound does the compiled prescription use, and where does the fit start for it if it is larger than floor(log_N ceil(e/w))?", + "why_it_matters": "The parameters file allows any larger explicit integer bound. The infeasible side of the theorem holds for it, but the fit side and the threshold t* are stated for the exact depth.", + "first_step": "Read the depth bound in the compiled stock formula, then replace D by that bound D' in the depth-two criterion; the first edge moves to 250*(2*H1 + log2(2*D'))/249.", + "blocked_by": "The compiled depth bound is not pinned in the sources used here." + }, + { + "question": "Can the last window of width at most 2*2^(-2*10^11) in log2 e around t* be decided exactly?", + "why_it_matters": "It would give the least fitting width itself, not only its location to within 2^(-2*10^11) bits.", + "first_step": "Fix q and B from the compiler realisation and find the block of w = ceil(e^(1/250)) that contains 4*N^2*w + 4*delta_B + 2*k_old.", + "blocked_by": "B is not materialised, so delta_B is known only to lie in [0, c_B]." + }, + { + "question": "Does the later frontier6030/frontier7000 BIT stage use the same rank, atom exponent and stock formula?", + "why_it_matters": "The theorem is bound to the sources of #4954. PR #7101 states that the same rank is retained later; a stage-record comparison would show that t* applies to the current selected record unchanged.", + "first_step": "Compare the stage record of certificates/frontier6030/CLAIM.json with research/query-thinned-controllers/RESULT.json and the pinned stock formula.", + "blocked_by": "That comparison needs the later stage's source bindings, which this package does not pin." + } + ] +} diff --git a/research/bit-stock-band-threshold/VERIFY.json b/research/bit-stock-band-threshold/VERIFY.json new file mode 100644 index 0000000000..8b85af3879 --- /dev/null +++ b/research/bit-stock-band-threshold/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/query-thinned-controllers/RESULT.json", + "research/selected-bit-stage-stock-band/PROOF.md", + "research/selected-bit-stage-stock-band/README.md", + "research/selected-old-leaf-reserve/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes and cited sentences; 170 envelope cases; 336,636 depth-two instances against the exact criterion; exact-integer translation scans on twelve (N, A) pairs; exact least fitting width at six large ranks; exact exponent arithmetic at the selected rank; ten rejection controls; exact receipt match." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same acceptance under python -O; every check raises, so none is stripped." + } + ] +} diff --git a/research/bit-stock-band-threshold/verify.py b/research/bit-stock-band-threshold/verify.py new file mode 100644 index 0000000000..c7eae996e3 --- /dev/null +++ b/research/bit-stock-band-threshold/verify.py @@ -0,0 +1,455 @@ +#!/usr/bin/env python3 +"""Close the six-bit fit window of the selected BIT stage's borrowed-digit prescription. + +Checks PROOF.md: pinned-source bindings, an exact criterion for the depth-two borrowed +digits on small parameters, the exact-integer translation lemma on small atoms and ranks, +exact exponent arithmetic at the selected rank N = 2^H1, and rejection controls. +Standard library only. Produced by Nick Petalas. Apache-2.0. +""" +import argparse +import hashlib +import json +import sys +from fractions import Fraction as Q +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +RECEIPT = HERE / 'RESULT.json' +SCHEMA = 'bit-stock-band-threshold/1' + +A_SEL = 250 # atom exponent 1/250: w = ceil(e^(1/250)) +TAU_BITS = 2 * 10**11 # window width 2^(-TAU_BITS) in log2 e +LIMIT = 10**6 # loop bound for every integer search + +QT_RESULT = 'research/query-thinned-controllers/RESULT.json' +PARAMS = 'research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json' +BRIDGE = 'research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md' +BAND_PROOF = 'research/selected-bit-stage-stock-band/PROOF.md' +BAND_README = 'research/selected-bit-stage-stock-band/README.md' +OLD_LEAF = 'research/selected-old-leaf-reserve/README.md' + +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= 1.""" + need(N >= 2 and n >= 1, 'ilog domain') + d, p = 0, N + for _ in range(LIMIT): + if p > n: + return d + d, p = d + 1, p * N + raise ValueError('ilog limit') + + +def ceil_log(q, x): + """Least c with q^c >= x, for x >= 1.""" + need(q >= 2 and x >= 1, 'ceil_log domain') + c, p = 0, 1 + for _ in range(LIMIT): + if p >= x: + return c + c, p = c + 1, p * q + raise ValueError('ceil_log limit') + + +def gl_order(N, q): + out = 1 + for i in range(N): + out *= q**N - q**i + return out + + +def iroot(x, k): + """floor(x^(1/k)) by bisection.""" + lo, hi = 0, 1 << (x.bit_length() // k + 1) + for _ in range(hi.bit_length() + 2): + mid = (lo + hi + 1) // 2 + lo, hi = (mid, hi) if mid**k <= x else (lo, mid - 1) + need(lo**k <= x < (lo + 1)**k, 'iroot') + return lo + + +def ceil_root(e, A): + """Least w with w^A >= e, i.e. w = ceil(e^(1/A)).""" + r = iroot(e, A) + return r if r**A == e else r + 1 + + +def stock(N, cG, e, w, k_old): + """Borrowed digits k = D(N^2(w-1)+cG)+k_old with D = floor(log_N ceil(e/w)).""" + n = -(-e // w) + D = ilog(N, n) + return D * (N * N * (w - 1) + cG) + k_old, D, n + + +# ------------------------------------------------------------------ Lemma 1 and Lemma 2 +def role_grid(N, q): + """Role counts B with c_B = 0..N^2+1: B = q^j and q^j + 1.""" + return sorted({q**j + s for j in range(N * N + 2) for s in (0, 1)}) + + +def check_envelope(cases=((2, 3), (2, 5), (3, 3), (3, 5), (4, 3), (2, 7), (5, 3))): + count = 0 + for N, q in cases: + G = gl_order(N, q) + need(q**(N * N - 1) < G < q**(N * N), 'GL order bounds %d %d' % (N, q)) + for B in role_grid(N, q): + cG, cB = ceil_log(q, B * G), ceil_log(q, B) + need(N * N <= cG <= N * N + cB, 'envelope %d %d %d' % (N, q, B)) + count += 1 + return count + + +def d2_threshold(N, w, delta, k_old, mutate=None): + """Claimed exact depth-two criterion: fits iff e > 4(N^2 w + delta) + 2 k_old.""" + base = 4 * (N * N * w + delta) + 2 * k_old + if mutate == 'off_by_one': + return base - 1 + if mutate == 'ignore_chart': + return 4 * N * N * w + 2 * k_old + if mutate == 'factor_two': + return 2 * (N * N * w + delta) + 2 * k_old + return base + + +def check_d2_criterion(mutate=None): + """For every depth-two width, the source formula agrees with the claimed criterion.""" + count = 0 + for N, qs, wmax in ((2, (3, 5, 7), 6), (3, (3, 5, 7), 6), (4, (3, 5), 5), (5, (3,), 3)): + for q in qs: + G = gl_order(N, q) + for B in role_grid(N, q): + cG = ceil_log(q, B * G) + delta = cG - N * N + need(0 <= delta <= ceil_log(q, B), 'chart excess within c_B') + for w in range(1, wmax + 1): + for k_old in (1, 2, 5): + thr = d2_threshold(N, w, delta, k_old, mutate) + for e in range((N * N - 1) * w + 1, (N**3 - 1) * w + 1): + k, D, _ = stock(N, cG, e, w, k_old) + need(D == 2, 'depth two range') + need((2 * k < e) == (e > thr), 'criterion N=%d q=%d B=%d w=%d e=%d' % (N, q, B, w, e)) + count += 1 + return count + + +# --------------------------------------------------- exact-integer translation lemma (small) +def pred_inf(e, N, A, s=2): + """e^(A-1) <= (2^s N^2)^A, i.e. e^((A-1)/A) <= 2^s N^2.""" + return e**(A - 1) <= ((1 << s) * N * N)**A + + +def pred_fit(e, N, A, M=4, c=10): + """e > c N^2 and (e - c N^2)^A >= (M N^2)^A e: forces e >= M N^2 e^(1/A) + c N^2.""" + return e > c * N * N and (e - c * N * N)**A >= (M * N * N)**A * e + + +def edge_widths(N, A): + """Largest e with pred_inf, least e from which pred_fit holds (pred_fit is monotone).""" + e_inf = iroot(((4 * N * N)**A), A - 1) + lo, hi = 10 * N * N + 1, 2 * e_inf + 10 * N * N + 2 + need(pred_fit(hi, N, A), 'fit predicate at the upper end') + for _ in range(hi.bit_length() + 2): + mid = (lo + hi) // 2 + lo, hi = (lo, mid) if pred_fit(mid, N, A) else (mid + 1, hi) + return e_inf, lo + + +def scan_translation(A, N, lo, hi, s_inf=2, M=4, c=10): + """Check T1 and T2 on every e in [lo, hi] with the source formula's extreme readings.""" + w = ceil_root(lo, A) + n_inf = n_fit = n_gap = 0 + for e in range(lo, hi + 1): + for _ in range(LIMIT): + if w**A >= e: + break + w += 1 + n = -(-e // w) + D = ilog(N, n) + if D >= 1 and pred_inf(e, N, A, s_inf): # best reading: chart excess 0, k_old = 1 + need(2 * (D * N * N * w + 1) >= e, 'T1 violated A=%d N=%d e=%d' % (A, N, e)) + n_inf += 1 + elif D == 2 and pred_fit(e, N, A, M, c): # worst reading: excess N^2, k_old = N^2 + need(2 * (2 * (N * N * (w - 1) + 2 * N * N) + N * N) < e, 'T2 violated A=%d N=%d e=%d' % (A, N, e)) + n_fit += 1 + elif D >= 2: + n_gap += 1 + return n_inf, n_fit, n_gap + + +def check_translation(s_inf=2, M=4, c=10): + rows = [] + for N, atoms, full in ((8, (2, 3, 4, 5), True), (16, (2, 3, 4, 5), True), (32, (2, 3, 4, 5), True)): + for A in atoms: + e_inf, e_fit = edge_widths(N, A) + need(e_inf < e_fit, 'infeasible edge below fit edge') + lo, hi = max(1, e_inf - 300), e_fit + 300 + if full and hi <= 150000: + lo = 1 + n_inf, n_fit, n_gap = scan_translation(A, N, lo, hi, s_inf, M, c) + rows.append([N, A, lo, hi, e_inf, e_fit, n_inf, n_fit, n_gap]) + return rows + + +def check_deeper_depths(N=64, top=400): + """Lemma 2(d): N^(D-2) >= 8D+1 for every D >= 3 up to a bound, at N = 64.""" + for D in range(3, top): + need(N**(D - 2) >= 8 * D + 1, 'depth three and beyond D=%d' % D) + return top - 3 + + +# ------------------------------------------------ exact transition at large rank (big integers) +def exact_transition(N, A, delta, k_old, w_lo, w_hi): + """Least e0 such that every width in [e0, w_hi^A] fits at depth two, by blocks of w. + + Block w is ((w-1)^A, w^A]; there the prescription fits iff e > 4*(N^2*w + delta) + 2*k_old. + """ + def thr(w): + return 4 * (N * N * w + delta) + 2 * k_old + need(w_lo < w_hi and w_hi - w_lo <= 64, 'block range') + need((w_hi - 1)**A > thr(w_hi), 'top block fits entirely') + for w in range(w_hi - 1, w_lo, -1): + if (w - 1)**A > thr(w): # block w fits entirely: keep descending + continue + return thr(w) + 1 if thr(w) < w**A else w**A + 1 + raise ValueError('no transition inside the block range') + + +def check_large_rank(s_inf=2, ranks=((40, 2), (41, 3), (51, 5), (59, 11), (100, 2), (101, 3))): + """Exact transition widths at N = 2^h: best and worst readings against both edges.""" + rows = [] + for h, A in ranks: + N = 1 << h + e_inf = iroot(((1 << s_inf) * N * N)**A, A - 1) + _, e_fit = edge_widths(N, A) + w_lo, w_hi = ceil_root(e_inf, A) - 2, ceil_root(e_fit, A) + 3 + best = exact_transition(N, A, 0, 1, w_lo, w_hi) + worst = exact_transition(N, A, N * N, N * N, w_lo, w_hi) + need(e_inf < best <= worst <= e_fit, 'transition inside the bracket h=%d A=%d' % (h, A)) + need(N * N <= ceil_root(e_inf, A)**(A - 1) and ilog(N, -(-e_inf // ceil_root(e_inf, A))) == 2, 'depth two') + rows.append([h, A, (best - e_inf) * 1000 // (N * N), (worst - e_inf) * 1000 // (N * N), + (e_fit - e_inf) * 1000 // (N * N)]) + return rows + + +# ----------------------------------------------------- exact exponent arithmetic at rank N +def t_star(H1, A, mlog): + """Real t with (A-1)/A * t = 2 H1 + mlog, i.e. e^((A-1)/A) = 2^mlog N^2.""" + return Q(A * (2 * H1 + mlog), A - 1) + + +def inf_by_exponent(H1, t, A, mlog): + return (A - 1) * t <= A * (2 * H1 + mlog) + + +def fit_by_exponent(H1, t, A, mlog, c): + """e = 2^t satisfies (e - c N^2)^A >= (2^mlog N^2)^A e, hence e >= 2^mlog N^2 e^(1/A) + c N^2.""" + margin = (A - 1) * t - A * (2 * H1 + mlog) # exponent of 2 in the leading ratio + x_small = t - 2 * H1 >= (1000 * c).bit_length() # c N^2 / e <= 1/1000 + base = Q(1000, 999)**A < 2 # (1 - x)^(-A) < 2 for x <= 1/1000 + return margin >= 1 and x_small and base + + +def depth_at_pow2(H1, t, A): + """floor(log_N ceil(e/w)) at e = 2^t from the sign of (A-1) t - A k H1 (never zero here).""" + D = 0 + for k in range(1, 8): + gap = (A - 1) * t - A * k * H1 + need(gap != 0, 'depth boundary hit exactly') + if gap > 0: + D = k + return D + + +def classify(H1, t, A=A_SEL): + """('k= TAU_BITS + 3, 'rho = 2^(-t/250) <= 2^(-(TAU_BITS+3))') + need(H1 >= 64 and ts > 2 * H1 + 1, 'selected rank domain') + t0 = int(ts) + need(t0 == 52182660963730 and decimal(ts).startswith('52182660963730.9236947791'), 'threshold decimal') + need(not inf_by_exponent(H1, t0 + 1, A, 2) and inf_by_exponent(H1, t0, A, 2), 'integer split of k= 1 + need(depth_at_pow2(H1, t1 - 1, A) == 0 and depth_at_pow2(H1, t1, A) == 1, 'depth-one onset') + need(t1 == 26091330481865 and depth_at_pow2(H1, t0 - 1, A) == 2, 'onset and depth two before t*') + return t0, tg0, decimal(ts), decimal(tg), t1 + + +# ----------------------------------------------------------------------------- controls +def control_tamper(): + def flip(raw): + return raw.replace(b'25986965159937', b'25986965159938', 1) + try: + load_sources((QT_RESULT, flip)) + except ValueError: + return True + return False + + +def control_raises(fn): + try: + fn() + except ValueError: + return True + return False + + +def controls(H1, table): + out = { + 'tampered_selected_rank_rejected': control_tamper(), + 'off_by_one_criterion_rejected': control_raises(lambda: check_d2_criterion('off_by_one')), + 'ignored_chart_excess_rejected': control_raises(lambda: check_d2_criterion('ignore_chart')), + 'factor_two_criterion_rejected': control_raises(lambda: check_d2_criterion('factor_two')), + 'inflated_infeasible_edge_rejected': control_raises(lambda: scan_translation(2, 8, 1, 70000, s_inf=3)), + 'deflated_fit_edge_rejected': control_raises(lambda: scan_translation(2, 8, 1, 70000, M=2)), + 'inflated_large_rank_edge_rejected': control_raises(lambda: check_large_rank(s_inf=3)), + 'shifted_rank_changes_table': selected_table(H1 + 1) != table, + 'fit_below_threshold_rejected': not fit_by_exponent(H1, int(t_star(H1, A_SEL, 2)), A_SEL, 2, 10), + 'infeasible_above_threshold_rejected': not inf_by_exponent(H1, int(t_star(H1, A_SEL, 2)) + 1, A_SEL, 2), + } + need(all(out.values()), 'rejection controls: %s' % [k for k, v in out.items() if not v]) + return out + + +# ------------------------------------------------------------------------------ receipt +def build_receipt(): + data, digests = load_sources() + H1 = bind(data) + t0, tg0, ts_dec, tg_dec, t1 = check_selected(H1) + table = selected_table(H1) + rows = check_translation() + deeper = check_deeper_depths() + need(table[0]['t'] == t0 - 6 and any(r['t'] == t0 and r['k_lt_e_over_2'] == 'infeasible' for r in table), + 'table rows') + return { + 'schema': SCHEMA, 'sources': digests, 'H1': H1, 'atom_denominator': A_SEL, + 'tau_log2_exponent': -TAU_BITS, 'depth_one_onset_t': t1, + 't_star_k_lt_e_over_2': {'fraction': '500*(H1+1)/249', 'floor': t0, 'decimal': ts_dec}, + 't_star_k_par_lt_e_over_4': {'fraction': '250*(2*H1+3)/249', 'floor': tg0, 'decimal': tg_dec}, + 'selected_table': table, + 'envelope_cases': check_envelope(), + 'depth_two_instances': check_d2_criterion(), + 'translation_scans': {'columns': ['N', 'A', 'e_lo', 'e_hi', 'e_inf_edge', 'e_fit_edge', + 'n_inf', 'n_fit', 'n_gap'], 'rows': rows}, + 'deeper_depth_checks': deeper, + 'large_rank_transitions': {'columns': ['h', 'A', 'best_minus_edge_milli_N2', 'worst_minus_edge_milli_N2', + 'fit_edge_minus_edge_milli_N2'], 'rows': check_large_rank()}, + 'controls': controls(H1, table), + } + + +def main(argv): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write', metavar='PATH', help='write a fresh receipt (never overwrites)') + args = ap.parse_args(argv) + receipt = build_receipt() + text = json.dumps(receipt, indent=2, sort_keys=True) + '\n' + if args.write: + out = Path(args.write) + need(not out.exists(), 'receipt path exists: ' + str(out)) + out.write_text(text, encoding='utf-8') + print('wrote', out) + return 0 + need(RECEIPT.read_text(encoding='utf-8') == text, 'stored RESULT.json differs from the recomputed receipt') + print('PASS_BIT_STOCK_BAND_THRESHOLD t*=%s guard_t*=%s depth2_instances=%d scans=%d large_rank=%d controls=%d' % ( + receipt['t_star_k_lt_e_over_2']['decimal'], receipt['t_star_k_par_lt_e_over_4']['decimal'], + receipt['depth_two_instances'], len(receipt['translation_scans']['rows']), + len(receipt['large_rank_transitions']['rows']), len(receipt['controls']))) + return 0 + + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:]))