diff --git a/research/pr4338-b2-chain-check/README.md b/research/pr4338-b2-chain-check/README.md new file mode 100644 index 0000000000..0a071be2e3 --- /dev/null +++ b/research/pr4338-b2-chain-check/README.md @@ -0,0 +1,86 @@ +# Independent check of #4338's ordinary B2 bootstrap arithmetic + +**Claim type: an independent exact check of a written arithmetic chain, +including a certified moment enclosure. No new κ.** This does not accept +#4338, and it checks none of its source-relative physical contracts. + +## Object + +[PR #4338](https://github.com/CrocSwap/integer-mult-bounds/pull/4338) (Ross +Richardson, head `0ac8192b…`) splits the optional ordinary B2 stage out of +#4270. With BIT coupling `c = 1/577`, it claims: + +- the ordinary saving `a2 = 57697923247/33292900000000 ≈ 0.00173304`; +- the bound `T_B2 ≤ 4283584·A·V·e^(1−a2)`; +- that `a2` exceeds the pooled complex endpoint `C`. + +Its own checker runs a frozen interval engine and an integer-power bisection. +No outside check existed. + +## Results + +Every link of PROOF.md §1, §3 and §4 holds, recomputed with exact rationals. +The inputs are read from main: `H` is the selected BIT supplier's +`nine.profile`, `a1` is PR2899's `ordinary_saving`, and `C` is +`staged-fourth-mixture-ceiling`'s root. + +| Link | Result | +| --- | --- | +| `a2 = c(1−c) + c·a1` | exactly the stated rational; `a2 − C` is exactly the stated `2.06·10⁻⁶` | +| §1: bootstrap at the complex rate | `a_next` and the outer-loss value match to 28 digits. The shortfall below `0.001727989140903569` is `5.84263·10⁻⁸` | +| `F = 32·64²·ΣH` | `118606528512` | +| `μ_1` | exactly `2874298095721977/2890625000000000 < 199/200` | +| `μ_(576/577)` | enclosure width `< 10⁻³³`, inside the stated `10⁻³⁰` interval. `1 − μ = 1.0614·10⁻⁶`, so the `10⁶` coefficient holds, and the old `9999/10000` cap is false | +| Fit comparisons | `17^128 > 32·16^128`; `32780·(17/16)·20 = 696575 < 2^20`; `2^(20/577) < 17/16` | +| Exponent algebra | `(1−c) + c(c−a1) = 1 − a2`; `2^(c−a1) < 17/16`; `a2 < c`; `1 − a2 − c > 1/2` | +| Coefficient | `801 + 4000000·17/16 + 32780 + 3 = 4283584` | +| Gap table | all four exact. `1 − a2 − c(1−a1) = (1−c)²`, and the minimum gap is `c − a2 = 6.24·10⁻⁸` | + +**Control.** Dropping the fallback weight `εF` moves `μ_(576/577)` below the +stated interval. The interval does include the fallback, as #4338 says. + +**Two tight spots.** + +- `1 − μ_(576/577)` exceeds the `10⁻⁶` that the `10⁶` coefficient needs by + only 6%. +- The minimum gap `c − a2` is `6.2·10⁻⁸`. + +**Orientation.** `a2` lies below the selected BIT saving +`0.0017334270…` by `3.9·10⁻⁷`. That is expected, since `a2 < c = 1/577` and the +BIT constructor needs `c` below its moment root. #4338 does not compare them. + +## Not covered + +- The source-relative contracts: + - the B1/C1/B2 factory composition and restoration; + - the 1,123-chart registry; + - the retained stock-depth bound (coupling-independent; see below); + - the fit predicates beyond the stated comparisons. +- The production B2 factory and any complex caller. +- The legacy target `0.001727989140903569`. It is quoted from #4338; its + source is not on main. + +## Reproduce + +```sh +python3.12 -B research/pr4338-b2-chain-check/verify.py +``` + +It prints `PASS_PR4338_B2_CHAIN_CHECK` in under a second, using only the +standard library. `vendor/B2-PROOF.md` is #4338's PROOF.md, byte-identical and +SHA256-checked, with 28 phrase checks. + +## Open next questions + +None from this check. The stock bound `k ≤ 16390 e^c log2 e` does not depend +on the coupling: `retuned-ordinary-coupling` derives it from `D(e) ≤ 2 log2 e`, +`|GL64(F_q)| < q^4096` and `w ≤ 2e^c`, all of which hold at `c = 1/577`. The +remaining obligations are #4338's own physical premises. + +## Credit + +The B2 construction and its arithmetic are #4338's (Ross Richardson with +OpenAI Codex assistance), composing Jose Manuel's ordinary and fast-primitive +sources, Rohan Arun's PR185/387 argument and the PR589 BIT profile. Prepared +by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) +assistance. Apache-2.0. diff --git a/research/pr4338-b2-chain-check/SOURCES.json b/research/pr4338-b2-chain-check/SOURCES.json new file mode 100644 index 0000000000..80b73b2606 --- /dev/null +++ b/research/pr4338-b2-chain-check/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/selected-bit-recursive-closure/RESULT.json", + "usage": "input", + "git_blob": "e7f281a85797dc91ad24e5e5ee6500966e9905b9", + "sha256": "85cdaa514113b9e49a578c6856057d2503307e6ba02510ef800d3ace67713e74" + }, + { + "path": "research/staged-fourth-mixture-ceiling/RESULT.json", + "usage": "input", + "git_blob": "2803d5c42b5d49ea72bd9bb006ffb4a9eec6a316", + "sha256": "53849028b12f7d9b726ac7576eeb64dc9a1a51bb2890edbb15aa83d1e39fae5f" + } + ] +} diff --git a/research/pr4338-b2-chain-check/TASK.json b/research/pr4338-b2-chain-check/TASK.json new file mode 100644 index 0000000000..37d2a5ae42 --- /dev/null +++ b/research/pr4338-b2-chain-check/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independently recompute #4338's B2 arithmetic chain: a2, the section 1 shortfall, mu_1 and the certified mu_(576/577) enclosure, the fit comparisons, the 4283584 coefficient and the gap table, with H, a1 and C bound to main.", + "scope_change_reason": "The card asks for independent coverage of a new paid-profile or moment claim; #4338 is new and had no outside check.", + "bottleneck_link": "#4338 removes an ordinary-rate obstruction for the pooled complex route; its arithmetic must hold before its physical contracts are worth review.", + "budget_minutes": 25, + "stop_rule": "Stop once every stated arithmetic link is certified or fails.", + "outcome": "completed", + "evidence": "verify.py: a2 and a2-C exact; section 1 digits and 5.84263e-8 shortfall; F = 118606528512; mu_1 exact < 199/200; mu_(576/577) inside the stated 1e-30 interval with width < 1e-33, 1-mu = 1.0614e-6; fit comparisons; coefficient 4283584; gap table exact, minimum c-a2 = 6.24e-8; dropping the fallback leaves the interval.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.", + "open_questions": [], + "no_open_questions_reason": "Every arithmetic link holds; the stock-depth bound is coupling-independent, and the remaining obligations are #4338's physical premises." +} diff --git a/research/pr4338-b2-chain-check/VERIFY.json b/research/pr4338-b2-chain-check/VERIFY.json new file mode 100644 index 0000000000..3a6d8899d8 --- /dev/null +++ b/research/pr4338-b2-chain-check/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/selected-bit-recursive-closure/RESULT.json", + "research/staged-fourth-mixture-ceiling/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Vendored PROOF.md hash and 28 phrases; H, a1, C bound to pinned main files; a2 and a2-C; section 1 outer-loss shortfall; F and mu_1 exact; certified mu_(576/577) enclosure in the stated interval; induction coefficients; fit comparisons; exponent algebra; 4283584 coefficient; gap table; fallback-omission control." + } + ] +} diff --git a/research/pr4338-b2-chain-check/vendor/B2-PROOF.md b/research/pr4338-b2-chain-check/vendor/B2-PROOF.md new file mode 100644 index 0000000000..b723a2fdca --- /dev/null +++ b/research/pr4338-b2-chain-check/vendor/B2-PROOF.md @@ -0,0 +1,391 @@ +# One ordinary bootstrap step that clears the complex rate + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. The construction composes Jose Manuel's completed ordinary and +fast-primitive sources, Rohan Arun's PR185/387 stopped-leaf argument, and the +retained PR589 BIT profile. It does not originate those components or their +bootstrap formula. + +Under the stated source-relative physical contracts, one further ordinary +stage supplies + +``` +a2 = 57697923247/33292900000000 + = 0.001733039874778105842386815206845904..., +T_B2(V,e) <= 4283584 A V e^(1-a2), +``` + +for a finite uniform coefficient `A` specified below. It exceeds the present +complex endpoint `C=0.001730980255989036959962` by the exact positive rational + +``` +a2-C = 342853411912956978405651/166464500000000000000000000000. +``` + +This is an ordinary interchange construction from the **BIT** component. +It invokes no part of the new complex source. It removes an ordinary-rate +obstruction once the completed binary interface is connected to the complex +caller; it does not by itself supply that caller or its outer embedding. + +## 1. Why a bootstrap at the complex rate is insufficient + +The demonstrated preceding ordinary rate is +`a1=169711/100000000=0.00169711`. If one retains the selected convenience +choice `s=(1-10^-24)C-10^-27`, the one-step value is + +``` +a_next = s(1-s)+s*a1 = 0.001730921627244654642552821294... . +``` + +Although this exceeds the requested legacy kappa, the legacy outer margin is + +``` +q=(1-2*10^-24)*a_next, +(1-10^-24)*q/(1+q) = 0.001727930714600372546778004395..., +``` + +which is below `0.001727989140903569` by more than `5.8426*10^-8`. +Comparing an ordinary rate directly with kappa omits a necessary outer loss. + +Instead choose the independent BIT coupling `c=1/577`. The BIT constructor +does not need `c2^80`, positive complete preceding, +intervening and trailing spectator extents, and the selected PR589 BIT +catalogue. The native ordinary interface maps the two complete radix-q +chunks of width `e`, preserves its borrowed input, returns a distinct owned +output, restores every spectator coordinate, and closes its owned work. +The binary wrapper preserves the same completed contract. Successful admitted +execution is the scope; interruption recovery is not asserted. + +The previous `B1` is the actual ordinary construction of +[`selected-bit-recursive-closure`](../selected-bit-recursive-closure/PROOF.md) +and PR2899, with its fixed coupling `17/10000` and saving `a1`. Its sealed +coarse caller uses its elementary `A0` routes and swaps. The successor `C1` +is the physical program in +[`selected-bit-fast-primitives`](../selected-bit-fast-primitives/PROOF.md): +both the reached weighted/remainder swap and the reached complete owner-chart +route use that completed `B1`. Entering `B1` suspends the successor factory +scope and restores both preceding bindings. `B1` completes under those +preceding bindings. Exiting the suspended scope then restores the successor +bindings before the caller acquires its output lease, copies the protected +result and clears that result. The preceding output remains protected until +this copy/clear finishes, before any reuse. + +The complete dependency order is + +``` +new complex caller -> binary B2 -> ordinary B2 -> C1 -> B1 -> C0 -> A0. +``` + +Only the leftmost caller is the new complex construction. Its correctness is +not used to construct anything to its right. Coarse recursive calls decrease +atom count; a call to the preceding ordinary implementation decreases the +fixed stage. `B1` never re-enters `C1` or `B2`. + +The existing factory composition is precise. In the one cold namespace +authenticated by `stage_sources.activate()`, create two distinct `Ordinary` +instances on the same immutable selected BIT binding, topology and programs: + +``` +previous = Ordinary(q, binding, topology, programs, + profile=Profile()) # 17/10000, m=64, rmax=42 +outer = Ordinary(q, binding, topology, programs, + profile=Profile(numerator=1, denominator=577)) +registry, receipt = selected_registry(actual_selected_bit_catalogue) +native_B2 = promote_ordinary(outer, previous, registry) +binary_B2 = Binary(native_B2) +``` + +`selected_registry` must bind all 1,123 actual data/host charts and their +inverse factor words. An identity-only `Registry(64)` is insufficient. +`promote_ordinary` changes the controller view of the fresh outer root +session before it reads numerical input; it reuses that session's actual +physical roles and adds the fixed successor scratch allowance. It does not +copy an active machine or alias its work with `previous`. + +The two predecessor exports are compatible at the source level. All 23 files +in `selected-bit-fast-primitives/inputs/pr2899.tar` are byte-identical to the +corresponding files in the retuned coupling's PR2899 export; the latter adds +twelve frozen dependencies. Their SHA256 values are respectively +`fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531` and +`0fef1707c6460418fd01fd49faf0d8ff7945907fa57284765c852a12d2674d3c`. +The independently cold-guarded loaders should not both be invoked into one +already populated namespace. + +This specifies a finite program composition under the retained source +arguments. The present arithmetic audit does not execute a production GL64 +payload or claim a new full physical-machine replay of that composition. +Changing `Profile` on an unpromoted C0-backed `Ordinary` supplies only a +retuned first stage and does not establish this B2 bound. + +## 3. Complete stopped BIT recurrence + +Write `p1=1-a1`. Retain the complete paid BIT histogram and bad-class term: + +``` +H={1:381024,2:400416,3:22752,4:26880, + 5:29376,6:17376,7:26784,42:288}, +m=64, W=28416, epsilon=10^-16, +F=32*64^2*sum(H)=118606528512. +``` + +Every paid request executes its complete low/high fibre; the per-request +bad-class estimate is retained. No average over selectively omitted prefixes +is used. The fast-primitive source's explicit local bill is bounded by + +``` +C_B1 V [252 w^p1 + (1598048/111)(w-1)^p1] + A_q V(n+1) + E_prep. +``` + +At `w=1`, omit the high-route term. The 252 bound is four calls for each +of at most 63 peeled pairs. The other coefficient counts both entrance and +return owner routes, with the actual same-q `B1` interface. It is a time +coefficient, unrelated to the old external row allowance also numbered 252. +`E_prep` includes coefficient/history preparation and is absorbed only in +the canonical root-coupled domain, by the complete target-fibre argument. + +Choose a finite `A>=1` dominating these uniform coefficients, the preceding +`B1` bound, all source access and output disposal, the outer wrapper bill, +and its elementary fallback. It may depend on the fixed prime, source, +compiled registry and fixed machine inventories. It does not depend on +width, payload contents, ancestor, prefix ordinal or external multiplicity. +No empirical bound such as `A<2^512` is asserted. + +For normalized time `T1(n,w)` and `f=floor(n/64)`, the actual stopped tariff is + +``` +T1(n,w) <= A w^p1 (0=64). +``` + +It includes all restoration, routing, selection, copying, marker work, +rewinds and private-work disposal. The preceding ordinary calls are in the +local toll, not additional C1 coarse children or parent row multipliers. + +Define `mu_t=(sum H[r](r/64)^t+epsilon F(1/64)^t)/W`. +The exact full-profile calculation gives + +``` +mu_1 = 2874298095721977/2890625000000000 < 199/200, +mu_(576/577) in + [999998938581682162866772413602, + 999998938581682162866772413603]/10^30 < 999999/1000000. +``` + +The old `9999/10000` power cap is false at this coupling. Use the increased +coefficient, not the predecessor's smaller number. Strong induction against +a monotone majorant, including the fallback maximum, yields + +``` +T1(n,w) <= 200 A n + 1000000 A n^(1-c) w^p1. (1) +``` + +The linear contraction pays `A n`; the strict power gap pays `A w^p1`. +No monotonicity of the machine's measured running time is assumed. + +The interval above was independently rechecked using both the outward +rational series in `frozen/interval_engine.py` and integer-power bisection: at scale +`Q=2^160`, consecutive integers bound each power through +`z^577 64^576 <= r^576 Q^577 < (z+1)^577 64^576`. +Both computations retain the rational fallback weight. + +## 4. Actual stock, wrapper and all-width coefficient + +Use the encoded selector of +[`retuned-ordinary-coupling`](../retuned-ordinary-coupling/PROOF.md), keeping +the original width fixed throughout each coarse root: + +``` +w=ceil(e^c), +D(e)=0 for e<64; D(e)=1+D(42 floor(e/64)) otherwise, +K(w)=269241600 |GL64(F_q)| q^(4096(w-1)), +stock=K(w)^D(e), k=min{j:q^j>=stock}. +``` + +Choose the stock before the body, then set `n=floor((e-k)/w)` and +`ell=e-k-nw`. Use elementary fallback if `2k>=e` or `n<64`. +The retained depth and stock proof gives `k<=16390 e^c log2(e)` for `e>=2`. +Since `17/10000=2^20`, both actual fit predicates hold. The sufficient comparisons +include `17^128>32*16^128` and +`32780*(17/16)*20=696575<2^20`; then `n>e^(1-c)/4-1>64`. +This is a sufficient cutoff, not a claim of the smallest fit threshold. + +The ordinary wrapper executes two completed reversed-body ROOT calls. Each +uses padding below two, so (1) is charged four times. Include the three +ordered body updates, restrictions, residual digits, high exchange, setup, +all scans, copying, rewinds, erasure and output return. Enlarging `A` as above +gives the complete bill + +``` +T_B2(V,e)/V <= A[801n + 4000000 n^(1-c) w^p1 + k+w+1]. (2) +``` + +The wrapper's retained elementary high/remainder operations are sufficient; +they are not silently promoted to a free weighted or reversed operation. + +Now `a2=c(1-c)+c*a1`. Since `c>a1`, + +``` +n^(1-c) w^p1 <= e^(1-c) w^(c-a1) + <= 2^(c-a1) e^(1-a2) + < (17/16) e^(1-a2). +``` + +Also `a21/2`, and `log2(e)<=2 sqrt(e)` for `e>=1`. +Consequently `n<=e^(1-a2)`, `k<=32780 e^(1-a2)`, +`w<=2 e^(1-a2)` and `1<=e^(1-a2)`. Substitution in (2) gives + +``` +801 + 4000000*(17/16) + 32780 + 2 + 1 = 4283584. +``` + +For the finite fallback range `e<2^20`, `e^a2<2^(20/512)<2`, so its +elementary `A V e` bound fits the same coefficient. The source's fixed-degree +logarithmic setup is retained and absorbed into `A`; the retuned proof uses +`(1+log2 V)^4<=512V`. Positive input volumes also absorb fixed compilation +allowances into a further finite coefficient. The binary wrapper pads two +complete fields by a factor below `q^2` and charges its own operations; this +only changes the fixed q-dependent coefficient. + +For comparison with the PR185/387 generic cutoff method, the four exact gaps +are + +| Gap | Value | +| --- | --- | +| `c-a2` | `2076753/33292900000000` | +| `1-a2-c` | `33177502076753/33292900000000` | +| `1-a2-c(1-a1)` | `331776/332929` | +| `1-c` | `576/577` | + +Their minimum is the first. The generic sufficient recipe remains valid: +choose a genuine coefficient bound `A_*<2^h`, then +`L>=max(20,36/delta^2,2(4+h)/delta)` and use the preceding completed algorithm +below `2^L`, enlarging the next constant by its actual fallback cost. +It must carry the preceding constant. The explicit coefficient argument +above avoids needing that enormous time-absorption cutoff: its `2^20` +cutoff is for physical stock fit, while `A` is retained in the time bound. + +## 5. Restoration and finite physical inventories + +Each B1 primitive restores its borrowed source, complete spectators and row +coordinate at its own return, before the successor reuses any output or row. +The parent C1 retains its fixed roles while the preceding complete inventory +is active. The successor adds 128 fixed scratch tapes and its separately +counted fixed-capacity high numerical bank. Distinct B1 and B2 instances have +distinct owned work; immutable source tables may be shared. + +The parent's stock quotient is reused only after each completed child +returns. Neither the two reversed-body calls nor the extra bootstrap stage +multiplies the externally supplied row divisor. B1's internal stock and +binary padding are included in its completed time/space contract. Depth-first +parking and the geometric child-volume sum give the retained +`O_q(V_root)+F_q` occupied/visited space, including blank retained backing +for the fixed roles. This is not per-return deallocation of host memory. + +This is the completed-interface premise of PR185 and PR387, not merely a +final two-call endpoint: two erroneous row changes that cancel at the outer +return would not meet it. The source-bound `StagePool.suspended` and +protected-output copy/clear are the relevant implementation boundaries. + +## 6. Boundary of the optional B2 route + +This package constructs and prices the optional ordinary B2 stage under its +retained source-relative physical contracts. It uses the canonical BIT, +preceding ordinary and fast-primitive sources; it invokes no pooled complex +supplier and has no dependency on PR #4270. + +The B2 rate is strictly above `C`, so it can be weakened to a desired +ordinary rate below `C`. This removes one rate obstruction. It does not +establish a complex or multiplication exponent. A consumer must bind the +completed B2 interface at its actual compact call sites and preserve every +native endpoint, hosting, width, restoration, stopping-rule and outer +analytic obligation at those calls. In particular, changing an ordinary +exponent does not remove exceptional repair, row separation or long-record +costs in the compact binary theorem of +[`physical-complex-compact`](../physical-complex-compact/PROOF.md). + +That theorem's complete tariff includes + +``` +s sum_rows T_B2(v0,nG) + O_m(V+M A_len^6+delta M A_len(R+A_len)), +``` + +with four binary calls for an earlier source/toggle and twelve for a later +source. A candidate complex join must separately establish its global +binding over every actual call and chart, its one-active-node recursion +and parked-parent reserve, common-grid precision, and the stopping/root +contract needed by the outer parameters. A modular fixture or a rate +table cannot supply this global invocation. + +The production B2 factory is specified by the source-relative composition +above, but this package's checker neither constructs nor executes it. +Implementation and caller admission remain open. They are not needed for +the exact conditional rate calculation and written cost derivation here. + +## 7. Exact evidence and proof scope + +Run the bounded check from this package: + +``` +python3 b2_bootstrap.py --output /tmp/b2-normal.json +python3 -O b2_bootstrap.py --output /tmp/b2-optimized.json +cmp /tmp/b2-normal.json /tmp/b2-optimized.json +``` + +The independent arithmetic and backend-source comparison are recorded in +[`evidence/B2-BOOTSTRAP.json`](evidence/B2-BOOTSTRAP.json). Both modes passed +with byte-identical receipts, the fallback retained, overlapping independent +rational moment enclosures, all four strict gaps, the exact `4283584` +coefficient, sufficient `2^20` fit and all 23 equal backend files. The eleven +negative controls reject the direct-rate/outer-loss shortcut, omitted +fallback, wrong power coefficient, profile-only bootstrap, infeasible +coupling, inadequate sufficient stock cutoff, omitted root padding, and +changed or missing authenticated source material. + +[`B2-PINS.json`](B2-PINS.json) authenticates the unchanged 54-file inventory +in [`SOURCE-MANIFEST.json`](SOURCE-MANIFEST.json). Each file is read directly +from its declared canonical repository path at the exact scientific-base +bytes, Git blob and SHA256. `VERIFY.json` declares all 54 inputs, so a +Git-free package export includes their complete bytes. No duplicate +2.2 MB closure archive is needed. `--source-root` selects another root and +requires the same full inventory and hashes, rejecting missing or changed +inputs. The legacy control names `missing_vendored_source` and +`changed_vendored_source` are retained; they now test the authenticated +canonical input map. + +The exact original interval engine is retained as +[`frozen/interval_engine.py`](frozen/interval_engine.py), authenticated before +its bytes are compiled and only its pure moment function is called. +The 23-member backend archives are inspected without extraction or source +execution. No production B2 factory is constructed or invoked. + +The receipt's complete mathematical projection is also checked against the +historical B2 receipt recorded at `46965e30a34af44499a1442daeb94cd3b68fa67a`. +Only `source_pins_sha256`, `local_inputs` and `source_bundle` transport fields +change. `B2-PINS.json` records the original receipt SHA256 and exact +projection digest. All rates, full moments, tariffs, fit, 23 backend member +hashes, eleven rejection controls and scope flags agree. + +The inspected reviewed PR185 proof has SHA256 +`bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa`; +the PR387 proof is +`15997b908604d124d688482db46e58da3117ecf1c176597afb1556a767c073d8`. +They are retained in `research/community-round8-audit/pr185-proof-reviewed.md` +and `research/bootstrap-depth-audit/sources/pr387/PROOF.md`. +The actual fast-primitive `stage.py` is +`44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647`. + +These finite checks support the stated source-relative construction and +written all-width cost derivation. They are not a production payload run, +independent human review, proof-assistant verification or a completed +integer-multiplication theorem. diff --git a/research/pr4338-b2-chain-check/vendor/NOTICE.md b/research/pr4338-b2-chain-check/vendor/NOTICE.md new file mode 100644 index 0000000000..6b0efddeb6 --- /dev/null +++ b/research/pr4338-b2-chain-check/vendor/NOTICE.md @@ -0,0 +1,13 @@ +# Vendored file + +`B2-PROOF.md` is a byte-identical copy of +`research/ordinary-b2-bootstrap/PROOF.md` from +[PR #4338](https://github.com/CrocSwap/integer-mult-bounds/pull/4338) at head +`0ac8192bdf6b5217787ffe44c4b1d91732ef6b23` (Git blob +`b723a2fdcad2753163959bac051424674650dd87`). + +It is copied, not pinned, because that PR head is not reachable from canonical main. +`verify.py` checks its SHA256 before reading any phrase. + +It was prepared for Ross Richardson with OpenAI Codex assistance and is Apache-2.0, +as its package states. diff --git a/research/pr4338-b2-chain-check/verify.py b/research/pr4338-b2-chain-check/verify.py new file mode 100644 index 0000000000..10363301ff --- /dev/null +++ b/research/pr4338-b2-chain-check/verify.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Independent exact check of #4338's ordinary B2 bootstrap arithmetic. + +Standard library only; no code from #4338. Its PROOF.md is vendored byte-identically +(vendor/NOTICE.md) and phrase-checked; H, a1 and C are read from their canonical files on +main. The moment at 576/577 is enclosed with exact rationals: ln by atanh after reducing by +powers of two, exp by Taylor with a Lagrange remainder. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROOF_SHA256 = "c2ca95cc85439768ebfae81057b845b9e26cc8f153ef787c15f74127456dba8b" +PHRASES = [ + "a2 = 57697923247/33292900000000", + "T_B2(V,e) <= 4283584 A V e^(1-a2),", + "a2-C = 342853411912956978405651/166464500000000000000000000000.", + "`a1=169711/100000000=0.00169711`", + "`s=(1-10^-24)C-10^-27`", + "a_next = s(1-s)+s*a1 = 0.001730921627244654642552821294... .", + "(1-10^-24)*q/(1+q) = 0.001727930714600372546778004395...,", + "which is below `0.001727989140903569` by more than `5.8426*10^-8`.", + "q=(1-2*10^-24)*a_next,", + "Instead choose the independent BIT coupling `c=1/577`.", + "H={1:381024,2:400416,3:22752,4:26880,\n 5:29376,6:17376,7:26784,42:288},", + "m=64, W=28416, epsilon=10^-16,\nF=32*64^2*sum(H)=118606528512.", + "mu_1 = 2874298095721977/2890625000000000 < 199/200,", + "[999998938581682162866772413602,\n 999998938581682162866772413603]/10^30 < 999999/1000000.", + "The old `9999/10000` power cap is false at this coupling.", + "T1(n,w) <= 200 A n + 1000000 A n^(1-c) w^p1.", + "`17^128>32*16^128`", + "`32780*(17/16)*20=696575<2^20`", + "T_B2(V,e)/V <= A[801n + 4000000 n^(1-c) w^p1 + k+w+1].", + "801 + 4000000*(17/16) + 32780 + 2 + 1 = 4283584.", + "Now `a2=c(1-c)+c*a1`. Since `c>a1`,", + "| `c-a2` | `2076753/33292900000000` |", + "| `1-a2-c` | `33177502076753/33292900000000` |", + "| `1-a2-c(1-a1)` | `331776/332929` |", + "| `1-c` | `576/577` |", + "Their minimum is the first.", + "Since `17/10000 0, "a2 - C as stated, positive") + + # 2. section 1: bootstrapping at the complex rate misses the legacy target after the outer loss + s = (1 - Q(1, 10**24)) * C - Q(1, 10**27) + a_next = s * (1 - s) + s * a1 + q = (1 - 2 * Q(1, 10**24)) * a_next + k_out = (1 - Q(1, 10**24)) * q / (1 + q) + need(f"{float(a_next):.15f}" == "0.001730921627245" and str(a_next.numerator * 10**30 // a_next.denominator).startswith("1730921627244654642552821294"), "a_next digits") + need(str(k_out.numerator * 10**30 // k_out.denominator).startswith("1727930714600372546778004395"), "outer-loss digits") + shortfall = Q("0.001727989140903569") - k_out + need(Q(58426, 10**12) < shortfall < Q(58427, 10**12), "short of the legacy target by 5.8426e-8 to 5.8427e-8") + + # 3. the stopped recurrence moments + F = 32 * M * M * sum(H.values()) + need(F == 118606528512 and sum(H.values()) == 904896, "F = 32*64^2*sum(H)") + mu1 = (sum(n * Q(r, M) for r, n in H.items()) + eps * F * Q(1, M)) / W + need(mu1 == Q(2874298095721977, 2890625000000000) and mu1 < Q(199, 200), "mu_1 exact and < 199/200") + t = 1 - c + m_lo, m_hi = moment(t, H, W, eps * F) + need(m_hi - m_lo < Q(1, 10**33), "enclosure width below 1e-33") + stated = (Q(999998938581682162866772413602, 10**30), Q(999998938581682162866772413603, 10**30)) + need(stated[0] <= m_lo and m_hi <= stated[1], "mu_(576/577) inside the stated 1e-30 interval") + need(m_hi < Q(999999, 10**6) and m_lo > Q(9999, 10**4), "below 1 - 1e-6; the old 9999/10000 cap is false") + need(1 / (1 - Q(199, 200)) == 200 and 1 / (1 - Q(999999, 10**6)) == 10**6, "the two induction coefficients") + # control: dropping the fallback weight moves mu_(576/577) out of the stated interval + need(moment(t, H, W, 0)[1] < stated[0], "control: the fallback weight is needed for the stated interval") + + # 4. stock fit, wrapper and all-width coefficient + need(17 ** 128 > 32 * 16 ** 128 and 32780 * Q(17, 16) * 20 == 696575 < 2 ** 20, "fit comparisons as stated") + # 2^(20 c) < 17/16 and 2k < e at e = 2^20, with k <= 16390 e^c log2 e + ln2_lo, ln2_hi = ln_bounds(Q(2)) + need(exp_bounds(20 * c * ln2_hi)[1] < Q(17, 16), "2^(20/577) < 17/16") + need(2 * 16390 * Q(17, 16) * 20 < 2 ** 20, "2k < e at e = 2^20") + need(801 == 4 * 200 + 1 and 4000000 == 4 * 10**6, "four root calls") + need(1 - c + c * (c - a1) == 1 - a2, "n^(1-c) w^(c-a1) exponent: (1-c) + c(c-a1) = 1-a2") + need(exp_bounds((c - a1) * ln2_hi)[1] < Q(17, 16), "2^(c-a1) < 17/16") + need(a2 < c and 1 - a2 - c > Q(1, 2) and c + Q(1, 2) <= 1 - a2, "a2 < c, 1-a2-c > 1/2") + need(801 + 4000000 * Q(17, 16) + 32780 + 2 + 1 == 4283584, "coefficient 4283584") + need(Q(17, 10000) < c < Q(1, 512) and a2 < Q(1, 512) and 20 * a2 < 1, "17/10000 < c < 1/512 and 2^(20 a2) < 2") + + # 5. the gap table + gaps = {"c-a2": c - a2, "1-a2-c": 1 - a2 - c, "1-a2-c(1-a1)": 1 - a2 - c * (1 - a1), "1-c": 1 - c} + need(gaps == {"c-a2": Q(2076753, 33292900000000), "1-a2-c": Q(33177502076753, 33292900000000), + "1-a2-c(1-a1)": Q(331776, 332929), "1-c": Q(576, 577)}, "gap table") + need(gaps["1-a2-c(1-a1)"] == (1 - c) ** 2 and min(gaps, key=gaps.get) == "c-a2", "(1-c)^2 and the minimum gap") + + sel_kappa = Q(pinned("certificates/selected-result.json")["kappa"]) + print(json.dumps({ + "status": "PASS_PR4338_B2_CHAIN_CHECK", + "a2": f"{float(a2):.15f}", + "a2_minus_C": f"{float(a2 - C):.4e}", + "a2_vs_selected_bit_lower": f"{float(a2 - Q(sel['bit_lower'])):.4e}", + "mu_1": f"{float(mu1):.12f}", + "mu_576_577_gap_to_1": f"{float(1 - m_hi):.6e}", + "legacy_shortfall": f"{float(shortfall):.6e}", + "min_gap_c_minus_a2": f"{float(gaps['c-a2']):.4e}", + "selected_kappa": str(sel_kappa), + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())