diff --git a/research/production-reference-gap/CHECKPOINT.md b/research/production-reference-gap/CHECKPOINT.md new file mode 100644 index 0000000000..dde622a7c9 --- /dev/null +++ b/research/production-reference-gap/CHECKPOINT.md @@ -0,0 +1,34 @@ +# Wave 5: literal production Reference gap + +Status: lead-reviewed source proof and registered normal/optimized checks +PASS. Committed-byte/mode gate and lead remote publication remain next. +No remote publication is asserted by this local checkpoint. +Base: 7c49fe32c55de02c2c873655c804b16e4c3fef0a. +Branch: research/production-reference-gap-20261109. +Worker: analytic_join; worktree: worker-analytic-wave5. + +Result: the actual Reference.for_cap allocation already forces +E>=47+ceil(log2 p^2), from its own normalized qbar and gauge allowance. +Combined with the credited ideal gap and exact outward endpoint budget, +its literal narrow_gap exceeds (1/8-2^-46)/p^2 >1/(16p^2) whenever the +fine-theta/lower-alpha domain and existing constructor cuts are legal. +No larger target or precision is introduced. This is not an assertion for +arbitrary manually specified References or all theta/alpha values. + +Prior result #4648 supplies the ideal/half-gap budget; RAW-GAUSSIAN-PROOF +supplies the actual certificate and for_cap error bound. Neither predecessor +ties that certificate's positive production threshold to for_cap's existing +normalized conditioning quantity. forward-fine-theta-conditioning concerns +the broad kernel and explicitly excludes this narrow claim. + +Executed: 37 actual for_cap constructors, separate rational log/pi/positive +exponential checks, 505 integer budget cases and 6 failure controls. +The largest original target period is 2^37, with lazy source coordinates; +no full period or original weight bank was materialized. +Proof, receipts, source hashes and bounded reproduction are local files. + +Complete: source pins, package metadata, independent lead review and +registered normal/-O replays. Next: committed-byte/mode verification and +lead publication. Old +published diagonal at b00d64b6204e83d468dde2db7480a2822e6940aa is frozen. +This independent package uses canonical inputs only. No new kappa. diff --git a/research/production-reference-gap/NOTICE.md b/research/production-reference-gap/NOTICE.md new file mode 100644 index 0000000000..b3fcca1ca4 --- /dev/null +++ b/research/production-reference-gap/NOTICE.md @@ -0,0 +1,28 @@ +# Attribution + +Prepared for @CubeJerry with substantial OpenAI assistance in source analysis, +proofs, exact independent calculations, implementation and packaging. +Apache-2.0. + +The unchanged canonical Reference, normalized Gaussian and rational circuit +source is Jose Manuel/jmbarrancoml's work with substantial OpenAI Codex +assistance. Its source credits Vlado Vojdanovski, Jeremy Kothe, Cinna Davis, +Chafik Boukhalfa, Mason Hale and the retained mathematical/compiler lineage. +The source files are authenticated external inputs with unchanged notices. + +The ideal majorant/half-gap bound in CrocSwap/integer-mult-bounds#4648 is +unpaidmoon's result with Cursor Grok assistance, crediting LOG-A/PR1673, +the PR1786 fine-prime audit and Cinna Davis's PR4100 integration. Its generic +rounding budget is a premise, not a new result here. The actual cap error, +interval width and positive conditioning enclosure are likewise credited +canonical source theorems. + +The new contribution is the implication from the literal cap allocator's +normalized qbar to its already-sufficient global narrow certificate budget. +The proof does not assume that narrow inverse in order to certify it. +The broad `forward-fine-theta-conditioning` work is distinct and credited +as prior overlap context, not imported as a narrow proof. + +Independent direct positive-series checks use classical rational series; +they import no retained interval backend. Finite evidence and AI lead review +do not imply human or proof-kernel acceptance. No new kappa is claimed. diff --git a/research/production-reference-gap/PR-DESCRIPTION.md b/research/production-reference-gap/PR-DESCRIPTION.md new file mode 100644 index 0000000000..1d8e940283 --- /dev/null +++ b/research/production-reference-gap/PR-DESCRIPTION.md @@ -0,0 +1,72 @@ +## Why this matters + +The actual canonical `Reference.for_cap` computes a narrow row-gap certificate +but leaves a positive value conditional. The Core/halo production family then +requires that same literal certificate to reach `1/(16p^2)`. A generic ideal +gap or unspecified high-precision rounding budget does not establish the +constructor's actual admission. + +## Exact result + +For every integer p>=2, radius R>=1, target t>=1 and legal cap/cut request, +under the source domain `theta in [1/(4p^2),1/p^2]` and +`pi alpha^2>=4 log(16p)`, the unchanged constructor returns + +`reference.narrow_gap > (1/8-2^-46)/p^2 > 1/(16p^2)`. + +No extra precision, larger target, changed Reference or different rounding +is introduced. The source's own normalized cap quantity has `qbar>=16pB`, +forcing `Q*>=2^21 alpha^2 pB` and `E>=47+ceil(log2 p^2)`. That existing +allocation funds the full reference error and both outward endpoint excesses. +The global narrow inverse is not assumed to derive its own admission. + +## Novelty and predecessors + +CrocSwap/integer-mult-bounds#4648 supplies the ideal/half-gap budget and leaves +actual W/precision binding open. The canonical raw Gaussian proof supplies +the literal certificate and cap error, while leaving positivity conditional. +This package supplies the missing allocation-to-certificate implication. +It does not reclaim those predecessor estimates or prove a new general +Gaussian theorem. `forward-fine-theta-conditioning` concerns the broad inverse +and explicitly excludes this narrow statement. + +All 14 scientific inputs and card provenance are pinned to canonical base +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The original constructor/interval +bodies execute unchanged; no source body is projected by this adapter. + +## Reproduction and checks + +```sh +python3 -B research/production-reference-gap/verify.py +python3 -O -B research/production-reference-gap/verify.py +python3 scripts/research_package.py --package research/production-reference-gap --check-only +python3 scripts/research_package.py --package research/production-reference-gap +python3 scripts/check_research_commit.py --package research/production-reference-gap --check-modes +``` + +Expected status is `PASS_PRODUCTION_REFERENCE_GAP`. Exact source-bound evidence +covers 37 actual cap constructions, 505 integer interval-budget cases and 6 +failure controls. A separate rational log/pi/direct-positive-Taylor oracle +checks alpha ceilings and actual certificates without importing the retained +interval backend. The largest period 2^37 and cap 2^15 remain lazy metadata; +no huge field, weight bank or native production run is claimed. + +## Costs, limitations and kappa status + +**No new kappa.** This removes one source-specific numerical admission, +conditional on the explicitly credited ideal, scalar enclosure and constructor +theorems. It does not collectively discharge the five selected assumptions. +Legal period cuts, complete shared-context delivery, source H/ideal N and +full transform integration, physical/native contracts and final recovery +remain required. Arbitrary manually specified References can still fail; +the controls demonstrate that scope boundary. + +The proof records an explicit sufficient onset for the unchanged O(p) +allocation bounds and keeps source descriptor costs, O(p^2 log p) offline +weights, subsequent page/Schur work and backing separate. No constructor-only +bill is passed off as the cost of the complete Gaussian transform. + +Prepared for **@CubeJerry** with substantial OpenAI assistance. Jose Manuel/ +jmbarrancoml, Mason Hale, unpaidmoon/#4648 and the retained PR1673/PR1786/ +PR4100 contributors retain their credit in NOTICE.md. Independent lead review +is separate evidence, not human or formal proof-kernel acceptance. diff --git a/research/production-reference-gap/PR-TITLE.txt b/research/production-reference-gap/PR-TITLE.txt new file mode 100644 index 0000000000..64c85acf15 --- /dev/null +++ b/research/production-reference-gap/PR-TITLE.txt @@ -0,0 +1 @@ +Prove the actual cap constructor funds the production narrow gap (no new kappa) diff --git a/research/production-reference-gap/PROOF.md b/research/production-reference-gap/PROOF.md new file mode 100644 index 0000000000..52464a89f3 --- /dev/null +++ b/research/production-reference-gap/PROOF.md @@ -0,0 +1,285 @@ +# The actual cap constructor already funds the production narrow gap + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. Apache-2.0. +Base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +**A source-specific all-parameter admission lemma; no new kappa.** + +## 1. Precise result and prior boundary + +Fix an integer p>=2. The source data satisfy + +`theta=e/S in [1/(4p^2),1/p^2]`, `rho=1+theta`, +`alpha` a positive integer, `a=pi alpha^2>=4 log(16p)`. + +Here and below log means natural logarithm. Use the literal canonical +`rational-unitary-fft/gaussian_reference.py` class method + +`Reference.for_cap(raw,S,e,alpha,B,R,t)`, (1) + +with dyadic B>=1, 2B<=S, rational R>=1 and integer t>=1. Retain its exact +canonical numerical source cohort. Require the constructor's legal-period +checks `2w (1/8-2^-46)/p^2 > 1/(16p^2)`. (2) + +Thus `narrow_inverse_bounds` is present. No extra precision, larger target, +different rounding, altered Reference or post hoc repair is needed. The +result is uniform in the source length, excess, cap, allowed radius and +target. Its gap implication needs no new eventual onset once the named +source inequalities and legal cuts hold. + +The outer source uses `alpha=ceil(sqrt((4/pi)log(16p)))`, which satisfies +the lower inequality. Its separate source-prime supply and legal-period +conditions are not established here. Section 5 gives an explicit sufficient +onset for the usual upper-alpha and O(p) precision estimates, and retains +the actual cost of source descriptors and later weight preparation. + +This closes the conditional positivity/production-size admission of the +actual cap constructor. It is not a theorem that every manually specified +Reference has this gap. It does not prove the ideal/full-transform identity, +physical delivery, native suppliers, final recovery or an unconditional +multiplication theorem. + +### What is already proved + +CrocSwap/integer-mult-bounds#4648 (`narrow-row-half-gap`) supplies + +`gamma=1-exp(-2a theta)-5exp(-2a)>=1/(8p^2)` (3) + +under the stated lower-alpha/theta domain, as well as a generic perturbation +budget. It explicitly leaves the actual stored-band precision/rounding +binding open. We credit (3); we do not re-prove or reclaim it. + +The canonical `RAW-GAUSSIAN-PROOF.md` §5 defines the actual computed +certificate d and proves that a positive d bounds the true rational narrow +reference row gap. It leaves positivity conditional. Its uniform-cap +construction proves the error bound used below. `GAUSSIAN-PROOF.md` §3 proves +the scalar outward interval width and the conditioning enclosure. These +are exact pinned source premises, not inferred from this finite replay. + +`forward-fine-theta-conditioning` studies the different broad inverse +conditioning bound and explicitly excludes the narrow kernel. The nearby +column, Schur and old factorwise-rounding results have different hypotheses. +The new implication is that the **existing normalized conditioning quantity +inside (1)** already forces enough reference accuracy to make its literal +narrow certificate pass. Neither a stronger general Gaussian estimate nor a +new exponential algorithm is claimed. + +## 2. The actual allocation is already more than large enough + +These are literal expressions in `Reference.for_cap`: + +`F*=1+alpha^2 theta(B^2+B+1)`, +`G*=alpha 2^ceil(8F*)`, +`H*=2 qbar(B,1/(alpha^2 rho))`, `Q*=G*^2 H*`, +`E=t+ceil(log2(8(R+1)Q*^2))`. (4) + +The normalized Gaussian constructor computes qbar from a positive certified +lower interval endpoint l_c for + +`exp(-pi/(4c))`, `c=1/(alpha^2 rho)`, + +by the exact formula `qbar=B/l_c`. Since `l_c<=exp(-a rho/4)` and rho>=1, + +`qbar >= B exp(a rho/4) >= B exp(log(16p)) =16pB`. (5) + +This uses the actual allocated rational quantity, not the norm of an +unknown narrow inverse. F*>=1 and alpha>=1 imply `G*>=2^8 alpha`, hence + +`Q* >= (2^8 alpha)^2 * 2 * 16pB + = 2^21 alpha^2 pB`. (6) + +With R>=1, B>=1 and t>=1, the unchanged integer allocation in (4) obeys + +`E >= t+46+ceil(log2(p^2)) + >= 47+ceil(log2(p^2))`. (7) + +In particular `2^-E<=2^-47/p^2`. No growth assumption on t or R was needed. +The global narrow inverse was never assumed to exist in deriving (5)-(7), +so the argument is not a circular use of its own conditioning certificate. +The relevant lower bound follows directly from the positive scalar enclosure +already constructed for the normalized cap allowance. + +## 3. Literal cutoffs, tails and outward certificate precision + +Set A=alpha^2 rho^2. The same function chooses + +`w=ceil(sqrt((E+5)/(3alpha^2)))`, +`W=max(ceil(A),ceil(sqrt(A(E+5)/3)),2w+2)`, +`b_E=E+3+ceil(log2(2max(w,W)+1))`. (8) + +It computes square-root ceilings by integer arithmetic and rejects illegal +period cuts. The unchanged uniform-cap source theorem supplies + +`E_N=reference.errors['narrow']<=2^-E`, `b_E>=E+3`. (9) + +Specifically, E_N is the actual rational geometric tail plus +`(2w+1)2^-b_E`. This is not an unnamed per-entry precision constant or a +floating estimate. The original function checks the rational bound before +returning. Its proof bounds both tails and coefficient row/column allowances +for the actual cutoffs (8). We consume that constructor theorem unchanged. + +The literal `Reference` constructor uses working precision + +`J=2(b_E+ceil(8alpha^2 rho^2)+16)+32 >= 2b_E+64` (10) + +for its adjacent and distant exponential enclosures. The predecessor proves +that an exponential enclosure at J>=16 has width at most + +`omega(J)=512 J^2 2^-J`. (11) + +For every integer b>=8 and J>=2b+64, + +`omega(J)<=2^-b`. (12) + +Here is a direct all-integer check of (12). J^2 2^-J decreases for J>=3, +so it suffices to put J=2b+64. After cancellation the assertion is +`512(2b+64)^2<=2^(b+64)`. At b=8 it is +`512*80^2<=2^72`. Increasing b multiplies its left side by +`((2b+66)/(2b+64))^2<2`, while the right side doubles. This proves (12) +for all b>=8, not just the verifier's finite range. + +Because a true exponential lies inside its outward enclosure, the excess +of its upper endpoint over the true value is at most the enclosure width. +Write those two nonnegative excesses as eta_adj and eta_dist. From (9)-(12), + +`eta_adj+5eta_dist+E_N + <=6*2^-b_E+2^-E + <=(7/4)2^-E + <2*2^-E <=2^-46/p^2`. (13) + +There is no exact-floor/separation requirement in this argument. It concerns +the actual rational endpoints returned by the existing interval method. + +## 4. The literal certificate clears the production threshold + +The actual constructor sets + +`d=1-adjacent_hi-5*distant_hi-E_N`. + +Subtract the explicitly funded excess (13) from the credited ideal +majorant gap (3). This gives exactly (2). The branch that computes +`narrow_inverse_bounds` is therefore taken on every source admitted by +Section 1; its positivity is no longer a separate hypothesis for this +particular constructor. + +By the existing same-reference theorem, d bounds the row gap of the actual +rational narrow H, including original period crossings and identity holes. +Its principal restrictions inherit that gap. Thus the source's existing +inverse-infinity bound is at most16p^2, and the least dyadic normalizer +obeys `u<=ceil(log2(16p^2))`. The usual dimension-independent column/inverse +estimates continue to use their actual physical bandwidth. We do not +replace a row estimate by a column estimate or improve an assembled kappa. + +This consequence applies when the common Reference supplied to every Core +and halo window is generated once by (1). A caller cannot create independently +rerounded References and invoke this lemma to identify their overlaps. A +manually constructed reference with the same theta/alpha but small entry +precision can fail; the replay contains an actual negative certificate of +that kind. Small alpha or theta outside the domain can also make (1)'s +certificate negative even though the cap constructor itself returns normally. + +## 5. Explicit production onset, widths and complete setup cost + +Now use the source's actual alpha ceiling, cap +`B=2^floor((15/16)log2 p)`, fine theta, and admitted radius/target with +`t+log2 R=O(p)`. Rational descriptors are supplied with polynomial bit height; +in the physical caller the radius can be a dyadic bound with O(p)-bit +description. A numerical value close to1 does not excuse an arbitrarily +long rational descriptor. + +A convenient sufficient onset for the following estimates is `p>=2^200`. +Let L=log(16p). Then L>100, and alpha<=sqrt(4L/pi)+1 gives + +`4L<=a<=4L+4sqrt(pi L)+pi<4L+8sqrt(L)+4<=5L`. + +The last inequality holds at L=100 and increases thereafter. Using pi>3 +and p>=16 gives `alpha^2<2L<=4log2 p`. Also + +`F*-1<=12 log2(p) p^-1/8 <=192 p^-1/16 <=1`. (14) + +The elementary maximum of `log2(p)/p^(1/16)` is +`16/(exp(1) log(2))<16`, using exp(1)>2 and log(2)>1/2. Finally +`(2^200)^(1/16)>192`, so the last step in (14) holds at the stated onset. +Thus `G*<=2^16 alpha` there. + +For completeness the same actual conditioning enclosure also has a simple +upper qbar bound. Its precision rule certifies width at most +`2^(-a_c-2)`, where `a_c=ceil(2/c)`, while the true positive exponential is +at least `2^-a_c`. Hence `l_c>=3/4 exp(-pi/(4c))` and +`qbar<= (4/3)B exp(a rho/4)`. Since rho<=5/4 and a<=5L, + +`qbar <= (4/3)B(16p)^2`. + +For p>=16, `4log2 p<=p`, so the preceding alpha bound gives `alpha^2<=p`. +Together with B<=p^(15/16) and (14), this yields the deliberately loose bound +`Q*<=2^43 p^4`. In (4) +this gives the explicit sufficient upper allocation + +`E<=t+ceil(log2 R)+90+8ceil(log2 p)`. (15) + +In particular E=O(p) without increasing the existing target. Equations (8) +then give the source's established + +`w=O(sqrt(p/log p))`, `W=O(sqrt(p log p)+log p)`, +`b_E=O(p)`, `J=O(p)`. + +The cap constructor does not enumerate the original S or S+e coordinates. +Its normalized Gaussian constructor may scan up to B candidate cutoffs; +each interval/rational operation has polynomial cost in the actual descriptor +and precision heights. A safe unamortized constructor tariff is +`B poly(p)` in this production family, with the declared source-description +read, parsing, interval arithmetic, allocation, comparison and disposal +included. More generally retain the actual B and descriptor/working heights; +O(log R) alone is not a representation-size bound. The theorem does not +reprice a later full matrix/Schur/compiler preparation by this constructor +tariff. + +The same constructor records full-cell weight precision + +`P_weight=ceil(2alpha^2/theta)+b_E+7=O(p^2 log p+p)`. + +Those larger weights remain offline setup, with actual later generation, +tables, caches and retained backing charged by the original source/physical +caller. The kernel precision adds `ceil(8alpha^2 w)+4=O(sqrt(p log p))` bits, +preserving O(p). This lemma neither lowers those widths nor declares the +original source field, context delivery or coefficient pages free. + +The strict period checks remain explicit. Their eventual satisfaction uses +the caller's original-axis size and the usual source-prime construction; we +do not infer it from the small fixtures or from (2). A complete caller may +retain its ordinary small-parameter fallback. The gap inequality itself +already holds for every p>=2 whose stated constructor/geometry domain holds. + +## 6. Executed checks and limitations + +The checker authenticates 14 canonical scientific inputs plus the frozen +task-card provenance. It executes the complete, unchanged canonical +`Reference.for_cap`, including the actual normalized Gaussian constructor, +interval cutoffs and literal rational gap. The checker executes the complete +unchanged constructor rather than an extracted allocation formula; its +existing AST parsing/compilation remains charged. + +The 37 cases cover p in {2,3,7,19,73,74,257,1024,65536}, near both fine-theta +endpoints, cap 1 and the actual dyadic p^(15/16) cap, with extra rational/large +radius and target cases. The largest target period is 2^37 and largest cap +2^15. These are metadata/constructor cases: no 2^37-entry field or huge +full-cell weight is generated. Empty original entry/weight/kernel caches and +the absent hole listing are checked explicitly. The actual alpha ceiling is +certified with independent rational log/pi bounds. + +A separately implemented direct positive Taylor/remainder oracle, inverted +after its exact rational calculation, corroborates the literal certificate's +two exponential terms. It imports no retained interval backend. The complete +source allocations and all resulting certificate hashes are recorded. The +505 finite integer checks support the interval-budget induction; the proof +of that induction is separate. Six controls distinguish low entry precision, +bad alpha, bad theta, invalid cap, illegal cuts and inadequate input radius. + +The universal argument still cites the prior ideal-majorant and outward +interval/constructor theorems. This is source-specific assumption reduction, +not independent human or proof-kernel acceptance of every cited source. +All five selected framework assumptions, global source integration and final +multiplication recovery are not collectively discharged by this result. diff --git a/research/production-reference-gap/README.md b/research/production-reference-gap/README.md new file mode 100644 index 0000000000..9a03032cbb --- /dev/null +++ b/research/production-reference-gap/README.md @@ -0,0 +1,103 @@ +# The actual cap constructor already funds the production narrow gap + +Prepared for **@CubeJerry**, with substantial OpenAI assistance. **No new kappa.** +Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. + +The canonical `Reference.for_cap` computes a narrow row-gap certificate but +leaves its positivity conditional. This package proves that the source's +fine-theta/alpha domain and the constructor's **existing** allocation already +force its literal rational `narrow_gap` above `1/(16p^2)`. No larger target, +extra precision, altered rounding or replacement Reference is needed. + +For every integer p>=2, legal cap/cut request, radius R>=1 and target t>=1, +with `theta in [1/(4p^2),1/p^2]` and `pi alpha^2>=4 log(16p)`, the result is + +`reference.narrow_gap > (1/8-2^-46)/p^2 > 1/(16p^2)`. + +This removes that separate production admission for this particular source +constructor. It does not apply to every manually specified Reference and +does not discharge the complete multiplication theorem's five assumptions. + +## Why the implication is new + +CrocSwap/integer-mult-bounds#4648 supplies the ideal narrow majorant gap and +generic half-gap rounding budget. It leaves actual W/precision binding open. +The canonical raw Gaussian proof supplies the literal certificate and the +cap constructor's error bound but keeps a positive certificate conditional. +The new observation joins those statements through the actual allocated +normalized Gaussian quantity: + +`qbar>=16pB`, `Q*>=2^21 alpha^2 pB`, +`E>=47+ceil(log2 p^2)`. + +Those are lower bounds on the **existing source allocation**, derived before +the global narrow inverse has been assumed to exist. The actual two outward +endpoint excesses and complete reference error then cost less than +`2^-46/p^2`. This is not a new general Gaussian or perturbation theorem. +`forward-fine-theta-conditioning` concerns the broad inverse and explicitly +excludes the narrow statement proved here. + +## Proof, costs and evidence + +[PROOF.md](PROOF.md) gives the all-parameter implication, exact source formulas, +source-derived precision and cutoff estimates, and a convenient explicit +`p>=2^200` onset for the usual O(p) allocation bounds. The gap implication +itself needs no new onset once its source domain and legal cuts hold. +The actual O(p^2 log p) offline weight precision, descriptor heights, later +coefficient/Schur/page work and retained backing remain charged. + +[SOURCES.json](SOURCES.json) pins all 14 live canonical scientific inputs and +the frozen task-card provenance. [source.py](source.py) opens the unchanged +constructor cohort. [independent.py](independent.py) supplies separate exact +rational log/pi and direct-positive-Taylor checks. [verify.py](verify.py) and +[evidence/REPLAY.json](evidence/REPLAY.json) record 37 actual `for_cap` cases, +505 integer interval-budget checks and 6 failure controls. + +Cases span p=2 through 65536, near both fine-theta endpoints, cap 1 and the actual +p^(15/16) cap, and extra rational/large radius and target values. The largest +target period is 2^37 and largest cap is 2^15. These are lazy constructor +metadata: no complete original field or large full-cell weight bank is +materialized. The fixtures do not claim source-prime generation or a native +production run. Controls exhibit actual negative certificates for low +manual entry precision, bad alpha and bad theta; invalid cap, cuts and +radius also reject. + +## Reproduce + +From the repository root with standard-library CPython 3.12: + +```sh +python3 -B research/production-reference-gap/verify.py +python3 -O -B research/production-reference-gap/verify.py +python3 scripts/research_package.py --package research/production-reference-gap --check-only +python3 scripts/research_package.py --package research/production-reference-gap +python3 scripts/check_research_commit.py --package research/production-reference-gap --check-modes +``` + +Expected scientific status is `PASS_PRODUCTION_REFERENCE_GAP`. All source +identity, numerical and negative-control tests use explicit checks under +optimized Python. Finite checks corroborate the written proof; they are not +universal or proof-kernel acceptance. + +## Open next questions + +1. Can every production Core/halo context be delivered from one such shared + cap-generated Reference at the complete source cost? This package supplies + its gap admission; period legality, context geometry and owned coefficient + delivery remain separate obligations. +2. Can the complete rational H-versus-ideal N/source-transform comparison be + joined to the actual normalized inverse and remaining diagonal? The + certificate theorem and component comparisons are credited; the complete + source prefix/suffix and final recovery remain required. +3. Can the remaining native, routing and physical lifecycle premises be + independently discharged at the same caller? This constructor lemma + supplies no such physical theorem and no new complete kappa. + +## Credit + +See [NOTICE.md](NOTICE.md). The same canonical Reference, Gaussian and interval +sources retain Jose Manuel/jmbarrancoml, Mason Hale and the original project +contributors' credit. The ideal/half-gap result is unpaidmoon/#4648, with +the PR1673/PR1786/PR4100 lineage. Substantial AI assistance was used; any +independent lead review is recorded separately, without human or kernel +acceptance claims. diff --git a/research/production-reference-gap/SOURCES.json b/research/production-reference-gap/SOURCES.json new file mode 100644 index 0000000000..0039e09a1f --- /dev/null +++ b/research/production-reference-gap/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "research/rational-unitary-fft/exact.py", + "usage": "input", + "git_blob": "aae41e6acfb2e5a4fafdd85727891eb746b57b42", + "sha256": "c9b89d7357210af69865690ba12e695366961f8b501a8fab9d0fefe3fb30c479" + }, + { + "path": "research/rational-unitary-fft/engine.py", + "usage": "input", + "git_blob": "e9f2f2b08dc2bc4c646e47dca92059351ca89384", + "sha256": "9e36aee0835e6b1b62997433581f88b5a434ccab8ae43e5c25d1deaaf1ebf653" + }, + { + "path": "research/rational-unitary-fft/triangular.py", + "usage": "input", + "git_blob": "2bd8de01a7ac80de7e6b9f8252bc69d0e0a291e8", + "sha256": "46780d95ddebfed22e8f0c18565fe2e768250afa5beeb31f450292cc06f7ec11" + }, + { + "path": "research/rational-unitary-fft/generator.py", + "usage": "input", + "git_blob": "d761d3c88b1685fb64d92d69f699b8218c9ec30f", + "sha256": "827ef9fe1bd664859995892b59843c390f7969c938fb7e1e6dc585c31a54b555" + }, + { + "path": "research/rational-unitary-fft/full.py", + "usage": "input", + "git_blob": "7f85ad1a89e81b7dfc6b54e7bd9547120e86d5d3", + "sha256": "1f42d5f2858564ffb320e54ba6aa29651025491569823e25006bf5862457b803" + }, + { + "path": "research/rational-unitary-fft/gaussian.py", + "usage": "input", + "git_blob": "52ad2e1d605f5f7d669234567c25bc087306dd44", + "sha256": "08155357fd39b5fd7959f51f1d205b6511b8577b51520d793c89f92368b399ab" + }, + { + "path": "research/rational-unitary-fft/gaussian_reference.py", + "usage": "input", + "git_blob": "92addfabde50655cea7ad5a84cca9cff5457adee", + "sha256": "ed4d0908646e391d4a0ea32c988a0301a1793a72294ac7058a664ed3283ca3c3" + }, + { + "path": "research/certified-gaussian-recovery/intervals.py", + "usage": "input", + "git_blob": "91d458865aa026bdf0d59653a4ecbfe3a178ecbc", + "sha256": "159d2a7d32a8cc7c8f56632a8ef127308b984a0a6753c9d6bdccacc6e7d6d4df" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md", + "usage": "input", + "git_blob": "1fb549d24a419abb50f5b772437d87e48c65fe06", + "sha256": "3f683643a0c0b45d58ec09ebe511e4006cd103e38753f82a4ce21a8570383358" + }, + { + "path": "research/narrow-row-half-gap/README.md", + "usage": "input", + "git_blob": "eb659ee46bc86d9799fd6aa7a0fc507bd3dd5ce9", + "sha256": "6b84925dbb647f1b5bec1140ffd5e8d4a211d99f90fd49c511764ce656a36830" + }, + { + "path": "research/forward-fine-theta-conditioning/README.md", + "usage": "input", + "git_blob": "8e2831a88a7edc504daeba91261546437a2a5375", + "sha256": "8aafb8704479eefe1772b7f0d68284bac02ac916473f1a72c258be598c18e964" + }, + { + "path": "research/capped-fusion-t74-k554/outer/check_gaugefree.py", + "usage": "input", + "git_blob": "3fbb4a1b2acc3d5120d93d2ffd7cd5007d4f7f0e", + "sha256": "5274b2838f322dc56a88570e4f9262fcd3857cd387160ad138e083ccdfbe9761" + }, + { + "path": "research/rational-unitary-fft/GAUSSIAN-PROOF.md", + "usage": "input", + "git_blob": "b7c9cad252943d519cb5ed4318c163798b9865a7", + "sha256": "9e6c567704bedcbd6f394ad736a874f918ef72444f49b65515aec32c0a1ed88e" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/production-reference-gap/TASK.json b/research/production-reference-gap/TASK.json new file mode 100644 index 0000000000..cb9e9187fd --- /dev/null +++ b/research/production-reference-gap/TASK.json @@ -0,0 +1,107 @@ +{ + "actual_scope": "Discharge the positive production-size admission of the literal canonical Reference.for_cap narrow_gap from the existing allocator and precise fine-theta/lower-alpha domain.", + "ai_assistance": "Substantial OpenAI assistance in source audit, proof, exact independent rational oracles, code and packaging. Independent lead review, if included, is separately recorded; no human or proof-kernel acceptance.", + "author": "Prepared for @CubeJerry", + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "bottleneck_link": "Core/halo numerical contracts require a common Reference with certified narrow_gap at least 1/(16p^2); the actual allocator leaves positivity conditional.", + "budget_minutes": 100, + "evidence": "Source-specific all-parameter proof: actual qbar and gauge force E>=47+ceil(log2 p^2), funding every literal endpoint excess and the complete reference error. No precision or target increase. Complete canonical constructor plus independent rational oracle checks.", + "finite_domain": "37 actual for_cap requests across p in {2,3,7,19,73,74,257,1024,65536}, fine-theta endpoints, cap1/actual cap, extra radius/target cases; 505 integer interval-budget cases; 6 failure controls. No random search.", + "independent_previous_package": false, + "no_new_kappa": true, + "open_questions": [ + { + "blocked_by": "Complete context delivery and inherited physical/native guards remain open.", + "first_step": "Bind original-period/legal-cut geometry and the prepared context streams to this actual constructor output.", + "question": "Can every production Core/halo context be delivered from one shared cap-generated Reference at the complete source cost?", + "why_it_matters": "The present result supplies its gap admission but does not implement the shared-context source delivery." + }, + { + "blocked_by": "Whole source-transform and recovery integration are outside this certificate result.", + "first_step": "Pin the actual H/ideal N comparison and outer extraction/scale interface before composing.", + "question": "Can the complete rational H-versus-ideal N/source-transform comparison join the actual inverse and remaining diagonal?", + "why_it_matters": "Final integer recovery needs the full exact target and accumulated prefix/suffix errors." + }, + { + "blocked_by": "No physical/native runtime is audited here.", + "first_step": "Select one literal native or ownership contract with its full paid model interface.", + "question": "Can the remaining native, route and lifecycle premises be discharged at the same caller?", + "why_it_matters": "A constructor admission is not a complete multiplication theorem." + } + ], + "original_card": { + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "uniform-transfer-audit", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ] + }, + "outcome": "completed", + "previous_public_commit": "b00d64b6204e83d468dde2db7480a2822e6940aa", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Previous public bridge/ledger/diagonal packages still assumed the actual Reference production gap. #4648 proves a generic budget but not this source allocator implication. The new scope derives the literal constructor admission, while excluding broad conditioning and full H-versus-ideal-N.", + "scope_status": "refined", + "seed": 78, + "source_projection_scope": "No adapter source projection. Complete canonical Reference.for_cap and Gaussian constructor execute; the canonical Gaussian constructor retains its own pinned Tsec extraction unchanged. No native or whole-period payload replay.", + "stop_rule": "Freeze after the literal all-parameter implication, complete source/precision cost and bounded independent controls are reviewed. Do not reprove the credited ideal half-gap, broaden to H-versus-ideal N or claim a complete multiplication theorem.", + "task_id": "uniform-transfer-audit", + "tracks": [ + "75-84 independent verification/formalization", + "60-74 adversarial audit" + ], + "wave": 5, + "worker": "analytic_join" +} diff --git a/research/production-reference-gap/VERIFY.json b/research/production-reference-gap/VERIFY.json new file mode 100644 index 0000000000..c028bd1b11 --- /dev/null +++ b/research/production-reference-gap/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rational-unitary-fft/exact.py", + "research/rational-unitary-fft/engine.py", + "research/rational-unitary-fft/triangular.py", + "research/rational-unitary-fft/generator.py", + "research/rational-unitary-fft/full.py", + "research/rational-unitary-fft/gaussian.py", + "research/rational-unitary-fft/gaussian_reference.py", + "research/certified-gaussian-recovery/intervals.py", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/rational-unitary-fft/RAW-GAUSSIAN-PROOF.md", + "research/narrow-row-half-gap/README.md", + "research/forward-fine-theta-conditioning/README.md", + "research/capped-fusion-t74-k554/outer/check_gaugefree.py", + "research/rational-unitary-fft/GAUSSIAN-PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate exact source inputs; execute unchanged cap constructors, independently certify source parameters/certificate, and reject out-of-scope or underfunded controls.", + "timeout_seconds": 180 + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "Authenticate exact source inputs; execute unchanged cap constructors, independently certify source parameters/certificate, and reject out-of-scope or underfunded controls.", + "timeout_seconds": 180 + } + ] +} diff --git a/research/production-reference-gap/evidence/LEAD-REVIEW.json b/research/production-reference-gap/evidence/LEAD-REVIEW.json new file mode 100644 index 0000000000..f0072d2f3f --- /dev/null +++ b/research/production-reference-gap/evidence/LEAD-REVIEW.json @@ -0,0 +1,14 @@ +{ + "status": "reviewed-under-stated-source-contracts", + "reviewer": "lead orchestrator /root", + "source": "Independent lead messages in the current run, 2026-11-09", + "method": "Direct review of the complete proof against literal canonical Reference.for_cap, Reference.__init__, Gaussian.qbar and #4648 README; no worker-verifier import for the proof argument.", + "findings": [ + "The lower allocation chain Qstar>=2^21 alpha^2 p B -> E>=47+ceil(log2 p^2) is valid.", + "The full certificate loss is at most (7/4)*2^-E under the source enclosure and constructor contracts.", + "No circular assumption of the global narrow inverse enters the allocation bound.", + "The full constructor AST work remains charged; alpha^2<=p is made explicit in the loose upper Qstar bound.", + "The 2^200 onset is limited to alpha/precision estimates; legal-period/global source onsets remain separate." + ], + "not_human_or_kernel_acceptance": true +} diff --git a/research/production-reference-gap/evidence/REPLAY.json b/research/production-reference-gap/evidence/REPLAY.json new file mode 100644 index 0000000000..263976c640 --- /dev/null +++ b/research/production-reference-gap/evidence/REPLAY.json @@ -0,0 +1,750 @@ +{ + "actual_for_cap_cases": 37, + "fixtures": [ + { + "allocation_sha256": "8529fa882dbcb5264c7f5fd06603c4990162294bfad69d26b502cff27687406e", + "alpha": 3, + "cap": 1, + "entry_bits": 133, + "error_bits": 124, + "excess": 241, + "gap_scaled_lower_pass": true, + "gap_sha256": "6ee5e10e7f6746a86043fb57e32540ed58b0ba39133ea68a0996278801c22a56", + "p": 2, + "radius": "1", + "source_halfwidth": 3, + "source_size": 3855, + "target": 1, + "target_halfwidth": 21, + "target_size": 4096, + "theta": "241/3855", + "weight_precision": 428, + "working_bits": 494 + }, + { + "allocation_sha256": "4585bfbb89d3dfd81200c4904434a1d390da3d21ace3acc8e0e65e836be1c76f", + "alpha": 3, + "cap": 1, + "entry_bits": 297, + "error_bits": 287, + "excess": 819, + "gap_scaled_lower_pass": true, + "gap_sha256": "d1d166f53af7841cd98fa145c9b413b81e323a109138d153336090af204f62ac", + "p": 2, + "radius": "1", + "source_halfwidth": 4, + "source_size": 3277, + "target": 1, + "target_halfwidth": 37, + "target_size": 4096, + "theta": "819/3277", + "weight_precision": 377, + "working_bits": 884 + }, + { + "allocation_sha256": "b2b7b3a0ca520cae6ead598c0a81dc610ca5fed6efadd5d578210311e2cfd074", + "alpha": 3, + "cap": 1, + "entry_bits": 104, + "error_bits": 95, + "excess": 111, + "gap_scaled_lower_pass": true, + "gap_sha256": "e0a13eb7c802e9ab7a560689ffa401e5d124182b180d047a4e9c238d8d93bda6", + "p": 3, + "radius": "1", + "source_halfwidth": 2, + "source_size": 3985, + "target": 1, + "target_halfwidth": 18, + "target_size": 4096, + "theta": "111/3985", + "weight_precision": 758, + "working_bits": 426 + }, + { + "allocation_sha256": "d63f6025468d539c9ce582c816afab32692abfd4da931179a6db84e1675beeec", + "alpha": 3, + "cap": 2, + "entry_bits": 138, + "error_bits": 129, + "excess": 111, + "gap_scaled_lower_pass": true, + "gap_sha256": "0ca9a4efce6718f1918194b67cf91856da1af9c3ce159c5913ff4f540e494fb3", + "p": 3, + "radius": "1", + "source_halfwidth": 3, + "source_size": 3985, + "target": 1, + "target_halfwidth": 21, + "target_size": 4096, + "theta": "111/3985", + "weight_precision": 792, + "working_bits": 494 + }, + { + "allocation_sha256": "d24f68e7621f2bb1cf70a1aa57c0e068647feff9dfd4d9072ae1529417d91031", + "alpha": 3, + "cap": 1, + "entry_bits": 173, + "error_bits": 164, + "excess": 409, + "gap_scaled_lower_pass": true, + "gap_sha256": "ba8990fad5d23a6d525ba47ef9dea5a3ab5438fa49f018f8533608a31755e0af", + "p": 3, + "radius": "1", + "source_halfwidth": 3, + "source_size": 3687, + "target": 1, + "target_halfwidth": 26, + "target_size": 4096, + "theta": "409/3687", + "weight_precision": 343, + "working_bits": 588 + }, + { + "allocation_sha256": "52168801f3aecc0f1f7c9278d83b60d043e7bc6a5ec889754ed25c1de1645b9f", + "alpha": 3, + "cap": 2, + "entry_bits": 304, + "error_bits": 294, + "excess": 409, + "gap_scaled_lower_pass": true, + "gap_sha256": "c4f9224867c4752f30f5ac70e35c496ed5a6018ef013b7b5458caa5abae1278f", + "p": 3, + "radius": "1", + "source_halfwidth": 4, + "source_size": 3687, + "target": 1, + "target_halfwidth": 34, + "target_size": 4096, + "theta": "409/3687", + "weight_precision": 474, + "working_bits": 850 + }, + { + "allocation_sha256": "5b5e9aaffb52f38a6930f959e57aae2d3bf8a939037c8b573f9595ce360a98d0", + "alpha": 3, + "cap": 1, + "entry_bits": 83, + "error_bits": 74, + "excess": 21, + "gap_scaled_lower_pass": true, + "gap_sha256": "2004a03afb18ad15b7959f1be43b3b8a51ec4b64bfd65038853a96e90c8aa046", + "p": 7, + "radius": "1", + "source_halfwidth": 2, + "source_size": 4075, + "target": 1, + "target_halfwidth": 16, + "target_size": 4096, + "theta": "21/4075", + "weight_precision": 3583, + "working_bits": 376 + }, + { + "allocation_sha256": "4afc9e8b891deb8c944723591c1d18ac8a1a5864a4f431f99aa2d0cb40e991cd", + "alpha": 3, + "cap": 4, + "entry_bits": 111, + "error_bits": 102, + "excess": 21, + "gap_scaled_lower_pass": true, + "gap_sha256": "93a47824e35ddf5028afdd74a9bfeb833c450bcfdcc3e25dbb3d178b01838760", + "p": 7, + "radius": "1", + "source_halfwidth": 2, + "source_size": 4075, + "target": 1, + "target_halfwidth": 19, + "target_size": 4096, + "theta": "21/4075", + "weight_precision": 3611, + "working_bits": 432 + }, + { + "allocation_sha256": "394e37d45ffa403d554049f9450fd5a8d0f84a65a161627f2b6e1a12c99226f3", + "alpha": 3, + "cap": 1, + "entry_bits": 96, + "error_bits": 87, + "excess": 81, + "gap_scaled_lower_pass": true, + "gap_sha256": "645b5786138f21cd6791cd2ee19ce69276809a58b867a11e75e3c8de69064022", + "p": 7, + "radius": "1", + "source_halfwidth": 2, + "source_size": 4015, + "target": 1, + "target_halfwidth": 17, + "target_size": 4096, + "theta": "81/4015", + "weight_precision": 996, + "working_bits": 406 + }, + { + "allocation_sha256": "7f86730d54997c329baa0bf9fab5dd6b8825214400bce965d5efa830335ac30e", + "alpha": 3, + "cap": 4, + "entry_bits": 204, + "error_bits": 195, + "excess": 81, + "gap_scaled_lower_pass": true, + "gap_sha256": "1f771ec63d838f442d0aa464eea4d6f03baba24ef6a6dd65c595abde3f88587a", + "p": 7, + "radius": "1", + "source_halfwidth": 3, + "source_size": 4015, + "target": 1, + "target_halfwidth": 25, + "target_size": 4096, + "theta": "81/4015", + "weight_precision": 1104, + "working_bits": 622 + }, + { + "allocation_sha256": "3a7ba4ef1f5b6443700675ad94997f431b92d75aefc68dd07882317ec2fac39a", + "alpha": 3, + "cap": 1, + "entry_bits": 79, + "error_bits": 70, + "excess": 12, + "gap_scaled_lower_pass": true, + "gap_sha256": "dfdcd9e7613e14be542008409362320870e0b4a67262c256400aa91aef1d05a6", + "p": 19, + "radius": "1", + "source_halfwidth": 2, + "source_size": 16372, + "target": 1, + "target_halfwidth": 16, + "target_size": 16384, + "theta": "3/4093", + "weight_precision": 24644, + "working_bits": 368 + }, + { + "allocation_sha256": "a9a15f130a2a4e82bf2eadf58b0c448e86bd5b6d3c9248a3ba5f1b85ecdf805e", + "alpha": 3, + "cap": 8, + "entry_bits": 97, + "error_bits": 88, + "excess": 12, + "gap_scaled_lower_pass": true, + "gap_sha256": "1a5557368cf5b58ae6fd5061a6a3ee6bed1cbe3716d7a1f765bcd62e5ce37290", + "p": 19, + "radius": "1", + "source_halfwidth": 2, + "source_size": 16372, + "target": 1, + "target_halfwidth": 17, + "target_size": 16384, + "theta": "3/4093", + "weight_precision": 24662, + "working_bits": 404 + }, + { + "allocation_sha256": "1ce549164b9983a2c5e994cb4db8a2532589d9105baf81b7a026831ebc6f04ab", + "alpha": 3, + "cap": 1, + "entry_bits": 79, + "error_bits": 70, + "excess": 45, + "gap_scaled_lower_pass": true, + "gap_sha256": "2ed9514fd332eedca19f30cd2c5930f0cd50baf264ed0e4064adce029d0926da", + "p": 19, + "radius": "1", + "source_halfwidth": 2, + "source_size": 16339, + "target": 1, + "target_halfwidth": 16, + "target_size": 16384, + "theta": "45/16339", + "weight_precision": 6622, + "working_bits": 368 + }, + { + "allocation_sha256": "98027717d4afed3defeaafc9c37bc01d5031d9f0b37a9ee31324b8202777b946", + "alpha": 3, + "cap": 8, + "entry_bits": 141, + "error_bits": 132, + "excess": 45, + "gap_scaled_lower_pass": true, + "gap_sha256": "f040132319d4842f80c8617b03bfd8e3655a5b824f5cadc75c890da5a12d9246", + "p": 19, + "radius": "1", + "source_halfwidth": 3, + "source_size": 16339, + "target": 1, + "target_halfwidth": 21, + "target_size": 16384, + "theta": "45/16339", + "weight_precision": 6684, + "working_bits": 492 + }, + { + "allocation_sha256": "9ab8c3e5619d4bd037e2877756eb2e3aeec03b8be8ead076045e983151fac7b3", + "alpha": 3, + "cap": 1, + "entry_bits": 79, + "error_bits": 70, + "excess": 13, + "gap_scaled_lower_pass": true, + "gap_sha256": "3d9d0c845d46d96b2d301dec4c001a5c381b75881220f79c02fd23dad4efad99", + "p": 73, + "radius": "1", + "source_halfwidth": 2, + "source_size": 262131, + "target": 1, + "target_halfwidth": 16, + "target_size": 262144, + "theta": "13/262131", + "weight_precision": 363037, + "working_bits": 368 + }, + { + "allocation_sha256": "e786847a1732d12792f75954a82ca348994d1831fe9df29797ff2f2a87855af5", + "alpha": 3, + "cap": 32, + "entry_bits": 101, + "error_bits": 92, + "excess": 13, + "gap_scaled_lower_pass": true, + "gap_sha256": "b6781fba0f01a6a6bb6af6280d5f718736daa505daa9fcab6c46c7e492872f44", + "p": 73, + "radius": "1", + "source_halfwidth": 2, + "source_size": 262131, + "target": 1, + "target_halfwidth": 18, + "target_size": 262144, + "theta": "13/262131", + "weight_precision": 363059, + "working_bits": 412 + }, + { + "allocation_sha256": "d4bade2db0da1b4be75c575f088790794d12e42bdef1b4077e9e1a802599acee", + "alpha": 3, + "cap": 1, + "entry_bits": 79, + "error_bits": 70, + "excess": 49, + "gap_scaled_lower_pass": true, + "gap_sha256": "2c5b3722dd89503a492af5b5e186dda83e14a17ceae5c9ffc202ad5fc5c4b0b2", + "p": 73, + "radius": "1", + "source_halfwidth": 2, + "source_size": 262095, + "target": 1, + "target_halfwidth": 16, + "target_size": 262144, + "theta": "49/262095", + "weight_precision": 96366, + "working_bits": 368 + }, + { + "allocation_sha256": "5af656ef2f9a9fe2bff3d3b08243d94bb7475e97cefd50d990f6d1cd24e2a6db", + "alpha": 3, + "cap": 32, + "entry_bits": 145, + "error_bits": 136, + "excess": 49, + "gap_scaled_lower_pass": true, + "gap_sha256": "c4b8091a33080a81947ae81eecf04e6bff513b8386674e545a79d1a59ef17056", + "p": 73, + "radius": "1", + "source_halfwidth": 3, + "source_size": 262095, + "target": 1, + "target_halfwidth": 21, + "target_size": 262144, + "theta": "49/262095", + "weight_precision": 96432, + "working_bits": 500 + }, + { + "allocation_sha256": "dafb9c5b79c00b4d358b312a833e7ddfaa9a45aeba25becb652ad3ccf8f56352", + "alpha": 4, + "cap": 1, + "entry_bits": 97, + "error_bits": 88, + "excess": 12, + "gap_scaled_lower_pass": true, + "gap_sha256": "e070f13bdd0834623f89888b8b016d51a4f7e7f47927af5099ae833fedde2e08", + "p": 74, + "radius": "1", + "source_halfwidth": 2, + "source_size": 262132, + "target": 1, + "target_halfwidth": 23, + "target_size": 262144, + "theta": "3/65533", + "weight_precision": 699123, + "working_bits": 516 + }, + { + "allocation_sha256": "7b8c4c61ad03833094ea51995a64421c08b454fd0bd8c3dc89af014d1318a1e0", + "alpha": 4, + "cap": 32, + "entry_bits": 131, + "error_bits": 122, + "excess": 12, + "gap_scaled_lower_pass": true, + "gap_sha256": "3e109cb03deb748cdc987482059543c869e798d33e7c013e6c0b03f3e4e85ea5", + "p": 74, + "radius": "1", + "source_halfwidth": 2, + "source_size": 262132, + "target": 1, + "target_halfwidth": 27, + "target_size": 262144, + "theta": "3/65533", + "weight_precision": 699157, + "working_bits": 584 + }, + { + "allocation_sha256": "335b8592b01e5776565ddf1a818cfcd707b978b8157e080a81fffad0f9ae3bba", + "alpha": 4, + "cap": 1, + "entry_bits": 97, + "error_bits": 88, + "excess": 47, + "gap_scaled_lower_pass": true, + "gap_sha256": "2aaf2b8b54759de3c0ac0387086a087460e717ec5c83c675910c84c11a30da78", + "p": 74, + "radius": "1", + "source_halfwidth": 2, + "source_size": 262097, + "target": 1, + "target_halfwidth": 23, + "target_size": 262144, + "theta": "47/262097", + "weight_precision": 178554, + "working_bits": 516 + }, + { + "allocation_sha256": "b8355d2f92a65e9fc2078285032a2021195eb2b35897335c193d04d0057528ac", + "alpha": 4, + "cap": 32, + "entry_bits": 204, + "error_bits": 194, + "excess": 47, + "gap_scaled_lower_pass": true, + "gap_sha256": "034acb9cba883185677a7415652917d935b181ac6492ad691b12ca9df61738ec", + "p": 74, + "radius": "1", + "source_halfwidth": 3, + "source_size": 262097, + "target": 1, + "target_halfwidth": 33, + "target_size": 262144, + "theta": "47/262097", + "weight_precision": 178661, + "working_bits": 730 + }, + { + "allocation_sha256": "c645162f9cd054363c2a1ccecf42d36e10d77283bc1cf1338654e4d6bdccf666", + "alpha": 4, + "cap": 1, + "entry_bits": 97, + "error_bits": 88, + "excess": 16, + "gap_scaled_lower_pass": true, + "gap_sha256": "6ab6c1b2f5d3788c4511adefcf37c96b0a994e69cc944b72ec80c3e39322e992", + "p": 257, + "radius": "1", + "source_halfwidth": 2, + "source_size": 4194288, + "target": 1, + "target_halfwidth": 23, + "target_size": 4194304, + "theta": "1/262143", + "weight_precision": 8388680, + "working_bits": 516 + }, + { + "allocation_sha256": "43d92edcb057a8c4141988e5c1ad69baa862147dd88f0c1fee74d8e5a88440b4", + "alpha": 4, + "cap": 128, + "entry_bits": 143, + "error_bits": 134, + "excess": 16, + "gap_scaled_lower_pass": true, + "gap_sha256": "2c064e4cc6e015ec4e7360c127d47685fd24323038b730415aa18077623fe74a", + "p": 257, + "radius": "1", + "source_halfwidth": 2, + "source_size": 4194288, + "target": 1, + "target_halfwidth": 28, + "target_size": 4194304, + "theta": "1/262143", + "weight_precision": 8388726, + "working_bits": 608 + }, + { + "allocation_sha256": "10aeee84f0635e5bab5ecda4f6e18ce269577966bda87f08acdf5e1c0e85288b", + "alpha": 4, + "cap": 1, + "entry_bits": 97, + "error_bits": 88, + "excess": 63, + "gap_scaled_lower_pass": true, + "gap_sha256": "4686528bd92dc75d698a240a590da941a68f630cd173fc33afba9fa982e44eb7", + "p": 257, + "radius": "1", + "source_halfwidth": 2, + "source_size": 4194241, + "target": 1, + "target_halfwidth": 23, + "target_size": 4194304, + "theta": "63/4194241", + "weight_precision": 2130513, + "working_bits": 516 + }, + { + "allocation_sha256": "165b0fa5a1cecf78d4b9003bd2c96b630c4d1b928a91470958b2d557c4237f8a", + "alpha": 4, + "cap": 128, + "entry_bits": 236, + "error_bits": 226, + "excess": 63, + "gap_scaled_lower_pass": true, + "gap_sha256": "e028823f8735d92bcbe0cbb412fb64d34032ea036eb24c16106aea6e5c386dfb", + "p": 257, + "radius": "1", + "source_halfwidth": 3, + "source_size": 4194241, + "target": 1, + "target_halfwidth": 36, + "target_size": 4194304, + "theta": "63/4194241", + "weight_precision": 2130652, + "working_bits": 794 + }, + { + "allocation_sha256": "762fb36dbc6c01ce0eb7bbf52d64aae8c3b0d16f3515a678841d12c3cb85fe11", + "alpha": 4, + "cap": 1, + "entry_bits": 97, + "error_bits": 88, + "excess": 8, + "gap_scaled_lower_pass": true, + "gap_sha256": "7457fdaa13d3a5954775b3ad98c896d9b4e59050988b9938dd7947c8971fe2f4", + "p": 1024, + "radius": "1", + "source_halfwidth": 2, + "source_size": 33554424, + "target": 1, + "target_halfwidth": 23, + "target_size": 33554432, + "theta": "1/4194303", + "weight_precision": 134217800, + "working_bits": 516 + }, + { + "allocation_sha256": "0a4b0becdc6e9ac1b33d4f0972d546251e61089b429fad3a6de898bfecb13b89", + "alpha": 4, + "cap": 512, + "entry_bits": 147, + "error_bits": 138, + "excess": 8, + "gap_scaled_lower_pass": true, + "gap_sha256": "6f13855e5a5e4f4b894b768813f7b99442ae697da25086d2dec8589d4029b0af", + "p": 1024, + "radius": "1", + "source_halfwidth": 2, + "source_size": 33554424, + "target": 1, + "target_halfwidth": 28, + "target_size": 33554432, + "theta": "1/4194303", + "weight_precision": 134217850, + "working_bits": 616 + }, + { + "allocation_sha256": "9af970795f19af6a6013c2930bc221ddd180bb97dad4e595e46af63514570a9f", + "alpha": 4, + "cap": 1, + "entry_bits": 97, + "error_bits": 88, + "excess": 31, + "gap_scaled_lower_pass": true, + "gap_sha256": "34a87cb4544cfa1d6eb7fc18254dff36cbb655d48b4f12f9936b9ba42be76dcb", + "p": 1024, + "radius": "1", + "source_halfwidth": 2, + "source_size": 33554401, + "target": 1, + "target_halfwidth": 23, + "target_size": 33554432, + "theta": "31/33554401", + "weight_precision": 34636906, + "working_bits": 516 + }, + { + "allocation_sha256": "07dc494ce55ed16866a6e55d7fe7d9261445670ef898dfccdafc5db6b82adc65", + "alpha": 4, + "cap": 512, + "entry_bits": 240, + "error_bits": 230, + "excess": 31, + "gap_scaled_lower_pass": true, + "gap_sha256": "7f1264ff30c354638ffff7524cdbcb55c56e3052474332271600ddba893bcbe4", + "p": 1024, + "radius": "1", + "source_halfwidth": 3, + "source_size": 33554401, + "target": 1, + "target_halfwidth": 36, + "target_size": 33554432, + "theta": "31/33554401", + "weight_precision": 34637049, + "working_bits": 802 + }, + { + "allocation_sha256": "46226eb970bc85b5bce40ac168a32cf6829650ae5b2578a3a4f4922e5972b956", + "alpha": 5, + "cap": 1, + "entry_bits": 118, + "error_bits": 109, + "excess": 8, + "gap_scaled_lower_pass": true, + "gap_sha256": "8e61f05e7251391b6923f3f91a7ecc53482eaee97ca9d07486bc3340fecad232", + "p": 65536, + "radius": "1", + "source_halfwidth": 2, + "source_size": 137438953464, + "target": 1, + "target_halfwidth": 31, + "target_size": 137438953472, + "theta": "1/17179869183", + "weight_precision": 858993459275, + "working_bits": 702 + }, + { + "allocation_sha256": "b766ac653d52839c81f2f3950f0dc916e8abfc9f7c5a8d9cd5a2cf0f08d1fa2b", + "alpha": 5, + "cap": 32768, + "entry_bits": 197, + "error_bits": 187, + "excess": 8, + "gap_scaled_lower_pass": true, + "gap_sha256": "f8cb5801b082562154016874c3109e40883c575ffac86a6b9f0a96435fe08959", + "p": 65536, + "radius": "1", + "source_halfwidth": 2, + "source_size": 137438953464, + "target": 1, + "target_halfwidth": 41, + "target_size": 137438953472, + "theta": "1/17179869183", + "weight_precision": 858993459354, + "working_bits": 860 + }, + { + "allocation_sha256": "57cefbd8b4c85d71de692965dc08afc9ce02ce1e8a5a7edd4d99b56c5ef722ed", + "alpha": 5, + "cap": 1, + "entry_bits": 118, + "error_bits": 109, + "excess": 31, + "gap_scaled_lower_pass": true, + "gap_sha256": "28e1879db5e2b19e01ef6c34e1ee2fdbb2a99940c7e8c826b8274144e9e3a2be", + "p": 65536, + "radius": "1", + "source_halfwidth": 2, + "source_size": 137438953441, + "target": 1, + "target_halfwidth": 31, + "target_size": 137438953472, + "theta": "31/137438953441", + "weight_precision": 221675731482, + "working_bits": 702 + }, + { + "allocation_sha256": "59695f9555d33059c1bce4c9d279b6a2045094f5aa88cea8ec663d876bb968c1", + "alpha": 5, + "cap": 32768, + "entry_bits": 341, + "error_bits": 331, + "excess": 31, + "gap_scaled_lower_pass": true, + "gap_sha256": "3bfcde3c564037e2d4065c4dbdfead07a0b79c102c6095b0ff5e8e1c0b47580a", + "p": 65536, + "radius": "1", + "source_halfwidth": 3, + "source_size": 137438953441, + "target": 1, + "target_halfwidth": 53, + "target_size": 137438953472, + "theta": "31/137438953441", + "weight_precision": 221675731705, + "working_bits": 1148 + }, + { + "allocation_sha256": "3489addce184b22a348cd9e10cb10341095bd66404a28e070fd93931113808ac", + "alpha": 3, + "cap": 1, + "entry_bits": 149, + "error_bits": 140, + "excess": 241, + "gap_scaled_lower_pass": true, + "gap_sha256": "b19db2f3b094f14c0ae4281d05979c91b474f157693190efcf66381683b54b50", + "p": 2, + "radius": "3/2", + "source_halfwidth": 3, + "source_size": 3855, + "target": 17, + "target_halfwidth": 23, + "target_size": 4096, + "theta": "241/3855", + "weight_precision": 444, + "working_bits": 526 + }, + { + "allocation_sha256": "dc78fbd6d87cac538e20525f9a95049dc2da5a036f6ec4dc2354446c1ef0a9e8", + "alpha": 3, + "cap": 8, + "entry_bits": 149, + "error_bits": 140, + "excess": 12, + "gap_scaled_lower_pass": true, + "gap_sha256": "67e30d80fbbfd05f2b7fc613148a213da0ae15b800264ba2f29cae6c369ca78b", + "p": 19, + "radius": "65536", + "source_halfwidth": 3, + "source_size": 16372, + "target": 38, + "target_halfwidth": 21, + "target_size": 16384, + "theta": "3/4093", + "weight_precision": 24714, + "working_bits": 508 + }, + { + "allocation_sha256": "f6acf4b6f5fbfd09de2ba45b4dad368d8eb117180ba1bfc3e149b0111b3dd2c8", + "alpha": 4, + "cap": 32, + "entry_bits": 206, + "error_bits": 196, + "excess": 12, + "gap_scaled_lower_pass": true, + "gap_sha256": "dca41601e2a715aa270f9f8eaae4e9c0d340eda029db83a82f75a994abced8cf", + "p": 74, + "radius": "3", + "source_halfwidth": 3, + "source_size": 262132, + "target": 74, + "target_halfwidth": 33, + "target_size": 262144, + "theta": "3/65533", + "weight_precision": 699232, + "working_bits": 734 + } + ], + "independent_interval_budget_cases": 505, + "negative_controls": 6, + "scope": "Actual canonical for_cap constructor and literal gap certificate; no physical/native or complete Gaussian replay.", + "source_inputs": 15, + "status": "PASS_PRODUCTION_REFERENCE_GAP" +} diff --git a/research/production-reference-gap/independent.py b/research/production-reference-gap/independent.py new file mode 100644 index 0000000000..8bae384974 --- /dev/null +++ b/research/production-reference-gap/independent.py @@ -0,0 +1,93 @@ +"""Exact rational logarithm/positive-series oracle, separate from Mason's code. + +Classical series are credited; this is a checker, never a production tariff. +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from functools import lru_cache + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def ceil_log2(value): + value = Q(value) + need(value > 0, "positive independent logarithm") + k, bound = 0, Q(1) + if value >= 1: + while bound < value: + k, bound = k + 1, bound * 2 + return k + while bound / 2 >= value: + k, bound = k - 1, bound / 2 + return k + + +@lru_cache(None) +def pi_box(bits=100): + def atan_inverse(d): + total = Q(0) + n = 0 + while True: + total += Q((-1) ** n, (2 * n + 1) * d ** (2 * n + 1)) + n += 1 + tail = Q(1, (2 * n + 1) * d ** (2 * n + 1)) + if tail < Q(1, 1 << (bits + 8)): + other = total + (-1) ** n * tail + return min(total, other), max(total, other) + a, b = atan_inverse(5), atan_inverse(239) + lo, hi = 16 * a[0] - 4 * b[1], 16 * a[1] - 4 * b[0] + scale = 1 << bits + return Q((lo * scale).__floor__(), scale), Q((hi * scale).__ceil__(), scale) + + +@lru_cache(None) +def log_box(integer, bits=100): + need(type(integer) is int and integer >= 1, "positive exact logarithm input") + k = integer.bit_length() - 1 + mantissa = Q(integer, 1 << k) + def local(x): + y = (x - 1) / (x + 1) + total, power = Q(0), y + for n in range(bits + 10): + total += 2 * power / (2 * n + 1) + power *= y * y + tail = 2 * power / ((2 * n + 3) * (1 - y * y)) + if tail < Q(1, 1 << (bits + 8)): + return total, total + tail + raise ValueError("bounded independent logarithm series") + a, b = local(Q(2)), local(mantissa) + return k * a[0] + b[0], k * a[1] + b[1] + + +def actual_alpha(p): + pi_lo, pi_hi = pi_box() + ln_lo, ln_hi = log_box(16 * p) + alpha = 1 + while alpha * alpha * pi_lo < 4 * ln_hi: + alpha += 1 + need((alpha - 1) ** 2 * pi_hi < 4 * ln_lo, + "finite alpha certificate separates the actual source ceiling") + return alpha + + +@lru_cache(None) +def decay_box(factor, bits=90): + factor = Q(factor) + need(factor >= 0, "nonnegative independent decay argument") + # A proved coarse bound avoids huge positive Taylor values when unnecessary. + if 3 * factor >= bits + 8: + return Q(0), Q(1, 1 << (3 * factor).__floor__()) + plo, phi = pi_box(bits + 16) + lo, hi = factor * plo, factor * phi + termlo = termhi = total_lo = total_hi = Q(1) + for n in range(1, 8 * (bits + 1) + 500): + termlo, termhi = termlo * lo / n, termhi * hi / n + total_lo, total_hi = total_lo + termlo, total_hi + termhi + if hi < n + 2: + tail = termhi * hi / (n + 1) / (1 - hi / (n + 2)) + if tail < Q(1, 1 << (bits + 16)): + return 1 / (total_hi + tail), 1 / total_lo + raise ValueError("bounded independent direct Taylor series") diff --git a/research/production-reference-gap/source.py b/research/production-reference-gap/source.py new file mode 100644 index 0000000000..35f3cc3383 --- /dev/null +++ b/research/production-reference-gap/source.py @@ -0,0 +1,52 @@ +"""Exact canonical Reference/for_cap cohort, with no projected source bodies. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +from contextlib import contextmanager +from hashlib import sha1, sha256 +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((HERE / "SOURCES.json").read_text())["files"] + for row in rows: + path = ROOT / row["path"] + need(path.is_file() and not path.is_symlink(), "regular canonical source input") + raw = path.read_bytes() + need(sha256(raw).hexdigest() == row["sha256"] and + sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() == row["git_blob"], + "unchanged production-gap source: " + row["path"]) + return len(rows) + + +@contextmanager +def opened(): + authenticate() + names = ("exact", "engine", "triangular", "generator", "full", "gaussian", "gaussian_reference") + need(not any(name in sys.modules for name in names), "cold actual Gaussian source cohort") + modules = {} + try: + for name in names: + spec = importlib.util.spec_from_file_location(name, + ROOT / "research/rational-unitary-fft" / (name + ".py")) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = modules[name] = module + spec.loader.exec_module(module) + raw = {path: (ROOT / path).read_bytes() for path in + (modules["gaussian"].INTERVALS, modules["gaussian"].EVALUATOR)} + yield modules["gaussian_reference"], raw + finally: + for name, module in modules.items(): + if sys.modules.get(name) is module: + del sys.modules[name] diff --git a/research/production-reference-gap/verify.py b/research/production-reference-gap/verify.py new file mode 100644 index 0000000000..5f53b6de71 --- /dev/null +++ b/research/production-reference-gap/verify.py @@ -0,0 +1,133 @@ +#!/usr/bin/env python3 +"""Actual for_cap admission, independent transcendentals, and scope controls. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +""" +import argparse +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from source import authenticate, opened, need +from independent import actual_alpha, ceil_log2, decay_box + + +def reject(function, text): + try: + function() + except ValueError as error: + need(text in str(error), "expected rejection: " + text) + return 1 + raise ValueError("negative control accepted: " + text) + + +def cap_for(p): + k = 0 + while 1 << (16 * (k + 1)) <= p ** 15: + k += 1 + return 1 << k + + +def fixture(source, raw, p, near_upper, cap, radius, target): + N = 1 << max(12, ceil_log2(32 * p * p)) + if near_upper: + e = N // (p * p + 1) + else: + e = -(-N // (4 * p * p + 1)) + S, alpha = N - e, actual_alpha(p) + theta = Q(e, S) + need(Q(1, 4 * p * p) <= theta <= Q(1, p * p), "actual original fine-prime relative-padding domain") + ref = source.Reference.for_cap(raw, S, e, alpha, cap, radius, target) + allocation = ref.allocation + E, b_e = allocation["error_bits"], ref.spec.entry_bits + G, H, Qstar = (Q(allocation[name]) for name in ("gauge_bound", "normalized_bound", "inverse_bound")) + qbar = H / 2 + need(G >= (1 << 8) * alpha and qbar >= 16 * p * cap, + "actual previous normalized conditioning allocation funds the narrow gap") + need(Qstar == G * G * H and Qstar >= (1 << 21) * alpha * alpha * p * cap, + "literal complete source inverse bound") + need(E == target + ceil_log2(8 * (radius + 1) * Qstar * Qstar) + and E >= target + 46 + ceil_log2(p * p), "unchanged source e has the derived minimum") + need(ref.errors["narrow"] <= Q(1, 1 << E) and b_e >= E + 3, + "actual complete narrow tail/entry allowance") + J = 2 * (b_e + (-(-(8 * alpha * alpha * ref.rho * ref.rho).numerator // + (8 * alpha * alpha * ref.rho * ref.rho).denominator)) + 16) + 32 + width = Q(512 * J * J, 1 << J) + need(J >= 2 * b_e + 64 and width <= Q(1, 1 << b_e), "literal outward interval width budget") + a, b = decay_box(2 * alpha * alpha * theta), decay_box(2 * alpha * alpha) + ideal_lo, ideal_hi = 1 - a[1] - 5 * b[1], 1 - a[0] - 5 * b[0] + need(ideal_lo >= Q(1, 8 * p * p), "independent actual ideal row-majorant gap") + need(ideal_lo - 6 * width <= ref.narrow_gap + ref.errors["narrow"] <= ideal_hi, + "independent direct-series bound agrees with literal certified gap") + strong = (Q(1, 8) - Q(1, 1 << 46)) / (p * p) + need(ref.narrow_gap >= strong > Q(1, 16 * p * p), "actual for_cap certificate clears the production gap") + need(ref.narrow_inverse_bounds is not None and ref._holes is None and + not ref.weights and not ref.kernel and not ref.entries, + "conditioning returned without enumerating the full axis or preparing weight pages") + return dict(p=p,source_size=S,excess=e,target_size=N,theta=str(theta),alpha=alpha,cap=cap, + radius=str(radius),target=target,error_bits=E,entry_bits=b_e,working_bits=J, + source_halfwidth=ref.spec.source_halfwidth,target_halfwidth=ref.spec.target_halfwidth, + weight_precision=ref.weight_precision, gap_scaled_lower_pass=True, + gap_sha256=sha256(str(ref.narrow_gap).encode()).hexdigest(), + allocation_sha256=sha256(json.dumps(allocation,sort_keys=True).encode()).hexdigest()) + + +def run(): + inputs = authenticate() + rows = [] + with opened() as (source, raw): + for p in (2, 3, 7, 19, 73, 74, 257, 1024, 65536): + for high in (False, True): + for cap in sorted({1, cap_for(p)}): + rows.append(fixture(source, raw, p, high, cap, Q(1), 1)) + for p, radius, target in ((2, Q(3, 2), 17), (19, Q(1 << 16), 38), (74, Q(3), 74)): + rows.append(fixture(source, raw, p, False, cap_for(p), radius, target)) + controls = 0 + # The theorem is about for_cap's actual allocation, not every Reference. + p, N = 257, 1 << 22 + e = -(-N // (4 * p * p + 1)) + direct = source.Reference(raw, N - e, e, actual_alpha(p), 4, 20, 8) + need(direct.narrow_gap < 0, "underfunded arbitrary Reference negative control") + controls += 1 + # for_cap alone does not supply the source alpha/theta inequalities. + bad_alpha = source.Reference.for_cap(raw, 4093, 3, 1, 1, 1, 1) + need(bad_alpha.narrow_gap < 0, "underfunded source alpha negative control") + controls += 1 + bad_theta = source.Reference.for_cap(raw, (1 << 100) - 1, 1, 3, 1, 1, 1) + need(bad_theta.narrow_gap < 0, "missing theta lower bound negative control") + controls += 1 + controls += reject(lambda: source.Reference.for_cap(raw, 7, 1, 3, 4, 1, 1), "uniform reference cap") + controls += reject(lambda: source.Reference.for_cap(raw, 7, 1, 3, 1, 1, 1000), "unique retained periodic lifts") + controls += reject(lambda: source.Reference.for_cap(raw, 4093, 3, 3, 1, Q(1, 2), 1), "uniform reference radius") + # Independent integer checks of the two induction bases/steps in the proof. + for b_e in range(8, 513): + J = 2 * b_e + 64 + need(512 * J * J <= 1 << (b_e + 64), "interval budget induction instances") + need((J + 2) ** 2 < 2 * J * J, "interval budget induction step") + need((Q(1, 8) - Q(1, 1 << 46)) > Q(1, 16), "strict uniform production threshold") + need(192 ** 16 < 1 << 200, "explicit sufficient cap-allocation onset") + return dict(status="PASS_PRODUCTION_REFERENCE_GAP",source_inputs=inputs,actual_for_cap_cases=len(rows), + independent_interval_budget_cases=505,negative_controls=controls,fixtures=rows, + scope='Actual canonical for_cap constructor and literal gap certificate; no physical/native or complete Gaussian replay.') + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--output") + args = parser.parse_args() + result = run() + encoded = json.dumps(result,indent=2,sort_keys=True)+"\n" + if args.output: + Path(args.output).write_text(encoded) + else: + need(json.loads(encoded) == json.loads((HERE / "evidence/REPLAY.json").read_text()), + "complete frozen production-reference-gap receipt") + print(json.dumps({k:v for k,v in result.items() if k!='fixtures'},sort_keys=True)) + + +if __name__ == "__main__": + main()