diff --git a/research/dyadic-full-cell-gaussian/PROOF.md b/research/dyadic-full-cell-gaussian/PROOF.md new file mode 100644 index 0000000000..18e47dcb3d --- /dev/null +++ b/research/dyadic-full-cell-gaussian/PROOF.md @@ -0,0 +1,276 @@ +# Effective preparation of the full Gaussian cell + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The exact source and q-LDU identities are retained from JoyboyBrian's PR5479 +and its Gaussian predecessors. This is a written proof with exact finite +corroboration. It is not independent human or formal proof-kernel acceptance. + +## Source and result + +Let p be an integer at least 16. Use the actual source parameters + +``` +alpha = ceil(sqrt((4/pi) log(16p))), +1/(4p^2) <= theta <= 1/p^2, rho = 1+theta, +N = floor(1/theta), b = pi/alpha^2, +K[k,i] = alpha^(-1) exp(-b(i-(k+1/2)/rho)^2), 0 <= i,k < N. +``` + +The preparation algorithm takes the source integer alpha and rational theta +as inputs. Source-prime selection and the computation of alpha remain upstream +work. Their cost is not set to zero. Write +`mu(M)=max(||M||_1,||M||_infinity)`. This norm is submultiplicative and bounds +the operator 2-norm. + +The following finite bound holds for every stated p and theta: + +``` +mu(K^(-1)) <= B = 5 p^6. +``` + +For every integer t>=0, the supplied algorithm constructs one banded dyadic +matrix A and one dense dyadic matrix R with + +``` +mu(A-K) <= delta, +mu(R-K^(-1)) <= 2^(-t), mu(R) <= 2B. +``` + +It gives exact interval and integer-residual certificates. Its preparation +cost is polynomial in N, t, log(p) and the bit length of theta. All matrices, +intermediate rational numbers and numerical proposals are charged below. +No physical native call or selected-kappa improvement is inferred. + +PR5479's eventual p^(2+eta) bound is asymptotically sharper. The new guard is +explicit from p=16 and is sufficient for certified reference preparation. +It is not a stronger asymptotic inverse theorem. + +## A finite inverse guard + +The retained source identity sets gamma=b/rho and +`P(gamma)=product_(r>=1)(1-exp(-2 gamma r))`. Every checkerboard inverse entry +has the form `alpha exp(E_ij) F_ij`, where + +``` +0 <= F_ij <= P(gamma)^(-3), +E_ij <= b/4 - gamma theta (i-j)^2. +``` + +For i<=j the last inequality uses j^2-i^2 >= (j-i)^2. For i>j, reflect both +indices as in PR5479. Its offset delta is in [1,2); the extra cross term has +the favorable sign. Thus the same inequality holds. These are exact finite +identities; no limit or finite-product replacement is used. + +For a>0, monotonicity of exp(-a x^2) gives +`sum_(d in Z) exp(-a d^2) <= 1+sqrt(pi/a)`. Apply this to each row and column +of the absolute inverse. The result is + +``` +mu(K^(-1)) <= alpha exp(b/4) P(gamma)^(-3) + (1+alpha sqrt(rho/theta)). (1) +``` + +The source's decreasing-integrand argument gives +`P(gamma)^(-3) <= exp(pi^2/(4 gamma)) = exp(pi alpha^2 rho/4)`. +We now make all remaining constants effective. + +Put u=log(p). For p>=16, `8/3 < log(16) <= u` and `log(16p)<=2u`. +The source ceiling gives +`alpha < sqrt(8u/pi)+1`. It follows that alpha<=sqrt(p): at p=16, +`sqrt(8 log(16)/3)+1 < sqrt(8)+1 < 4`; the difference +`exp(u/2)-sqrt(8u/3)-1` is increasing for u>=log(16), because its derivative +is at least `2-1/2`. Also alpha>=3, b<1 and rho<=257/256. +Using `3= 1-sum(u_j)` then gives a positive lower bound for the +entire infinite product. This charges the tail, rather than replacing the +infinite product by its partial product. + +A lower bound for exp(-b/4) bounds exp(b/4) from above. An integer square-root +calculation gives a rational upper bound for sqrt(rho/theta), with denominator +2^32. Substitution in (1), followed by an integer ceiling, gives B_q. Use +`B=min(5p^6,B_q)` for every subsequent bit and band choice. Both inputs to +this minimum are proved upper bounds. The product interval uses +`64+16 bit_length(p)` working bits. In the production regime gamma is +Theta(1/log p), so the required term count and interval work are polynomial +in log p. The source's product lower bound and these guard bits keep the +rounded product positive. For an explicit termination bound, alpha^2<=p and +rho<=257/256 give 1-q>3/p. The interval and grid errors are at most three +units in the working grid, so the upper ratio has gap at least 1/p. Within +4p^2 steps its geometric tail, including rounded-power error, is below +2^(-32). The cumulative product error is at most +`20 p^4 2^(-work) < p^(-4/3)/2`; the source product bound gives +`P(gamma)>=p^(-4/3)`. Thus the product stays positive for every p>=16. +These conservative bounds suffice even without the sharper logarithmic +production estimates. This reduces the large excess in the uniform +polynomial guard without a numerical norm estimate. + +## Bandwidth and entry rounding + +Let G=ceil(log2 B), Q=t+2G+4 and choose the least integer w with + +``` +w >= alpha, 30 w^2 >= 7 alpha^2 (Q+3). +``` + +Set m=min(N,2w+1), L=Q+ceil(log2 m)+2 and U=t+G+ceil(log2 N)+4. +Keep entries with |i-k|<=w and round each to a multiple of 2^(-L), with a +certified entry error at most 2^(-L). Set the other entries to zero. + +The source displacement from the diagonal is +`(k theta-1/2)/rho`, whose absolute value is at most 1/2 because k=w+1) exp(-b(d-1/2)^2) + <= (2/alpha + alpha/(pi(w+1/2))) exp(-b(w+1/2)^2) + < exp(-b w^2) <= 2^(-(Q+3)). (2) +``` + +The first inequality uses the first term and the Gaussian tail integral. +The strict coefficient bound uses alpha>=3, w>=alpha and pi>3. +The last step uses pi>3 and log(2)<7/10. It remains valid when the band +covers the whole cell, since then the omitted sum is zero. +There are at most m rounded entries per row and column. Consequently + +``` +delta = m 2^(-L) + 2^(-(Q+3)) <= (3/8) 2^(-Q). (3) +``` + +In particular B delta<1/8, so A is invertible and +`mu(A^(-1)) <= B/(1-B delta) < 2B`. A shifted Gaussian sum is at most its +maximum plus its integral. It gives +`mu(K) <= 1/alpha+rho < 3/2`; hence `mu(A)<2`. + +The width is `O(sqrt((t+log p) log p))`. It becomes +`O(sqrt(p log p))` when t=O(p), as in the source's common-reference accuracy +regime. No capped RawGaussian API admission follows from that order bound. + +## Exact coefficient intervals + +The code encloses pi with Machin's identity and alternating rational sums. +The identity follows from +`tan(4 atan(1/5))=120/119` and +`(120/119-1/239)/(1+120/(119*239))=1`, with the angle in (0,pi/2). +Each alternating remainder lies between its partial sum and the sum with +the next term. Outward dyadic rounding retains this enclosure. + +To enclose exp(-x), x>=0, divide x by 2^k until z<=1. Compute the positive +Taylor sum for exp(z) on an outward-rounded integer grid. If the last term +is T_n, the omitted tail is at most `3 T_n z/(n+1)`: after the next term, +the ratios are at most 1/(n+2). Invert the positive interval, then square +it k times with outward rounding. The code checks the final width and +increases the working grid if needed. Each step encloses the exact value. +The Taylor remainder decreases factorially. The cumulative rounding width +is `O(2^k n/2^work)`, so work polynomial in the requested bits and k suffices. +All divisions use integer floor or ceiling, not a floating-point error model. + +For retained entries, x=pi z with rational z. Evaluate the two pi endpoints +and use monotonicity. The derivative bound +`z exp(-pi_low z) <= 1/(e pi_low) < 1` controls pi uncertainty uniformly in z. +The chosen pi and exponential guard bits make the resulting entry interval +narrower than half an output grid step. Rounding its midpoint to the nearest +grid value therefore has error below one step. The code checks that both +interval endpoints lie within the claimed step for every retained entry. + +## Inverse preparation and the decisive certificate + +First compute a 60-digit Decimal elimination proposal, with row pivoting. +Round its entries to multiples of 2^(-U). This proposal is untrusted. +The verifier multiplies integer numerators to compute every entry of AR-I, +and computes the exact absolute row and column sums. Accept only if + +``` +epsilon = mu(AR-I) <= 2^(-(t+G+3)), +mu(R) <= 2B, +B (delta mu(R)+epsilon) <= 2^(-t). (4) +``` + +If the proposal or its certificate fails, use exact rational elimination +with row pivoting and round the exact inverse to the same grid. This is a +complete algebraic algorithm, not a numerical assumption. All intermediate +fractions are computed and charged. Invertibility guarantees a nonzero pivot +at each column after row exchanges. + +The exact path always passes. Its rounding error has mu-norm at most +`N 2^(-U)/2 <= 2^(-(t+G+5))`. Since mu(A)<2, its residual is strictly below +the first bound in (4). The inverse-norm guard follows from (3), and the +last error bound has strict slack. In particular (3) and the first two +bounds in (4) imply an error at most `(11/64)2^(-t)`. + +For every accepted proposal, independently of how it was obtained, + +``` +K^(-1)-R = K^(-1) ((I-AR)+(A-K)R). +``` + +This exact identity proves (4)'s error bound and retains the multiplication +order. The error bound holds for every input vector, not only +for a sampled payload. It also bounds the operator 2-norm. + +## Preparation resources and exact scope + +Let H be the binary length of the rational theta descriptor. Formation uses +`O(N min(N,w))` certified exponential entries, with polynomial work in +H, t and log(p) per entry. The executable currently stores the forward +matrix densely, including its zero entries. It also stores the dense inverse. +No sparse-memory saving is claimed for that implementation. + +For the exact completion path, integer forward coefficients have O(L) bits. +Every reduced elimination fraction is a ratio of minors. The determinant +bound gives `O(N(L+log N))` bits per numerator and denominator. Thus exact +preparation uses O(N^3) rational operations on numbers of that size and +`O(N^3(L+log N))` working bits. With school arithmetic this gives +`O(N^5(L+log N)^2)` bit work, up to the usual integer-arithmetic logarithmic +factors. The fixed-precision proposal adds O(N^3) Decimal operations before +that worst-case cost. The final arrays use `O(N^2(t+log p))` bits, plus +dimensions and the source descriptor. All these are positive costs. + +This constructs a common numerical reference and its inverse table. It does +not place them in a native supplier, emit a reversible dirty circuit, pay a +whole multiplication caller, or establish page delivery, tape movement, +stock reuse, preparation amortization or outer recovery. A physical consumer +must use this same reference and charge those operations. The source's +p^10 analytic inverse allowance is compatible with the finite guard, but +its complete API is not admitted here. No new kappa is claimed. + +## Verification boundary + +The verifier rebuilds complete 256-column and 299-column cells. The latter +uses p=17, alpha=3, theta=601/599-1, with literal prime checks, and retains +N=floor(599/2)=299. It certifies two requested accuracies on that geometry. +All retained coefficients have exact intervals and all inverse-residual +entries are computed with integers. An independent rational Taylor sum +checks the exponential enclosure on a bounded set of arguments. Exact +inverse completion is checked on separate small matrices with a row exchange. +The large cells use certified Decimal proposals; a large exact-completion +run is not claimed. Mutants reject an altered inverse, omitted forward +coefficient, incomplete cell, wrong parameter domain and failed guard. diff --git a/research/dyadic-full-cell-gaussian/README.md b/research/dyadic-full-cell-gaussian/README.md new file mode 100644 index 0000000000..1c251bcc6c --- /dev/null +++ b/research/dyadic-full-cell-gaussian/README.md @@ -0,0 +1,92 @@ +# A certified dyadic full-cell Gaussian reference and inverse + +The exact broad Gaussian cell now has an explicit inverse guard from p=16 +and a complete numerical preparation algorithm. It constructs one banded +dyadic reference A and a dyadic inverse R with certified error at most +2^(-t), for every requested t>=0. Both the maximum absolute row sum and +column sum are controlled. No new kappa is claimed. + +The uniform guard is `5p^6`. A finite q-product enclosure gives a much tighter +guard for actual preparation, with its infinite tail charged. The algorithm +checks every retained Gaussian coefficient by rational intervals and every +inverse residual entry by integer arithmetic. A Decimal proposal is accepted +only after these exact checks. Exact rational elimination completes the +algorithm if that proposal fails. + +[PROOF.md](PROOF.md) gives the full quantifiers, finite constants, error ledger +and preparation costs. [prepare.py](prepare.py) implements the construction. +[RESULT.json](RESULT.json) records complete 256- and 299-column cell checks. +[SOURCES.json](SOURCES.json) retains the exact analytic sources. + +## Scope and connection to the source + +The source is the full cell `N=floor(1/theta)`, with +`alpha=ceil(sqrt((4/pi)log(16p)))` and +`1/(4p^2)<=theta<=1/p^2`. Its half-grid phase and dilation are unchanged. +The algorithm receives the source alpha and rational theta; source-prime +selection and parameter setup remain upstream work. It checks sufficient +conditioning guards and does not silently alter those parameters. + +JoyboyBrian's PR5479 proves sharper eventual conditioning but leaves a +rounded reference and its preparation open. This package closes that +numerical implication with finite constants. It does not install the table +in a native supplier, admit a capped RawGaussian API, or price a physical +caller. Coefficient storage, exact elimination, and numerical proposal work +are explicit costs. Page delivery, tape movement, stock reuse, preparation +amortization, online reversible execution and outer recovery remain open. +The main transform still limits the selected conditional kappa 0.00310045. + +## Verification + +Python 3.12 and the standard library suffice. + +``` +python3.12 -B scripts/research_package.py --package research/dyadic-full-cell-gaussian +python3.12 -B scripts/check_research_commit.py --package research/dyadic-full-cell-gaussian +``` + +Expected: `PASS_DYADIC_FULL_CELL_GAUSSIAN`, +`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. +Both normal and optimized modes rebuild the complete cells. The 299-column +case uses the primes p=17, s=599 and t=601, with theta=t/s-1; this t is the +source-prime name, not the requested accuracy. Its floor remains 299. +Requested accuracy bits are 4 on the 256-column case and 12 and 40 on the +299-column case. The literal source ceiling is checked separately. + +The checks include independent rational exponential enclosures, exact +integer residuals, all input columns, three small exact inverse cases with +row pivoting, and mutants for wrong coefficients, inverse entries, cell +size, domain and conditioning. Retained sources are authenticated first. +The fixed result is mandatory and never rewritten by verification. + +The large cells use certified Decimal proposals. A large exact rational +completion run is not claimed. The universal theorem is the written proof, +not an inference from these cells. The same assistant wrote the proof and +checker; there is no independent human or formal proof-kernel review. +No native or selected cold replay, whole outer admission, full historical +suite, Lean or Docker run was used. Full-history preflight is unavailable +in this shallow checkout. + +## Open next questions + +1. Which actual full-cell consumer can use this exact common reference + while paying its complete page, route, precision, stock and outer bill? + A numerical inverse table does not provide that physical implementation. +2. Can a structured inverse application reduce the dense table and exact + completion costs without weakening the same residual certificate? + The current implementation stores dense arrays and prices them as such. + +## Credit + +JoyboyBrian's [PR5479](https://github.com/CrocSwap/integer-mult-bounds/pull/5479) +supplies the production full-cell source and uniform q-product estimates. +The retained half-line and Gaussian source notes preserve Jose Manuel, +Vlado Vojdanovski, Cinna Davis, Ryanson Jonathan, Nick Petalas and the +classical q-LDU/product lineage. The earlier eventual bound is not new here. +New effective guard, certified dyadic preparation, exact residual check, +proof and implementation: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. + +Base: canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority 7. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19188471). +No selected-frontier file is changed. diff --git a/research/dyadic-full-cell-gaussian/RESULT.json b/research/dyadic-full-cell-gaussian/RESULT.json new file mode 100644 index 0000000000..f637feb7e6 --- /dev/null +++ b/research/dyadic-full-cell-gaussian/RESULT.json @@ -0,0 +1,107 @@ +{ + "cells": [ + { + "accuracy_bits": 4, + "certificate": { + "inverse_error": "193941296949026675/295147905179352825856", + "inverse_norm": "10673470919/4194304", + "reference_error": "35/2199023255552", + "residual": "35310141767097/590295810358705651712" + }, + "inverse_sha256": "15fd13726b472ffbd4e6295adfa2ae3fd885d39c9c3261ebf6ee325d6d3ff9c9", + "method": "certified Decimal proposal", + "parameters": { + "B": 6550, + "G": 13, + "N": 256, + "Q": 34, + "W": 9, + "alpha": 3, + "entry_bits": 41, + "formed_entries": 4774, + "inverse_bits": 29, + "inverse_guard": { + "finite_product_terms": 32, + "interval_bits": 144, + "product_lower": "4526305653571755351059794140025847143915266692397240278457286173244082272621330522581/15576559826111346428442598571857963538100051218594157025384345782806124327503692562432", + "q_product_bound": 6550, + "uniform_bound": 83886080 + }, + "p": 16, + "theta": "1/256" + }, + "reference_sha256": "5b1c4c2436a629e4d74ef9dbb50ae47dcfa3f6ba5eaad1e6b0b595f684caed94" + }, + { + "accuracy_bits": 12, + "certificate": { + "inverse_error": "176672070122923951863/77371252455336267181195264", + "inverse_norm": "191118796668471/68719476736", + "reference_error": "37/562949953421312", + "residual": "10920632244564633/77371252455336267181195264" + }, + "inverse_sha256": "0881bb65120810c3c1c51d98a492352f0d94e43054140d76af891c7f9d2e35d2", + "method": "certified Decimal proposal", + "parameters": { + "B": 7049, + "G": 13, + "N": 299, + "Q": 42, + "W": 10, + "alpha": 3, + "entry_bits": 49, + "formed_entries": 6169, + "inverse_bits": 38, + "inverse_guard": { + "finite_product_terms": 32, + "interval_bits": 144, + "product_lower": "18131708633312277877664716741222981121517424841118274174640338007085864490962728462411/62330624564441952344499551777868466211389955333066518894158273840030897753204803502080", + "q_product_bound": 7049, + "uniform_bound": 120687845 + }, + "p": 17, + "theta": "2/599" + }, + "reference_sha256": "eac13d6deaae5c6fdc4d646e1089e57f8f232e94a8dafc3e04dc59a046a9908d" + }, + { + "accuracy_bits": 40, + "certificate": { + "inverse_error": "13296713070570400726146402679/1393796574908163946345982392040522594123776", + "inverse_norm": "205212245335355388794247/73786976294838206464", + "reference_error": "43/151115727451828646838272", + "residual": "6266482695091451266550347/11150372599265311570767859136324180752990208" + }, + "inverse_sha256": "72d5d5529181d5786c01a60d7c20d17370b4e59a6d7b93bf8adbf69d4e3c9603", + "method": "certified Decimal proposal", + "parameters": { + "B": 7049, + "G": 13, + "N": 299, + "Q": 70, + "W": 13, + "alpha": 3, + "entry_bits": 77, + "formed_entries": 7891, + "inverse_bits": 66, + "inverse_guard": { + "finite_product_terms": 32, + "interval_bits": 144, + "product_lower": "18131708633312277877664716741222981121517424841118274174640338007085864490962728462411/62330624564441952344499551777868466211389955333066518894158273840030897753204803502080", + "q_product_bound": 7049, + "uniform_bound": 120687845 + }, + "p": 17, + "theta": "2/599" + }, + "reference_sha256": "c84f11b176dbb275679c5985e656e370bfcecad32575312d74ad7b2bc2547505" + } + ], + "exact_enclosure_and_geometry_checks": 33, + "exact_inverse_checks": 3, + "inverse_guard": "5*p^6", + "production_threshold": 16, + "rejecting_controls": 14, + "scope": "Certified reference and inverse preparation; no physical caller or new kappa.", + "status": "PASS_DYADIC_FULL_CELL_GAUSSIAN" +} diff --git a/research/dyadic-full-cell-gaussian/SOURCES.json b/research/dyadic-full-cell-gaussian/SOURCES.json new file mode 100644 index 0000000000..6018d4cb2d --- /dev/null +++ b/research/dyadic-full-cell-gaussian/SOURCES.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "research/dyadic-full-cell-gaussian/vendor/PR5479.md", + "usage": "input", + "git_blob": "90262d4a23471882bef976610b44beb777684dab", + "sha256": "df5707688aa2b046ca3e910f864b502e70a151fa7ef19c4cd6f7b34a66d856aa", + "pin": "head:a33104e680c0c0e75ff601636b38efa2fccf2475:research/dyadic-full-cell-gaussian/vendor/PR5479.md" + }, + { + "path": "research/dyadic-full-cell-gaussian/vendor/HALF-LINE.md", + "usage": "input", + "git_blob": "794842c1155fe826742a98e6107256b040a39b9d", + "sha256": "2bf0e36ecd0c3647888e78bc0b8ae30614f5daf07511a4424d69cb3efc29c904", + "pin": "head:a33104e680c0c0e75ff601636b38efa2fccf2475:research/dyadic-full-cell-gaussian/vendor/HALF-LINE.md" + }, + { + "path": "research/dyadic-full-cell-gaussian/vendor/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242", + "pin": "head:a33104e680c0c0e75ff601636b38efa2fccf2475:research/dyadic-full-cell-gaussian/vendor/GAUSSIAN.md" + } + ], + "external_inputs": [ + { + "local_path": "vendor/PR5479.md", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "source_path": "research/production-gaussian-boundary-limit/PROOF.md", + "sha256": "df5707688aa2b046ca3e910f864b502e70a151fa7ef19c4cd6f7b34a66d856aa" + }, + { + "local_path": "vendor/HALF-LINE.md", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "source_path": "research/gaussian-half-line-operator-limit/PROOF.md", + "sha256": "2bf0e36ecd0c3647888e78bc0b8ae30614f5daf07511a4424d69cb3efc29c904" + }, + { + "local_path": "vendor/GAUSSIAN.md", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "source_path": "research/unconditional-batched-crt/GAUSSIAN.md", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + } + ] +} diff --git a/research/dyadic-full-cell-gaussian/TASK.json b/research/dyadic-full-cell-gaussian/TASK.json new file mode 100644 index 0000000000..91883823b2 --- /dev/null +++ b/research/dyadic-full-cell-gaussian/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove an effective full-cell Gaussian inverse guard and construct a certified dyadic reference and inverse at arbitrary requested accuracy.", + "scope_change_reason": "Take the released rounded-reference implication from PR5479. Keep physical caller admission and active BIT/P104 late-binding work outside scope.", + "bottleneck_link": "Replace an unspecified common-reference perturbation and inverse-preparation premise with a constructive numerical contract and positive resource bounds.", + "budget_minutes": 150, + "stop_rule": "Complete this numerical preparation implication and exact certificates. Do not infer physical supplier admission or a new kappa.", + "outcome": "completed", + "evidence": "PROOF.md, prepare.py, verify.py and RESULT.json.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. The same assistant wrote the proof and checker; no independent human review.", + "open_questions": [ + { + "question": "Can an actual full-cell consumer admit this same reference?", + "why_it_matters": "Numerical preparation does not pay physical native and outer execution.", + "first_step": "Bind the exact table and all page, route, stock and precision costs at one caller.", + "blocked_by": "No physical consumer is supplied." + }, + { + "question": "Can structured inverse application replace dense preparation?", + "why_it_matters": "The present exact completion and dense table have explicit polynomial costs.", + "first_step": "Retain the exact residual contract while deriving and pricing a structured algorithm.", + "blocked_by": "No fast structured inverse implementation is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4202#discussioncomment-19188471", + "nonce": "77c89ad746e961fdc71037cd00717d21", + "upstream": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "priority_revision": 7, + "overlap_utc": "2026-10-26T04:52:55.590693+00:00", + "local_notes": 7676, + "open_prs": 363, + "discussion_records": 4990, + "coverage": "All tracked main notes and complete cached PR/Discussion pagination; no unpublished-work coverage." + } +} diff --git a/research/dyadic-full-cell-gaussian/VALIDATION.md b/research/dyadic-full-cell-gaussian/VALIDATION.md new file mode 100644 index 0000000000..ce51bdb2b8 --- /dev/null +++ b/research/dyadic-full-cell-gaussian/VALIDATION.md @@ -0,0 +1,33 @@ +# Validation record + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +Scientific commit: `7de506ab616688dfd5131de2b4b38edb359e6693`. +Registered CPython 3.12.14 normal and optimized checks pass. Both reconstruct +all three cells and match the same fixed receipt. The complete 256-column +cell uses 4 accuracy bits. The complete 299-column prime-ratio cell uses 12 +and 40 bits. Every retained entry is enclosed and every inverse-residual +entry is checked with integers. The exact completion code passes three +separate small matrix checks. Fourteen invalid cases are rejected. + +The eleven package files pass committed-byte and official export checks. +The optimized Git-free export passes with empty PATH and read-only source +files. All twelve exported files, including the export manifest, keep their +hashes. A separate copy with an appended line in the retained PR5479 proof +fails with `retained source changed` before preparation. The base and +retention commit are immediate ancestors. Full-history preflight is not +available in this shallow checkout. + +The publication update adds this record and final coordination counts. It +changes no scientific code, source or receipt. Its committed bytes and +export integrity are checked separately. Current main remains +df0137efd35e11b4445734bf612bdd4c7ebc330c, with no priority, guidance or selected +record drift. The final cache has 363 open PRs and 4990 Discussion records. +All tracked main notes were searched. Only the predecessor and this claim +match the precise full-cell reference scope. Unpublished work and arbitrary +PR diff contents are outside this coverage. + +Large exact rational completion, physical native or selected cold replay, +page and tape implementation, stock reuse, outer admission, the full +historical suite, Lean, Docker and independent human review were not run. +The large cells use certified Decimal proposals. CI is not asserted here. diff --git a/research/dyadic-full-cell-gaussian/VERIFY.json b/research/dyadic-full-cell-gaussian/VERIFY.json new file mode 100644 index 0000000000..6816bfd8f8 --- /dev/null +++ b/research/dyadic-full-cell-gaussian/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dyadic-full-cell-gaussian/vendor/PR5479.md", + "research/dyadic-full-cell-gaussian/vendor/HALF-LINE.md", + "research/dyadic-full-cell-gaussian/vendor/GAUSSIAN.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Rebuild complete source cells and certify all Gaussian entry intervals, integer inverse residuals, exact completion examples and rejecting controls." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Rebuild complete source cells and certify all Gaussian entry intervals, integer inverse residuals, exact completion examples and rejecting controls." + } + ] +} diff --git a/research/dyadic-full-cell-gaussian/prepare.py b/research/dyadic-full-cell-gaussian/prepare.py new file mode 100644 index 0000000000..54a1364ef4 --- /dev/null +++ b/research/dyadic-full-cell-gaussian/prepare.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Certified full-cell preparation. Ali Romman with OpenAI Codex. Apache-2.0.""" +from fractions import Fraction as F +from decimal import Decimal, localcontext, ROUND_HALF_EVEN +from math import isqrt +from functools import lru_cache +import json +from hashlib import sha256 + +def need(ok, msg): + if not ok: + raise ValueError(msg) + +def ceilq(x): + return -(-x.numerator // x.denominator) + +def quant(x, b, upper=False): + s = 1 << b + return F(ceilq(x * s) if upper else x.numerator * s // x.denominator, s) + +@lru_cache(None) +def pi_bounds(bits): + + def atan(q): + n = bits + 8 + total = sum((F((-1) ** k, (2 * k + 1) * q ** (2 * k + 1)) for k in range(n)), F()) + nxt = F((-1) ** n, (2 * n + 1) * q ** (2 * n + 1)) + return (min(total, total + nxt), max(total, total + nxt)) + a, b = atan(5) + c, d = atan(239) + return (quant(16 * a - 4 * d, bits), quant(16 * b - 4 * c, bits, True)) + +def expneg(x, bits): + x = F(x) + need(type(bits) is int and bits >= 0 and (x >= 0), 'nonnegative exponent and precision') + k = 0 + while x > 1: + x /= 2 + k += 1 + work = bits + 2 * k + 2 * (bits + 2 * k + 20).bit_length() + 16 + while True: + scale = 1 << work + xl = x.numerator * scale // x.denominator + xu = ceilq(x * scale) + low = high = sl = su = scale + n = work + 8 + for j in range(1, n + 1): + low = low * xl // (scale * j) + high = -(-high * xu // (scale * j)) + sl += low + su += high + tail = -(-3 * high * xu // (scale * (n + 1))) + low = scale * scale // (su + tail) + high = -(-scale * scale // sl) + for _ in range(k): + low = low * low // scale + high = -(-high * high // scale) + if high - low <= 1 << work - bits: + return (F(low, scale), F(high, scale)) + work *= 2 + +@lru_cache(None) +def inverse_guard(p, alpha, theta): + """Bound both absolute inverse norms by a finite q-product interval.""" + rho = 1 + theta + need(alpha * alpha <= p, 'polynomial alpha guard') + bits = 64 + 16*p.bit_length() + plo, phi = pi_bounds(bits) + lower, _ = expneg(phi*alpha*alpha*rho/4, bits) + need(lower >= F(1, p**4), 'finite product guard') + _, upper_q = expneg(2*plo/(alpha*alpha*rho), bits) + scale = 1 << bits + q = ceilq(upper_q*scale) + need(0 < q < scale, 'strict q-product ratio') + power, product, terms = q, scale, 0 + while True: + terms += 1 + product = product*(scale-power)//scale + following = -(-power*q//scale) + tail = F(following, scale-q) + if tail <= F(1, 1 << 32): + break + power = following + product_lower = F(product, scale)*(1-tail) + need(product_lower > 0, 'positive product lower bound') + exponential_lower, _ = expneg(phi/(4*alpha*alpha), bits) + square_scale = 1 << 64 + root_integer = isqrt(ceilq(rho/theta*square_scale)) + while root_integer*root_integer < rho/theta*square_scale: + root_integer += 1 + root = F(root_integer, 1 << 32) + sharpened = ceilq(alpha*(1+alpha*root)/(exponential_lower*product_lower**3)) + bound = min(5*p**6, sharpened) + return bound, dict(uniform_bound=5*p**6, q_product_bound=sharpened, + finite_product_terms=terms, product_lower=str(product_lower), + interval_bits=bits) + +def parameters(p, alpha, theta, t): + need(type(p) is int and type(alpha) is int and (type(t) is int) and isinstance(theta, F) and (p >= 16) and (alpha >= 3) and (F(1, 4 * p * p) <= theta <= F(1, p * p)) and (t >= 0), 'production domain') + n = theta.denominator // theta.numerator + B, _ = inverse_guard(p, alpha, theta) + g = (B - 1).bit_length() + q = t + 2 * g + 4 + w = max(alpha, isqrt((7 * alpha * alpha * (q + 3) + 29) // 30)) + while 30 * w * w < 7 * alpha * alpha * (q + 3): + w += 1 + width = min(n, 2 * w + 1) + l = q + (width - 1).bit_length() + 2 + out = t + g + (n - 1).bit_length() + 4 + return (n, B, g, q, w, l, out) + +def reference(p, alpha, theta, t): + n, B, g, q, w, l, out = parameters(p, alpha, theta, t) + plo, phi = pi_bounds(l + 20) + rho = 1 + theta + a = [[0] * n for _ in range(n)] + terms = 0 + for k in range(n): + for i in range(max(0, k - w), min(n, k + w + 1)): + z = (F(i) - (F(k) + F(1, 2)) / rho) ** 2 / (alpha * alpha) + lo, _ = expneg(phi * z, l + 10) + _, hi = expneg(plo * z, l + 10) + lo /= alpha + hi /= alpha + mid = (lo + hi) / 2 + s = 1 << l + v = (2 * mid.numerator * s + mid.denominator) // (2 * mid.denominator) + need(F(v - 1, s) <= lo <= hi <= F(v + 1, s), 'certified entry rounding') + a[k][i] = v + terms += 1 + return (a, dict(p=p, alpha=alpha, theta=str(theta), N=n, B=B, G=g, Q=q, W=w, entry_bits=l, inverse_bits=out, formed_entries=terms, inverse_guard=inverse_guard(p, alpha, theta)[1])) + +def inverse_candidate(a, l, bits, digits): + n = len(a) + with localcontext() as c: + c.prec = digits + scale = Decimal(2) ** l + lu = [[Decimal(v) / scale for v in row] for row in a] + perm = list(range(n)) + for k in range(n): + p = max(range(k, n), key=lambda i: abs(lu[i][k])) + need(lu[p][k] != 0, 'nonzero candidate pivot') + lu[k], lu[p] = (lu[p], lu[k]) + perm[k], perm[p] = (perm[p], perm[k]) + upper = [(j, lu[k][j]) for j in range(k + 1, n) if lu[k][j]] + for i in range(k + 1, n): + if lu[i][k]: + f = lu[i][k] / lu[k][k] + lu[i][k] = f + for j, u in upper: + lu[i][j] -= f * u + lower = [[(j, lu[i][j]) for j in range(i) if lu[i][j]] for i in range(n)] + upper = [[(j, lu[i][j]) for j in range(i + 1, n) if lu[i][j]] for i in range(n)] + result = [[0] * n for _ in range(n)] + scale = Decimal(2) ** bits + for col in range(n): + y = [Decimal(0)] * n + for i in range(n): + y[i] = Decimal(perm[i] == col) - sum((v * y[j] for j, v in lower[i]), Decimal(0)) + for i in range(n - 1, -1, -1): + y[i] = (y[i] - sum((v * y[j] for j, v in upper[i]), Decimal(0))) / lu[i][i] + for i in range(n): + result[i][col] = int((y[i] * scale).to_integral_value(rounding=ROUND_HALF_EVEN)) + return result + +def residual(a, r, l, out): + n = len(a) + den = 1 << l + out + cols = [0] * n + rowmax = 0 + for i, row in enumerate(a): + acc = [0] * n + for k, v in enumerate(row): + if v: + for j, u in enumerate(r[k]): + acc[j] += v * u + acc[i] -= den + rowmax = max(rowmax, sum(map(abs, acc))) + for j, v in enumerate(acc): + cols[j] += abs(v) + return F(max(rowmax, max(cols)), den) + +def norms(r, out): + return F(max(max((sum(map(abs, row)) for row in r)), max((sum((abs(row[j]) for row in r)) for j in range(len(r))))), 1 << out) + +def exact_candidate(a, entry_bits, output_bits): + """Use exact elimination if the numerical proposal fails its certificate.""" + n = len(a) + scale = 1 << entry_bits + rows = [[F(v, scale) for v in row] + [F(i == j) for j in range(n)] for i, row in enumerate(a)] + for k in range(n): + pivot = next((i for i in range(k, n) if rows[i][k]), None) + need(pivot is not None, 'invertible dyadic reference') + rows[k], rows[pivot] = (rows[pivot], rows[k]) + value = rows[k][k] + rows[k] = [x / value for x in rows[k]] + for i in range(n): + if i != k and rows[i][k]: + value = rows[i][k] + rows[i] = [x - value * y for x, y in zip(rows[i], rows[k])] + scale = 1 << output_bits + return [[(2 * x.numerator * scale + x.denominator) // (2 * x.denominator) for x in row[n:]] for row in rows] + +def certify(a, r, meta, accuracy): + n = meta['N'] + need(len(a) == len(r) == n and all((len(row) == n for row in a + r)), 'complete square arrays') + epsilon = residual(a, r, meta['entry_bits'], meta['inverse_bits']) + inverse_norm = norms(r, meta['inverse_bits']) + delta = F(min(n, 2 * meta['W'] + 1), 1 << meta['entry_bits']) + F(1, 1 << meta['Q'] + 3) + need(epsilon <= F(1, 1 << accuracy + meta['G'] + 3), 'inverse residual') + need(inverse_norm <= 2 * meta['B'], 'inverse norm guard') + error = meta['B'] * (delta * inverse_norm + epsilon) + need(error <= F(1, 1 << accuracy), 'full-cell inverse error') + return dict(reference_error=str(delta), residual=str(epsilon), inverse_norm=str(inverse_norm), inverse_error=str(error)) + +def prepare(p, alpha, theta, accuracy): + a, meta = reference(p, alpha, theta, accuracy) + method = 'certified Decimal proposal' + try: + r = inverse_candidate(a, meta['entry_bits'], meta['inverse_bits'], 60) + certificate = certify(a, r, meta, accuracy) + except (ValueError, ArithmeticError): + r = exact_candidate(a, meta['entry_bits'], meta['inverse_bits']) + certificate = certify(a, r, meta, accuracy) + method = 'exact rational elimination' + receipt = dict(parameters=meta, accuracy_bits=accuracy, method=method, certificate=certificate, reference_sha256=sha256(json.dumps(a, separators=(',', ':')).encode()).hexdigest(), inverse_sha256=sha256(json.dumps(r, separators=(',', ':')).encode()).hexdigest()) + return (a, r, receipt) diff --git a/research/dyadic-full-cell-gaussian/vendor/GAUSSIAN.md b/research/dyadic-full-cell-gaussian/vendor/GAUSSIAN.md new file mode 100644 index 0000000000..adfb28c93e --- /dev/null +++ b/research/dyadic-full-cell-gaussian/vendor/GAUSSIAN.md @@ -0,0 +1,263 @@ +# Fine-prime Gaussian assembly audit + +Written all-size argument, 2026-10-19; PROOF.md supplies final integration. +This is not a formal proof-assistant certification. +Retained sources are PR1673's capped Gaussian papers and PR1758/1786's +shifted Toeplitz, sparse-union and fine-prime constructions. Their original +conditional labels are not treated as proofs of their interface premises. + +## One fixed reference matrix and uniform conditioning + +Use theta=t/s-1 in [1/(4p^2),1/p^2], rho=1+theta and +alpha=ceil(sqrt((4/pi)log(16p))). Write a=pi alpha^2 and b=pi/(alpha^2 rho^2). +Eventually 4log(16p)<=a<=5log(16p). Source primes, alpha and all cutoffs are +computed from p. The prime-interval argument in the pinned fine-prime proof +uses Trudgian's explicit unconditional prime-counting bound; its main term +t/(4p^2 log t) dominates its error because log t=Theta(p^(1-epsilon)). +There are eventually more than d distinct primes in the required intervals. +Trial division costs 2^O(p^(1-epsilon))*poly(p)=2^o(p). The capacity ratio +T/S<2 follows from sum theta_i=O(d/p^2). No unproved short-interval premise +is used; small failed parameter checks invoke the elementary multiplier. + +Let N be the normalized narrow Gaussian matrix. The exact nearest-neighbor +pair estimate and Gaussian tail give +||N-I||_infinity <= exp(-2a theta)+5exp(-2a). +Thus its row gap exceeds 1/(8p^2) eventually. Remove its tiny diagonal +aliases, truncate at physical bandwidth W=O(sqrt(p)polylog(p))=1/(16p^2) and row norm<2. Augment target holes by identity. +This gives Haug permutation-similar to H direct_sum I, with bandwidth= (1-exp(-gamma theta)) exp(-pi^2/(3gamma)) > p^-5 + +eventually. To check the last inequality, gamma=Theta(1/log p), +theta>=1/(4p^2), and pi^2/(3gamma)=a rho/3 <=2 log p eventually. +Use 1-exp(-gamma theta)>=gamma theta/2. Therefore every capped broad +interior K has ||K^-1||_2=theta/2. For the broad block choose the shrunken +shift s=-delta(1-theta), whose gap>=theta. The remaining diagonal range +on a capped block is O(a theta B^2+a theta B), not O(aB). + +For the normalized shifted Gaussian symbol, Jacobi's product and the +interlaced phase bound prove + + Re phi >= (1-exp(-gamma(1-2|s|))) exp(-pi^2/(3gamma)), + ||phi|| <= 3+sqrt(2pi/gamma). + +Both bounds are polynomial in p for gamma=Theta(log p) or Theta(1/log p). +Every finite Toeplitz section is therefore accretive with polynomial +norm and inverse norm. Every recursive Schur descendant has inverse norm +at most mu^-1 and norm at most Lambda+Lambda^2/mu. In bounding its +shears use this enlarged bound; Lambda/mu alone is not required. + +vendor/SHALLOW-TOEPLITZ.md gives an explicit no-ancilla circuit. Its Schur +displacement rank grows by at most one per level; a rank-r Stein +displacement gives T=sum L(g_j)U(h_j). With bounded orthonormal generators, +use P=I+U(h)/gamma0, gamma0>=2||h||_1, and +Px; y+=gamma0 L(g)x; P^-1x; y-=gamma0 L(g)x. +This is a dirty shear with restored source. The triangular parity split +runs its two children on disjoint coordinates. These identities give +depth O(log^4 B) and logarithmic prefix norm O(log B log poly(p)). +Partial generator shears add; their norms are not multiplied as though +they were unrelated dense matrices. Ancestor factors contribute only +O(log B) polynomial factors along a recursive path. + +Exact rational Schur matrices and normalized rational Gram-Schmidt give +a polynomial-time coefficient generator. Offline rational numbers may +have poly(p) bits. Final data-gate coefficients and all relevant prefix +norms need only O(log^2 p) guard bits per axis. The shifted circuit may +approximate the fixed reference interior, rather than share identical +rounded coefficients: its entry error is poly(p)2^-Cp, and +X^-1-Y^-1=X^-1(Y-X)Y^-1 bounds the inverse error as well. + +For g=p^beta axes the total uncompleted log amplification is + + O(g a B^2/p^2 + g polylog(p)). + +The exact ledger checks beta+2xi-2<1 and beta<1. Thus this is o(p). +The complex supplier's own common-grid guard is O(g)=o(p). One fixed +Cp+o(p) online precision suffices for the complete tensor circuit. + +## The five factors, boundary arithmetic and current-value union schedule + +Write Q=[[A,B1],[C1,D1]], with F=D1-C1 A^-1 B1. Execute + + Q^-1=diag(A^-1,I) E_-B1 diag(A,F^-1) E_-C1 diag(A^-1,I), + Q=diag(A,I) E_C1 diag(A^-1,F) E_B1 diag(A,I), + +in right-to-left matrix order. Here E_B1 and E_C1 are the corresponding +upper/lower shears with ORIGINAL banded couplings. There are three dense +interior stages and two sparse windows. Dense stages require scattering +the prior sparse union and gathering a new one afterwards. + +For the narrow inverse, strict row diagonal dominance survives every +elimination with at least the original row gap and bounded row sum. +Every principal inverse is polynomially bounded. This bounds every pivot, +Schur matrix and partial block right-hand side in a no-pivot boundary solve. +For the broad forward map, F is APPLIED, never inverted; its norm is +bounded by ||D1||+||C1|| ||A^-1|| ||B1||. It is banded after the carve. + +Batch right-hand sides in dyadic width between W and2W. Dense block updates +use Strassen's seven-product identity. Its recursive additions have +polynomial growth in W; 7^16<2^45 gives exponent tau=45/16. Rounding after +each block update creates residual poly(p)2^-Cp. A core has polynomial +length and its inverse and partial solve norms are polynomial, so the +total local residual remains poly(p)2^-Cp. All pages, copied headers, +transposes, erasures and rewinds are charged. The global boundary cost is + + O(V d W^(tau-1)/B polylog(p)). + +Use the per-visit schedule in vendor/UNION-SCHEDULE.md, not the older g scans of +the whole union. Each record carries F(x)={i:xi in Ei}. These flags are +invariant under every sparse factor. Round r tags a current record by +the r-th member of F(x), stably distributes by that axis, transposes the +polynomial row field and applies the axis factor on complete Ei-lines. +The tag restriction depends only on the other coordinates along such a +line. Undo the transpose and distribution before deleting finished records. +Later rounds use the updated values. Stored split masks reconstruct the +original order on return. The number of visits is exactly +sum_x |F(x)|=sum_i |Ui|<=g mu V in record units. + +Tag extraction and headers have O(g log L)=o(p) bits and fit the cost of +each visited coefficient. Two-tape stable radix passes and level-by-level +lockstep transposes use a fixed number of tapes. Payload records deleted +at different rounds are disjoint; all indicator stacks together have at +most g V bits, which fits O(Vp) bits because gfloor(tj/s+1/2) are increasing injections. Their +tensor product preserves lexicographic order. A target coordinate k has +candidate j=max(0,ceil(s(2k-1)/(2t))); membership is exactly j0, put b=pi/alpha². Let 0=1)(1-exp(-2tr)), and a=alpha exp(b/4)/P(b)^3. +On H=L²(0,infinity) direct-sum L²(0,infinity), let T have kernel + + T(x,y)=exp(-b(y²-x²)) 1{x<=y}. + +Partition the finite indices at floor(N/2). U_h maps e_i to the normalized +indicator h^-1/2 1_[hi,h(i+1)) in the first summand on the left half; +on the right half it maps e_i to the analogous indicator indexed by n-i +in the second summand. U_h is an isometry. Its adjoint averages over cells; +the orthogonal complement of its image is mapped to zero. Then + + || U_h (h A) U_h* - a(T direct-sum T) || -> 0. + +In particular, + + sqrt(theta) ||K^-1||₂ -> alpha exp(b/4)/(2 sqrt(b) P(b)^3). + +This is for each fixed alpha. Uniformity for alpha growing with theta is +NOT asserted. The section is N=floor(1/theta), beta_0=-1/2; changing section +length or starting phase can change the limit. The result determines the +finite matrix boundary layers, not merely a formal differential expression. + +## Exact predecessor identity and full coefficient + +Credit the finite Gaussian q-LDU identity to the lineage retained by Vlado +Vojdanovski/#1673 and Jose Manuel/#4193, reproduced by JoyboyBrian/#5103 and +Nick Petalas/#5150. Set gamma=b/rho, q=exp(-gamma), Q=q², +P_j=product_(r=1)^j(1-Q^r). For G[i,j]=q^((i-j)²), + + G^-1[i,j]=(-1)^(i+j) sum_(k=max(i,j))^(N-1) + q^(2k-i-j) P_k/(P_i P_(k-i) P_j P_(k-j)). + +K=Dr G Dc with the exact positive diagonals in #5103. For i<=j, d=j-i, +define the FULL positive coefficient (not just its first summand) + + F_ij = sum_(r=0)^(N-1-j) Q^r P_(j+r)/(P_i P_(d+r) P_j P_r). + +Then + + A_ij = alpha exp(E_ij) F_ij, + E_ij = b beta_j²/rho² - gamma theta(j²-i²), + beta_j=theta j-1/2. (1) + +For i>j the same coefficient after reflection i'=n-i,j'=n-j satisfies + + E_ij = b beta_j²/rho² + - gamma theta[(j'+delta)²-(i'+delta)²], + delta=1/theta-n in [1,2). (2) + +The coefficient is invariant under simultaneous reflection because G and +G^-1 are. These are exact formulas. In particular all entries of A are +nonnegative. The predecessor entry lemma gives F_ij<=P(gamma)^-3. +Both exponents are <=b/4. The upper triangle is attached to the left edge; +the strictly lower triangle is attached to the right edge. We assign the +diagonal only to the upper triangle. + +Here is the coefficient limit with an explicit error. For gamma>=b/2 put +r0=exp(-b) and p0=exp(-r0/(1-r0)²). Then all finite products and P(gamma) +are >=p0, because -log(1-z)<=z/(1-z) and geometric summation apply. +Also |P_j-P(gamma)|<=r0^(j+1)/(1-r0). For i>=m, d>=m and N-j>=m+1, + + |F_ij-P(gamma)^-3| <= E_m, + E_m=5 p0^-5 r0^m/(1-r0)². (3) + +Indeed replace P_(j+r), P_i, P_(d+r), P_j by P(gamma) in each term. +The numerator and three inverse factors have telescoping error bounded by +4 p0^-5 r0^(m+1)/(1-r0). Sum Q^r<=1/(1-r0), and bound the omitted tail +by p0^-4 r0^(N-j)/(1-r0). The limiting infinite sum is +P(gamma)^-2 sum Q^r/P_r =P(gamma)^-3: the sum telescopes since +Q^r/P_r=1/P_r-1/P_(r-1) for r>=1. This is why the prefactor contains +THREE infinite-product factors. Dropping all but r=0 does not recover it. +Finally logarithmic differentiation of the convergent product gives + + |P(gamma)^-3-P(b)^-3| <= L_b h², + L_b=6 b p0^-3 r0/(1-r0)³, (4) + +using b-gamma<=b h². Termwise differentiation is justified by the same +summable bound 2 sum k r0^k/(1-r0). + +## Uniform tails, including the middle and cross-edge entries + +Set C=alpha exp(b/4)p0^-3. For i<=j the matrix entry is at most +C exp[-gamma h²(j²-i²)]. For i>j use the reflected bound with delta>=0, +which is no larger than C exp[-gamma h²(j'²-i'²)]. +Fix R>=1, h<=1/2, J=floor(R/h), and suppose 2J<=N. Remove the left +upper-triangular J by J corner and the right strictly-lower J by J corner. +For the upper remainder j>=J, j²-i²=(j-i)(j+i)>=(j-i)J. Every row sum +and every column sum of h times this remainder is bounded by + + C h sum_(d>=0) exp(-gamma h² J d) + <= C(h+1/(gamma h J)) <= C(h+2/(gamma R)). + +The inequality 1/(1-exp(-z))<=1+1/z follows from exp(z)>=1+z. +The lower remainder has the identical bound by reflection. Schur's test +therefore bounds their SUM in operator norm by 2C(h+4/(bR)). This bound +includes the middle and cross-edge blocks; no unproved localization is used. +The two retained corners act in different summands of H, so are a direct +sum, not a sum on a shared output. In particular their norms do not add +in quadrature. + +For the continuum operator, remove its [0,Jh]² triangle. The same row and +column integral bound gives norm <=1/(b Jh)<=2/(bR). After multiplying +by a<=C and allowing both summands, the continuum tails cost <=4C/(bR). +Together the discrete and continuum tail errors are safely bounded by + + 4C(h+4/(bR)). (5) + +This also proves boundedness of T, by a compact-window bound plus its tail. + +## Compact-window comparison and a quantitative convergence regime + +Suppose J>=m>=1 and N-J>=m+1 as well. On each corner the integral kernel +of U_h(h A)U_h* is A_ij on its h by h cells: the h in h A cancels the +normalization h^-1 from the two indicators. On cells with i>=m and +j-i>=m, (3)-(4) control the coefficient. Everywhere both the discrete +kernel and the proposed limiting kernel have magnitude <=C. + +For x in [hi,h(i+1)), y in [hj,h(j+1)), 0<=i<=j=1 and h<=1/2, gives + + |E_ij-[b/4-b(y²-x²)]| <= D, + D=12b(R+1)²h. (6) + +For example the beta²/rho² discrepancy is at most b[h(R+2)+h²], +the gamma discrepancy at most b h²(R+2)², the reflected delta term +at most4bRh, and rounding x,y to cell endpoints at most4b(R+1)h. +Their sum is bounded by (6). Each exponential argument is <=b/4, so +the mean-value theorem gives an absolute exponential error <=exp(b/4)D. + +The exceptional cells i=m, N-J>=m+1; these follow from R/h=h^-11/10, +m<=2h^-1/5 and h<=1/64. Every term of (8) tends to zero, including +R r0^m. Alternatively first choose R, then m, then h. Constants can be +very large for large alpha; this is not a uniform growing-alpha estimate. + +## Exact half-line norm and the endpoint domain + +Let L=-d/dx+2bx on its maximal domain of locally absolutely continuous +u with u,Lu in L²(0,infinity). No boundary condition is imposed on u at0. +For compactly supported smooth f, u=Tf is locally absolutely continuous, +satisfies Lu=f and lies in L². The homogeneous solution exp(bx²) is not +in L², so this inverse is unique. Boundedness extends T to all L² and +identifies it with L^-1 by closedness (or the distributional equation). + +The adjoint is L*=d/dx+2bx on its maximal L² graph domain with g(0)=0. +Integration by parts first on compact intervals proves the boundary term; +cutoffs and the graph norm give the stated domains. More explicitly the +Dirichlet form identity below controls both g' and xg. Truncation and +mollification with the zero trace show that smooth compactly supported +functions on [0,infinity) vanishing at0 form a graph core. At infinity +the boundary term vanishes by those cutoffs. These facts also follow by +solving the first-order distributional adjoint equation and imposing its +boundary pairing with arbitrary u(0). + +For that core, integration by parts gives + + ||L*g||² = integral [|g'|²+4b²x²|g|²-2b|g|²] + >=4b ||g||². (9) + +A direct proof of the inequality, requiring no oscillator spectrum, is the +ground-state identity with v=x exp(-bx²): + + integral [|g'|²+(4b²x²-6b)|g|²] + = integral v² |(g/v)'|² >=0. + +Use a cutoff at0 first; g(0)=0 makes the limiting boundary term zero. +The identity extends by the graph core. Duality then gives +||Tf||<=||f||/(2sqrt(b)): for every core g, +=, and the range of L* is dense (ker L=0). +Density and (9) bound this functional on that range, giving the asserted +bound without a boundary assumption on Tf itself. +Equality is attained at f(x)=x exp(-bx²), since + + T f(x)=exp(-bx²)/(4b), + ||exp(-bx²)||² / ||x exp(-bx²)||²=4b. + +Therefore ||T||=1/(2sqrt(b)). This is a half-line Dirichlet condition on +the ADJOINT, derived from the original Volterra inverse, not an assumed +Neumann condition on a full-line oscillator. The direct sum has the same +norm as either summand. Norm continuity in (8) completes the theorem. + +## Relationship to the formal prediction and limitations + +Ryanson Jonathan/#4408 observed theta^-1/2 growth; #4435 proposed +exp(pi alpha²/4)/(2alpha sqrt(pi)) by a two-frequency approximation and +explicitly left the boundary condition and rigorous upper argument open. +JoyboyBrian/#5103 proved a full-cell upper order; Nick Petalas/#5150 proved +a matching edge lower order. Those results and classical q-binomial +identities are credited dependencies, not new deliverables here. +The exact fixed-alpha coefficient above keeps the entire theta product. +No replacement of it by the formal large-alpha expression is made, and no +joint theta/alpha limit is inferred. The new result is the complete +operator-norm boundary-layer limit with its domain and explicit remainder. + +The exact-real theorem does not supply coefficient preparation, an inverse +application algorithm, rounded prefixes, integer width, physical movement +or storage, native supplier admission, outer transfer or integer recovery. +No selected frontier or multiplication theorem changes. + +## Open next questions + +1. Obtain useful uniform constants for the production growing-alpha regime; + (8) is explicit but too coarse to assert that regime. +2. Classify sections whose endpoint distance or length scales like sqrt(theta), + where a different limiting interval or boundary layer can occur. +3. Bind an actual rounded complete Gaussian caller, preserving all preparation, + prefix, movement and storage charges, before substituting any new guard. diff --git a/research/dyadic-full-cell-gaussian/vendor/PR5479.md b/research/dyadic-full-cell-gaussian/vendor/PR5479.md new file mode 100644 index 0000000000..90262d4a23 --- /dev/null +++ b/research/dyadic-full-cell-gaussian/vendor/PR5479.md @@ -0,0 +1,224 @@ +# A uniform production-scale Gaussian boundary limit + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +This is a scoped written theorem with exact finite corroboration, not a +formal-kernel or independent-human proof acceptance. + +## Quantifiers and exact source + +Let h=sqrt(theta), rho=1+theta, N=floor(1/theta), and n=N-1. For +0<=k,i=1}(1-exp(-2tr)), a_b=alpha exp(b/4) P(b)^-3, +and s=sqrt(b)*h. Split the indices at floor(N/2). Embed each left index +as the normalized indicator of [si,s(i+1)) in the first L² half-line; +embed right index i as the corresponding indicator at n-i in the second. +Call this isometry U_s. Let T have kernel +exp(-(y²-x²)) 1{x<=y} on L²(0,infinity). + +Uniformly for + + h -> 0, h^(1/5) <= b <= 1, (1) + +we prove + + || U_s (s A/a_b) U_s* - (T direct-sum T) || -> 0. (2) + +The retained half-line proof establishes ||T||=1/2 using the maximal +first-order operator -d/dx+2x and its Dirichlet adjoint; we retain that +endpoint-domain result. Thus (2) gives the uniform relative asymptotic + + ||K^-1||₂ = (1+o(1)) alpha exp(b/4) + / (2 sqrt(b theta) P(b)^3). (3) + +This extends the predecessor's fixed-alpha theorem to a specified joint +regime. The first retained source case remains alpha=3,theta=1/400,N=400; +that small fixture need not satisfy the eventual domain (1). Source geometry +is checked exactly, not used as evidence that an asymptotic quantifier holds. + +The actual PR4100 setup is alpha=ceil(sqrt((4/pi)log(16p))) and +1/(4p²)<=theta<=1/p². It satisfies (1) eventually, uniformly in theta. +Here p tends through positive integers, logarithms are natural, and the +ceil and floor in the displayed source are retained. This is the untruncated +full cell, not a claim that the existing capped RawGaussian API accepts it. + +## Relative q-product lemma + +Retain the exact q-LDU identity, credited through #1673, #4193, #5103 and +#5150 and the pinned half-line theorem. Set gamma=b/rho, Q=exp(-2gamma), +P_j=product_{r=1}^j(1-Q^r), P=P(gamma). For i<=j define L=N-1-j and + + F_ij=sum_{r=0}^L Q^r P_(j+r)/(P_i P_(j-i+r) P_j P_r). + +Then A_ij=alpha exp(E_ij)F_ij, with + + E_ij=b(theta*j-1/2)²/rho²-gamma*theta*(j²-i²). (4) + +For i>j reflect both indices: i'=n-i,j'=n-j, with i'=1 put + + eps_m=Q^(m+1)/((1-Q)(1-Q^(m+1))). + +If i>=m, j-i>=m, and L>=m, then + + exp(-4 eps_m) <= P³ F_ij <= 1. (6) + +Here are the details that avoid the predecessor's exponentially poor +absolute constants. Write R_j=P_j/P. For j>=m, + + 0<=log R_j=sum_{r>j}-log(1-Q^r) + <=Q^(j+1)/((1-Q)(1-Q^(j+1)))<=eps_m. + +The positive weights w_r=P Q^r/P_r sum to one, since +Q^r/P_r=1/P_r-1/P_(r-1) for r>=1. Moreover +sum_{r=0}^L w_r=P/P_L=1/R_L>=exp(-eps_m). Now + + P³ F_ij=sum_{r=0}^L w_r R_(j+r)/(R_i R_(j-i+r) R_j). + +Each numerator is >=1 and each of the three denominator factors is +<=exp(eps_m), proving the lower bound. For the upper bound, +P_(j+r)/P_j<=1, P_i,P_(j-i+r)>=P, and sum Q^r/P_r<=1/P. +This also proves P³F<=1 outside the good region. No finite product is +silently substituted for P, and the whole r-sum is essential. + +For b<=1, h<=1/2, gamma>=b/2. Logarithmic differentiation gives + + d log P(t)/dt = sum_{r>=1} 2r/(exp(2tr)-1) + <= 2/(1-exp(-b))³ <=16/b³, gamma<=t<=b. + +Consequently, with + + k=exp(48 h²/b²)-1, + +we have 1<=P(b)^3/P(gamma)^3<=1+k. On the good cells, + + |P(b)^3 F_ij-1| <=4(1+k)eps_m+k. (7) + +Everywhere 0<=P(b)^3 F_ij<=1+k. The derivative bound follows from a +convergent geometric majorant, so differentiation under the sum is valid. + +## Uniform operator estimate + +Choose R>=1, J=floor(R/s), m>=1, and assume s<=R/2, +2J<=N, J>=m, and N-J>=m+1. Retain the left upper-triangular J-square +and right strictly-lower J-square, assigning the diagonal only once. +Their images lie in the two different half-line summands. + +In the upper remainder j>=J, j²-i²>=(j-i)J. Each row sum and each +column sum of sA/a_b is at most + + (1+k)s sum_{d>=0} exp(-s² J d/rho) + <=(1+k)(s+rho/(sJ)) <=(1+k)(s+4/R). + +We used rho<=2 and sJ>=R/2. Reflection gives the same estimate on the +lower remainder. This includes middle and cross-edge entries. The +continuum remainder has norm at most 2/R per summand by the analogous +row/column integral; using a sum instead of a maximum only enlarges +our bound. A safe combined discrete/continuum tail allowance is + + 4(1+k)(s+4/R). (8) + +On each retained square, x=s(i+u), y=s(j+v), 0<=u,v<=1. The exponent +bound in the pinned half-line proof, with its window radius replaced +by R/sqrt(b), gives + + |E_ij - (b/4-(y²-x²))| <= D, + D=12(R+1)² h. (9) + +Indeed its bound is 12b(R/sqrt(b)+1)²h, at most (9) when b<=1. +The same calculation covers the reflected offset delta in [1,2). +Both exponents after subtracting b/4 are nonpositive, hence exp has +Lipschitz constant one on their range. + +Cells with i=h^(11/10); thus R/s>=h^(-11/10), + J<=h^(-6/5), while N=floor(h^-2). Hence 2J<=N. +* m<=2h^(-2/5), so J>=m and N-J>=m+1 eventually. +* ms(R+1)<=4h^(3/5): use m<=h^(-1/5)/b+1, + s=h sqrt(b), b>=h^(1/5), and R+1<=2h^(-1/10). +* Q<=exp(-b); bm>=h^(-1/5). Thus + eps_m<=4b^-1 exp(-h^(-1/5)) + <=4h^(-1/5)exp(-h^(-1/5)). +* k<=exp(48h^(8/5))-1, and RD<=48h^(7/10). + +All terms in (10) tend to zero uniformly. In particular the R times +exponential tail vanishes, Rk=O(h^(3/2)), and (8) is O(h^(1/10)). +This proves (2) without exchanging two unquantified limits. + +## Production polynomial conditioning, with ceilings preserved + +Put l=log(16p). The actual alpha satisfies +sqrt(4l/pi)<=alpha=1} f(2br) + <=(1/(2b)) integral_0^infinity f(x)dx + =pi²/(12b). + +The integral follows by the positive exponential series and +sum_{k>=1}1/k²=pi²/6. Therefore P(b)^-3<=exp(pi alpha²/4). +For sufficiently large p, (2) bounds the normalized norm by one, giving + + ||K^-1||₂ <= alpha²/(sqrt(pi)*h) + exp(b/4+pi alpha²/4) + <= 2p alpha²/sqrt(pi) + exp(b/4+l+sqrt(pi*l)+pi/4). (11) + +For every fixed eta>0, the right side is <=p^(2+eta) eventually. +This is a uniform polynomial upper bound, with the asymptotic coefficient +still given exactly by (3). We do not replace its product by an unproved +large-alpha formula, nor assert a sharp p-power lower bound here. +In particular a p^10 allowance eventually dominates this *exact full-cell +inverse norm*. A rounded or truncated reference would additionally need +its own perturbation bound (for example ||K^-1|| ||Delta||<1); this proof +has not admitted such a reference or its circuit. + +## Decision, costs and next obligations + +The fixed-alpha restriction is removed for the actual production scale. +A full-cell conditioning objection based solely on taking alpha to infinity +is therefore resolved for this exact kernel. Existing capped-section +conditioning arguments remain separate, and no existing program is changed. + +The theorem constructs no coefficient producer or inverse-application +algorithm. Common rational reference formation, truncation, grid rounding, +all circuit prefix bounds, coefficient/page storage and physical delivery, +tape movement, preparation amortization and integer recovery retain their +costs and proof obligations. No charge is assigned zero; no runtime, +complete multiplication theorem, supplier admission or new kappa follows. + +Open next questions: bind a specified rounded full-cell reference using +(11) and its actual entry-error invoice; then determine whether any concrete +inverse consumer can exploit the guard while paying all preparation and +physical costs. An arbitrary-section or different-endpoint theorem requires +fresh geometry; the present N, phase and reflection domain must not be dropped. diff --git a/research/dyadic-full-cell-gaussian/verify.py b/research/dyadic-full-cell-gaussian/verify.py new file mode 100644 index 0000000000..a7457f097a --- /dev/null +++ b/research/dyadic-full-cell-gaussian/verify.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +"""Check the full-cell reference. Ali Romman with OpenAI Codex. Apache-2.0.""" +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +from runpy import run_path +from math import isqrt +import json + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def reject(fn): + try: + fn() + except ValueError: + return + raise ValueError('invalid control accepted') + + +def independent_exp(x, terms): + """Use a separate rational Taylor enclosure without range reduction.""" + term = total = F(1) + for j in range(1, terms+1): + term *= x/j + total += term + tail = term*x/(terms+1)/(1-x/(terms+2)) + return 1/(total+tail), 1/total + + +def check(): + for row in json.loads((HERE/'SOURCES.json').read_text())['external_inputs']: + need(sha256((HERE/row['local_path']).read_bytes()).hexdigest() == row['sha256'], + 'retained source changed') + m = run_path(str(HERE/'prepare.py'), run_name='preparation') + exp = m['expneg'] + comparisons = 0 + for x in (F(0), F(1, 257), F(1, 2), F(1), F(7, 3), F(17)): + lo, hi = exp(x, 80) + rlo, rhi = independent_exp(x, 240) + need(lo <= rlo <= rhi <= hi, 'independent exact exponential enclosure') + need(hi-lo <= F(1, 1 << 80), 'exponential width') + comparisons += 1 + pi_lo, pi_hi = m['pi_bounds'](120) + need(F(3141592653589793, 10**15) < pi_lo < pi_hi + < F(3141592653589794, 10**15), 'independent coarse pi bracket') + # The fixed Machin identity follows from this exact tangent calculation. + tangent = (F(120, 119)-F(1, 239))/(1+F(120, 119*239)) + need(tangent == 1, 'Machin tangent identity') + controls = 0 + receipts = [] + for p, theta, accuracy in ((16, F(1, 256), 4), (17, F(2, 599), 12), + (17, F(2, 599), 40)): + a, r, receipt = m['prepare'](p, 3, theta, accuracy) + meta = receipt['parameters'] + need(meta['N'] == (256 if p == 16 else 299), 'complete source floor') + lo, _ = exp(pi_hi, 80) + _, hi = exp(pi_lo*F(9, 4), 80) + need(hi < F(1, 16*p) < lo, 'actual source alpha is three') + rho = 1+theta + for k in (0, meta['N']//2, meta['N']-1): + for i in (0, meta['N']//2, meta['N']-1): + left = F(i)-(F(k)+F(1, 2))/rho + right = (2*i*rho-2*k-1)/(2*rho) + need(left == right, 'literal phase and dilation identity') + comparisons += 1 + bad = [row[:] for row in r] + bad[0][0] += 1 << meta['inverse_bits'] + reject(lambda: m['certify'](a, bad, meta, accuracy)) + controls += 1 + bad_a = [row[:] for row in a] + bad_a[0][0] = 0 + reject(lambda: m['certify'](bad_a, r, meta, accuracy)) + controls += 1 + reject(lambda: m['certify'](a, r[:-1], meta, accuracy)) + controls += 1 + receipts.append(receipt) + for prime in (17, 599, 601): + need(all(prime % d for d in range(2, isqrt(prime)+1)), 'literal prime fixture') + need(F(601, 599)-1 == F(2, 599), 'fine-prime ratio fixture') + # Force the exact completion path on independent small integer matrices. + exact_checks = 0 + for a in ([[0, 1], [1, 1]], [[3, 1], [2, 1]], + [[1, 2, 0], [0, 1, 3], [0, 0, 1]]): + r = m['exact_candidate'](a, 0, 24) + need(m['residual'](a, r, 0, 24) == 0, 'exact inverse with pivoting') + exact_checks += 1 + for args in ((15, 3, F(1, 256), 4), (16, 3, F(1, 2048), 4), + (16, 3, F(1, 256), -1)): + reject(lambda args=args: m['parameters'](*args)) + controls += 1 + reject(lambda: exp(-1, 40)) + reject(lambda: m['reference'](16, 4, F(1, 256), 4)) + controls += 2 + return dict(status='PASS_DYADIC_FULL_CELL_GAUSSIAN', cells=receipts, + exact_enclosure_and_geometry_checks=comparisons, + exact_inverse_checks=exact_checks, rejecting_controls=controls, + production_threshold=16, inverse_guard='5*p^6', + scope='Certified reference and inverse preparation; no physical caller or new kappa.') + + +def main(): + result = check() + need(result == json.loads((HERE/'RESULT.json').read_text()), 'fixed result receipt') + print(result['status']) + print('Complete 256- and 299-column cells; exact interval and inverse-residual certificates') + + +if __name__ == '__main__': + main()