diff --git a/research/pr4270-outer-exponent-check/README.md b/research/pr4270-outer-exponent-check/README.md new file mode 100644 index 0000000000..819330c44b --- /dev/null +++ b/research/pr4270-outer-exponent-check/README.md @@ -0,0 +1,80 @@ +# Independent check of #4270's conservative exponent chain + +**Claim type: an independent exact check of a written arithmetic chain, +including a certified moment enclosure. No new κ.** This does not accept +#4270. It checks no physical, hosting or analytic premise. + +## Object + +[PR #4270](https://github.com/CrocSwap/integer-mult-bounds/pull/4270) +(Ross Richardson, head `a929a3fa36301bdfcffe82afd37434dd9e3c4887`) claims a +conditional `κ = 1/580`, above the selected `0.001672660197076918`. + +Its conservative argument in `OUTER-JOIN.md` §1 and §5 rests on a chain of +explicit inequalities. Before this package, the only outside check was +thu-nmrc's comment on the PR, which replayed the registered commands under +Python 3.11 and matched the source hashes. No independent recomputation of +the chain existed. + +## Results + +Every link holds. Each is computed here with exact rationals from the +vendored text and the pooled fill's result file. + +| Link | Margin | +| --- | --- | +| Pooled moment `Σ n_r (r/73)^(1−a)/322560` at `a = C`, against 1. The certified upper bound is `1 − 7.4158·10⁻²⁵`, and the moment exceeds 1 at the bracket's upper end `C + 10⁻²⁴`. Because it straddles 1, the bracket pins `m = 73` and `W = 322560` for #4181's profile. | `7.4·10⁻²⁵` | +| `σ* = 0.99826995 > 1 − C` (so the moment at `σ*` is below 1) | `9.3·10⁻⁷` | +| `τ = 332353/332929 < σ*` | `4.9·10⁻⁸` | +| Stopped-tree leaf exponent `σ* + θ(1−σ*) < α_layer = 0.99827`. The internal exponent and the root reservation `.998` are lower still. | `4.8·10⁻⁸` | +| `Φ = 1 − (997/1000)(1 − α_layer) = 0.99827519` exactly; full-support router `β = 41544341/41616125 < Φ` | `9.8·10⁻⁸` | +| The other cost powers stay below `Φ`: `.997`, `.9981`, `3/5`, `.997τ` (the support's second term) and `.997` (the CRT `D·Tp` term) | at least `1.75·10⁻⁴` (from `.9981`) | +| `1 − Φ > 1/580` | `6.7·10⁻⁷` | +| `1/580 >` selected `κ` | `5.1·10⁻⁵` | + +**Control.** The old physical Fourier rate `.00172380303` falls short of +`1/580`, as `OUTER-JOIN.md` itself says. So the changed layer exponent is +load-bearing. + +**Reading the margins.** The tightest links are `σ* − τ`, `α_layer −` leaf +and `Φ − β`, all at about `5–10·10⁻⁸`. They pass, but any upstream change to +`τ` or `β` at that scale would need this chain rechecked. + +## Not covered + +This package does not cover: + +- the pooled native/hosting identities, the stopped-tree proof itself, the + support and Gaussian constructions, or the analytic prime and Gaussian + theorems — all of which #4270 states as premises; +- the derivation of `τ`, `β` or `Φ`'s form from their sources (only the + arithmetic on them is checked); +- the cost table's row structure (only its listed powers are checked); +- any production run, or any proof-kernel check. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/pr4270-outer-exponent-check --check-only +python3.12 -B research/pr4270-outer-exponent-check/verify.py +``` + +It prints `PASS_PR4270_OUTER_EXPONENT_CHAIN` in under a second, using only +the standard library. + +## Open next questions + +1. **Bind `τ` and `β` to their sources.** + - *Why it matters:* the chain's tightest margins (about `5·10⁻⁸`) sit on + these two constants. + - *First step:* recompute `τ = 332353/332929` from PR3599's encoded + coupling, and `β` from the full-support router's invoice. + - *Blocked by:* nothing. + +## Credit + +The audited chain is #4270's (Ross Richardson with OpenAI Codex assistance). +The pooled fill is Rohan Arun's (PR #4181). The chain cites, among others, +Jose Manuel's physical constructions and Tekalign's CRT converter. Prepared +by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) +assistance. Apache-2.0. diff --git a/research/pr4270-outer-exponent-check/SOURCES.json b/research/pr4270-outer-exponent-check/SOURCES.json new file mode 100644 index 0000000000..4ad162d174 --- /dev/null +++ b/research/pr4270-outer-exponent-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/pr4270-outer-exponent-check/TASK.json b/research/pr4270-outer-exponent-check/TASK.json new file mode 100644 index 0000000000..a8980eb594 --- /dev/null +++ b/research/pr4270-outer-exponent-check/TASK.json @@ -0,0 +1,100 @@ +{ + "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 #4270's conservative kappa = 1/580 exponent chain (OUTER-JOIN.md sections 1 and 5) with exact rationals, including a certified enclosure of the pooled moment at its stated root bracket.", + "scope_change_reason": "The card asks for independent source-bound coverage of a new paid-profile or ceiling claim; #4270 is the newest such claim above the selected kappa and had only a replay audit.", + "bottleneck_link": "#4270 proposes a conditional kappa above the selected record; its exponent chain must hold before its premises are worth reviewing.", + "budget_minutes": 30, + "stop_rule": "Stop once every link of the written chain is recomputed exactly or a link fails.", + "outcome": "completed", + "evidence": "verify.py: pooled moment straddles 1 across #4181's 1e-24 root bracket (upper 1 - 7.4e-25 at 1-C); sigma*-(1-C)=9.3e-7; sigma*-tau=4.9e-8; alpha-leaf=4.8e-8; Phi exact, Phi-beta=9.8e-8; other powers below Phi; (1-Phi)-1/580=6.7e-7; 1/580 above selected by 5.1e-5; old Fourier rate control falls short.", + "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": [ + { + "question": "Bind tau and beta to their sources.", + "why_it_matters": "The chain's tightest margins (about 5e-8) sit on these two constants.", + "first_step": "Recompute tau from PR3599's encoded coupling and beta from the full-support router invoice.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4270-outer-exponent-check/VERIFY.json b/research/pr4270-outer-exponent-check/VERIFY.json new file mode 100644 index 0000000000..01524d4955 --- /dev/null +++ b/research/pr4270-outer-exponent-check/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Vendored #4270 OUTER-JOIN.md and #4181 RESULT.json hashes and 13 phrases; certified pooled moment enclosure across the root bracket; every link of the conservative exponent chain; old-rate control." + } + ] +} diff --git a/research/pr4270-outer-exponent-check/vendor/NOTICE.md b/research/pr4270-outer-exponent-check/vendor/NOTICE.md new file mode 100644 index 0000000000..4b7265fddd --- /dev/null +++ b/research/pr4270-outer-exponent-check/vendor/NOTICE.md @@ -0,0 +1,16 @@ +# Vendored files + +These are byte-identical copies from +[PR #4270](https://github.com/CrocSwap/integer-mult-bounds/pull/4270) at head +`a929a3fa36301bdfcffe82afd37434dd9e3c4887`. + +| Vendored file | Source path in #4270 | Git blob | +| --- | --- | --- | +| `OUTER-JOIN.md` | `research/complex-pooled-full-admission/OUTER-JOIN.md` | `50cf3eefd5a4198f011bf378c5d6ddd2319feb0a` | +| `pr4181-RESULT.json` | `research/complex-pooled-full-admission/frozen/pr4181/RESULT.json` | `5a0ba7aeeb39f849e09ab15cc65afb79028a20e2` | + +They are copied, not pinned, because that PR head is not reachable from canonical main. +`verify.py` checks their SHA256 values before using them. + +`OUTER-JOIN.md` was prepared for Ross Richardson with OpenAI Codex assistance. The pooled +fill result is Rohan Arun's (PR #4181). Both are Apache-2.0, as their packages state. diff --git a/research/pr4270-outer-exponent-check/vendor/OUTER-JOIN.md b/research/pr4270-outer-exponent-check/vendor/OUTER-JOIN.md new file mode 100644 index 0000000000..50cf3eefd5 --- /dev/null +++ b/research/pr4270-outer-exponent-check/vendor/OUTER-JOIN.md @@ -0,0 +1,355 @@ +# A conservative complete conditional integer transfer + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. This composition uses Jose Manuel's physical root, support, +Fourier, ring/chirp and Gaussian constructions; Tekalign's encoded CRT +conversion; the original integer-assembly and analytic sources; and the +credited pooled supplier lineage. Their source-relative premises remain +explicit. The new result is the source-specific composition and complete +cost/error comparison, not authorship of those components. + +## Statement and proof boundary + +Under the completed physical and analytic contracts specified below, the +pooled supplier admits a fixed finite-tape integer multiplication construction +with exact output and + +``` +T(n) = O(n (log n)^(1-1/580)), +space O(n)+F_q, +kappa = 1/580 = 0.0017241379310344827586... . +``` + +This is a conditional all-parameter composition, separate from the exact +finite release and the more aggressive legacy arithmetic candidate +`0.001727989140903569`. The conservative value includes the physical root's +actual stopping rule, both support-routing directions, the full Fourier and +Gaussian calls, three CRT conversions, normalization, integer recovery, +all child-return copies, restoration and fixed compiled inventories. + +The required contracts are the pooled arbitrary-input native/common-cover +identities and whole-call hosting; the retained completed BIT/ordinary, +Compact and fixed-tape primitives; the source-relative physical root and +Gaussian refinement/locality/rounding arguments; and the stated analytic +Gaussian and prime theorems. These are mathematical premises, not conclusions +of a bounded replay. The construction does not use a rounded recursive C +child. Exact children run on one guarded grid; truncation occurs only at +the complete normalized interfaces prescribed by their source. + +`OUTER-PINS.json` freezes exact proof and constructor references. It is not +an executable export of every transitive Gaussian source. PR3935 is pinned +at `f687fa171ef760fa98a4be1289717b47dd4ee0b3`; canonical references are pinned +at `12fa8c5c844be21bfefb38a19503fbd867a11244`. The source-specific global +binding and its physical proof are in `physical_global_bridge.py` and +`PHYSICAL-GLOBAL.md` (with the local refinement in `PHYSICAL-BRIDGE.md`). +The constructor/cohort comparison and exact margins +are separated in `OUTER-DOMAIN.md`; exact normalization/error controls are +in `OUTER-CHECK.md`. No complete production-prime payload, end-to-end +Gaussian integer program, human review or formal-kernel theorem is claimed. + +## 1. The physical layer rate actually used + +Retain PR3599's completed ordinary backend and its exact encoded coupling +`1/577`; no B2 backend is needed for this theorem. Put + +``` +tau = 332353/332929, +sigma_star = 0.99826995, +alpha_layer = 0.99827, +theta_stop = 1/1000000. +``` + +The pooled complete moment is less than one at `1-C`, where +`C=0.001730980255989036959962`. Since every child ratio is strictly below +one and `sigma_star>1-C`, it is also less than one at `sigma_star`. +Moreover `tau=4n/b, +N=log2 T, +D=floor(p^(997/1000)), d=D+1, +ell=ceil(N/D), r=2^ell, +alpha_G=floor(p^(1/1000)), u=alpha_G^2. +``` + +Eventually `D>=2`, `D=2` and `T<2^b`, while +`4n/b<=T<8n/b`. Choose exactly `N-D(ell-1)` of the D target lengths to +be `r`, the remainder `r/2`, and put a long axis last. Their product is +exactly T. The actual TensorPlan parameters are `axes=D-1`, +`dimensions=D` and `d=D+1`; these names must not be interchanged. + +For each target length t choose a distinct odd prime in + +``` +((1-1/(2d))*t, (1-1/(4d))*t). +``` + +The required multiplicity is at most D for each of the two target sizes. +Baker--Harman--Pintz Theorem 1 gives a prime in each sufficiently large +interval `[x-x^(21/40),x]`. As in the retained rad20 prime argument, pack +at least D disjoint such intervals inside each required interval. The +sufficient comparison `12d^2=ceil(log2(8p))`, +`ud<=p`, `d>4w+2` for `w=ceil(sqrt(16p/u))+2`, +`L=2^ceil(log2(p^8))>=64dH` for `H=4096p^3`, and +`s_i>2(L+2H+2w)`. The target lengths have more than one complete L tile. +All descriptors have O(p) bits. The required source windows, period margins +and signed origins are those computed by the original-axis producer; no +unverified arbitrary coefficient page is accepted instead. + +All eventual conditions are fixed before numerical input. They can be +tested by encoded integer arithmetic, including the final error gate below. +Use schoolbook multiplication if a finite-size admission fails. Each +condition eventually holds; this branch therefore covers only a fixed +bounded range of n and fits the final bound after enlarging its constant. + +## 3. Complete interfaces and normalization + +Write `F_-` and `F_+` for the tensor Fourier maps on the prime box, both +normalized by `1/S`. Let `R_i x(j)=x(t_i j mod s_i)` and `R=tensor_i R_i`. +The actual Gaussian endpoint is `A_-=R F_-`; conjugating its input and +output gives `A_+=R F_+`. Since `F_+ R=R^-1 F_+`, + +``` +A_+(A_-x * A_-y) = (x cyclic-convolve y)/S^2. +``` + +Here `*` is coordinatewise multiplication. Omitting R from either source +contract, treating two normalized maps as unscaled inverses, or retaining +only one factor S would change the result. + +Initially scale each radix digit by `2^(-b-2)`, producing p-grid values +of modulus less than 1/4. Pad through S coefficients. Execute two complete +forward CRT conversions to natural prime-box order, then two completed +Gaussian calls. Copy and consume each protected output before reusing its +owner. Multiply corresponding returned Gaussian values exactly with four +signed integer word products, then truncate each component toward zero to +the p grid. Execute the opposite Gaussian call on that complete packet. + +Every Gaussian packet uses signed least-significant-bit-first components of +width `p+2`, real before imaginary. The CRT conversion treats these as +opaque complete records of width `2(p+2)`. It preserves the complete rows +and performs its actual padding, global field permutation, triangular shifts +and cropping. It checks every discarded padding bit. There are three full +CRT conversions in total, including the final inverse below. + +The synthetic Fourier maps used inside the chirp both normalize by their +polynomial-address volume M and compose to `I/M`. PR3763's completed chirp +already restores its required factors. The Gaussian theorem then supplies +`R F_s` with its exact global scale `2^gamma`. We neither add nor delete a +second normalization at these internal interfaces. + +## 4. A complete error and recovery budget + +Let `h=2^-p`, `M=T/r=2^A`, and + +``` +gamma=D(2u+ceil(log2(32p))+1), +H_err=Dp^2+32+2D. +``` + +PR3935 gives each completed Gaussian call, on any admitted half-disk input, +error below + +``` +E=2^gamma (Dp^2+4sqrt(2)M+22+2D) h + < 2^gamma T H_err h. +``` + +This includes coefficient generation, expansion, the complete chirp, +principal-core compression, all local rounding, exact `2^gamma` restoration +and final width reduction. We assume the source's analytic locality and +conditioning estimates at their stated production domain. Its reduced +p48 fixture is not evidence that this asymptotic domain was executed. + +Apply the additional encoded gate + +``` +b >= gamma+ceil(log2 H_err)+9. (1) +``` + +It holds eventually since `gamma=O(p^.999+p^.997 log p)=o(p)`. +It also implies the source guard +`p>=gamma+A+ceil(log2 H_err)+8`. Thus returned values remain in the +required disk and the retained Gaussian narrowing is valid. + +For the first two exact transforms the norm is at most 1/4. Their computed +values have norm at most `1/4+E`, eventually below .26. The product's +componentwise p-grid truncation changes its Gaussian value by less than +`2h`. Its error from the product of exact transforms is at most +`E/2+E^2+2h<=E+2h`. Its norm is below `.26^2<1/2`, so the third Gaussian +call is admissible. The exact normalized map is a contraction; the complete +three-call result therefore has error below `2E+2h` from the desired +scaled cyclic convolution. + +Now multiply each numerator exactly by `S^2`, restore the scale +`2^(2b+4)`, and round the real component to its unique nearest integer. +The resulting coefficient error is strictly less than + +``` +S^2 2^(2b+4) (2E+2h) + < 64 H_err 2^(gamma-b) + <= 1/8 (by (1)). +``` + +This uses `S 1/580, +``` + +the strict positive difference absorbs the remaining fixed logarithm. +Using `p=Theta(log n)` proves the stated conditional exponent. The target +`1/580` is above the selected `0.001672660197076918`. The old physical +Fourier rate `.00172380303` does not itself reach `1/580`; the changed +complex layer supplies the additional margin. We make no measured-runtime +claim and no uniform claim as any of these fixed margins tends to zero. + +## 6. What this does and does not close + +This written construction joins explicit completed source contracts and +accounts for every outer invocation, format, normalization, error and paid +restoration term. The finite all-provider release, global source binding, +bounded exact controls and constructor evidence support different parts of +that argument and must remain separately labelled. + +The inherited universal native/hosting, physical primitive/refinement and +Gaussian analytic hypotheses still require scientific admission. The source +code is a fixed-controller realization argument, not an emitted universal +transition table. The new integer wrapper is specified by the complete +encoded sequence above; an end-to-end production execution is not claimed. +The selected frontier remains unchanged pending independent review. diff --git a/research/pr4270-outer-exponent-check/vendor/pr4181-RESULT.json b/research/pr4270-outer-exponent-check/vendor/pr4181-RESULT.json new file mode 100644 index 0000000000..5a0ba7aeeb --- /dev/null +++ b/research/pr4270-outer-exponent-check/vendor/pr4181-RESULT.json @@ -0,0 +1,31 @@ +{ + "status": "AUTHOR_CHECKED_FINITE_CONDITIONAL_CONSTRUCTION", + "calls": 3240, + "fourth_calls": 1080, + "selector": "tick t < 1080 uses the four-entry word of its orientation", + "profile": { + "1": 8060040, + "2": 2310120, + "3": 751788, + "4": 327240, + "5": 66420, + "8": 25920, + "48": 138492 + }, + "idle": { + "3": 22788, + "5": 1620, + "48": 138492 + }, + "root_lower": "865490127994518479981/500000000000000000000000", + "root_upper": "1730980255989036959963/1000000000000000000000000", + "root_lower_decimal": "0.001730980255989036959962", + "root_upper_decimal": "0.001730980255989036959963", + "conditional_kappa": "17309802559890369599619999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "conditional_kappa_decimal": "0.0017309802559890369599619999999999999999999998999999999999999999999999", + "predecessor": "PR4088 research/staged544-mixed-fourth-entry", + "predecessor_upper": "1730979115670792472761/1000000000000000000000000", + "gain_over_pr4088_upper": "11403182444872009999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "gain_over_pr4088_upper_float": 1.140318244487201e-09, + "gain_percent": 6.587706542290104e-05 +} \ No newline at end of file diff --git a/research/pr4270-outer-exponent-check/verify.py b/research/pr4270-outer-exponent-check/verify.py new file mode 100644 index 0000000000..fa2b2908b8 --- /dev/null +++ b/research/pr4270-outer-exponent-check/verify.py @@ -0,0 +1,127 @@ +#!/usr/bin/env python3 +"""Independent exact check of #4270's conservative exponent chain (kappa = 1/580). + +Standard library only; no code from #4270. Constants come from its OUTER-JOIN.md +and the pooled fill's RESULT.json, vendored byte-identically (see vendor/NOTICE.md). +The pooled moment 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] +VENDORED = { + "vendor/OUTER-JOIN.md": "bfb4677ee82ffc070be880eca87af05fd096686b464dfd5268cee1b27afa453e", + "vendor/pr4181-RESULT.json": "d823509ea38e545db6c287a85c00bc4257825fb2710728dfc776c8801d2becd9", +} +PHRASES = [ + "tau = 332353/332929,", "sigma_star = 0.99826995,", "alpha_layer = 0.99827,", "theta_stop = 1/1000000.", + "`C=0.001730980255989036959962`", "the root reservation exponent is still `.998`.", + "Phi = 1-(997/1000)(1-alpha_layer) = 0.99827519.", "`beta=41544341/41616125 1/580,", "Fourier rate `.00172380303` does not itself reach `1/580`", + "`O(V [g^alpha_layer log p + (g+1)^tau (log p)^(1+tau)]).`".strip("`"), +] +M, W = 73, 322560 # pooled moment width and role count, as in #4270's ledger and #4088/#4181 + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def atanh_ln(x, terms=45): + z = (x - 1) / (x + 1) + s = 2 * sum(z ** (2 * k + 1) / (2 * k + 1) for k in range(terms + 1)) + return s, s + 2 * z ** (2 * terms + 3) / ((2 * terms + 3) * (1 - z * z)) + + +def ln_bounds(x): + k = (x.numerator // x.denominator).bit_length() - 1 + a, b = atanh_ln(Q(2)) + c, d = atanh_ln(x / 2 ** k) + return k * a + c, k * b + d + + +def exp_bounds(y, terms=30): + s, term = Q(0), Q(1) + for k in range(terms + 1): + s += term + term = term * y / (k + 1) + return s, s + 3 * term + + +def moment_bounds(profile, a): + """sum_r n_r (r/M)^(1-a) / W, with (r/M)^(1-a) = (r/M) exp(a ln(M/r)).""" + lo = hi = Q(0) + for r, n in profile.items(): + ln_lo, ln_hi = ln_bounds(Q(M, r)) + lo += n * Q(r, M) * exp_bounds(a * ln_lo)[0] + hi += n * Q(r, M) * exp_bounds(a * ln_hi)[1] + return lo / W, hi / W + + +def main(): + for rel, digest in VENDORED.items(): + need(hashlib.sha256((HERE / rel).read_bytes()).hexdigest() == digest, f"vendored {rel}") + text = (HERE / "vendor/OUTER-JOIN.md").read_text() + need(all(p in text for p in PHRASES), "OUTER-JOIN.md phrases") + pins = {row["path"]: row["sha256"] for row in json.loads((HERE / "SOURCES.json").read_text())["files"]} + sel_path = ROOT / "certificates/selected-result.json" + need(hashlib.sha256(sel_path.read_bytes()).hexdigest() == pins["certificates/selected-result.json"], "selected pin") + selected_kappa = Q(json.loads(sel_path.read_text())["kappa"]) + + fill = json.loads((HERE / "vendor/pr4181-RESULT.json").read_text()) + profile = {int(r): n for r, n in fill["profile"].items()} + root_lo, root_hi = Q(fill["root_lower"]), Q(fill["root_upper"]) + C = Q("0.001730980255989036959962") + need(C == root_lo and root_hi - root_lo == Q(1, 10**24), "C is the pooled fill's certified root bracket") + + # 1. The pooled moment straddles 1 across the bracket (this pins M and W given the profile). + at_c, above = moment_bounds(profile, root_lo), moment_bounds(profile, root_hi) + need(at_c[1] < 1 < above[0], "pooled moment < 1 at 1-C and > 1 just above") + margin = 1 - at_c[1] + + tau, sigma, alpha, theta = Q(332353, 332929), Q("0.99826995"), Q("0.99827"), Q(1, 10**6) + # 2. Stopped tree: moment(sigma) <= moment(1-C) < 1 needs sigma > 1-C; tau < sigma < alpha. + need(sigma > 1 - C, "sigma_star > 1 - C") + need(tau < sigma < alpha, "tau < sigma_star < alpha_layer") + internal = sigma - theta * (sigma - tau) + leaf = sigma + theta * (1 - sigma) + need(internal < alpha and leaf < alpha and Q("0.998") < alpha, "stopped-tree and reservation exponents") + + # 3. Outer layer: Phi as written, and every listed cost power strictly below it. + phi = 1 - Q(997, 1000) * (1 - alpha) + need(phi == Q("0.99827519"), "Phi = 0.99827519 exactly") + beta = Q(41544341, 41616125) + powers = {"full-support router beta": beta, "Gaussian payload .997": Q("0.997"), + "Gaussian payload .9981": Q("0.9981"), "scalar words 3/5": Q(3, 5), + "support second term .997 tau": Q("0.997") * tau, "CRT D Tp term .997": Q("0.997")} + for name, power in powers.items(): + need(power < phi, f"{name} < Phi") + + # 4. The conclusion: 1 - Phi > 1/580 > selected kappa; the old rate alone falls short. + kappa = Q(1, 580) + need(1 - phi > kappa > selected_kappa, "1 - Phi > 1/580 > selected kappa") + need(Q("0.00172380303") < kappa, "control: the old physical Fourier rate does not reach 1/580") + + print(json.dumps({ + "status": "PASS_PR4270_OUTER_EXPONENT_CHAIN", + "pooled_moment_upper_at_1_minus_C": f"1 - {float(margin):.6e}", + "sigma_star_minus_1_minus_C": f"{float(sigma - (1 - C)):.3e}", + "sigma_star_minus_tau": f"{float(sigma - tau):.3e}", + "alpha_minus_leaf_exponent": f"{float(alpha - leaf):.3e}", + "phi_minus_beta": f"{float(phi - beta):.3e}", + "one_minus_phi_minus_kappa": f"{float(1 - phi - kappa):.3e}", + "kappa_minus_selected": f"{float(kappa - selected_kappa):.3e}", + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())