diff --git a/research/asymmetric-gaussian-precision/PROOF.md b/research/asymmetric-gaussian-precision/PROOF.md new file mode 100644 index 0000000000..2aa143e3e0 --- /dev/null +++ b/research/asymmetric-gaussian-precision/PROOF.md @@ -0,0 +1,189 @@ +# Asymmetric accuracy for normalized convolution + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Contract and new conclusion + +Take the normalized channel in Jerry Chen / CubeJerry's +[#6993](https://github.com/CrocSwap/integer-mult-bounds/pull/6993), retained at +`research/deferred-gaussian-recovery/PROOF.md`, sections 2-4. Its exact +Fourier identity, source interfaces and physical endpoints are premises. +They are not reverified here. Cinna Davis's #4100 supplies the construction +and exact source definitions. Ryanson Jonathan's #4320 supplies the +identity/recovery audit, and his #4415 supplies the predecessor one-middle +error ledger. #6993 retains the further native, +scalar, source, codec and Fourier attribution in its NOTICE.md. + +Let b >= 1 and Gamma >= 0 be integers, and let 1 <= S < 2^b. Set + + h = ceil(log2 S), a = 2h + 2b + 7, + epsilon = 2^-a, lambda = 2^-Gamma. + +All vector norms in the argument are the maximum complex modulus. The two +ideal forward maps and the ideal opposite map are lambda times maps with +operator norm at most one. Their exact composition with pointwise product +is the inherited normalized convolution, with accumulated scale lambda^3. +The original input vectors have norm at most 1/4. + +Suppose the approximate forward calls have errors at most lambda epsilon +on those inputs. Suppose the approximate opposite call has error at most +lambda^3 epsilon on every admitted quarter-disk input, including its +actual rounded input. Keep the original common q grid, with + + q >= a + 3Gamma + 7, + +and retain every additional source, reference, native and ledger guard. +The pointwise operation multiplies exactly and truncates each real and +imaginary component toward zero once on that grid. No other uncharged +rounding operation is allowed. + +Then every forward return has norm below 1/2, the actual pointwise result +has norm below 1/4, and the opposite return has norm below 1/2. The final +error after multiplying by S^2 2^(2b+4+3Gamma) is strictly below 1/4. +Consequently the same final nearest-integer gate remains valid. + +The new forward-map tolerance is lambda epsilon, replacing #6993's +lambda^3 epsilon. It is larger by exactly 2^(2Gamma). This is an accuracy +allocation result, conditional on delivering the named maps. It asserts +no reduction in the common q grid or completed physical cost. + +## Separate the four error sources + +Write U,V for the ideal forward returns and Uhat,Vhat for the approximate +ones. More generally, allow forward errors alpha,beta, pointwise error +delta, and opposite error omega. Since |U|,|V| <= lambda/4, + + ||Uhat Vhat - UV|| + <= (lambda/4)(alpha+beta) + alpha beta. + +Multiplication is coordinatewise. Apply the ideal opposite map to the +actual rounded product first. Its operator norm is at most lambda. The +opposite algorithm's error is then charged at that actual input. The +complete error E in the normalized final result satisfies + + E <= lambda[(lambda/4)(alpha+beta) + alpha beta + delta] + omega. (1) + +This argument does not require the approximate routines to be linear or +contractive. Their error promises must hold on the reached input domains. + +Substitute alpha=beta=lambda epsilon and omega=lambda^3 epsilon. Each +component truncation has error below 2^-q, so the complex modulus error +satisfies delta < sqrt(2) 2^-q < 2^(1-q). The q guard gives + + delta < lambda^3 epsilon/64. + +Divide (1) by lambda^3 to obtain + + E/lambda^3 < epsilon(3/2 + epsilon + lambda/64) + <= epsilon(3/2 + 1/512 + 1/64) + = (777/512)epsilon < 2epsilon. (2) + +Here a >= 9, including S=1, b=1 and Gamma=0. The larger forward error is +attenuated once by the other forward output and once by the opposite map. +The opposite algorithm's own error has neither attenuation factor. + +## Verify the actual input and return radii + +Each approximate forward return has norm at most + + lambda(1/4+epsilon) <= 129/512 < 1/2. + +The actual rounded product has norm strictly below + + lambda^2(1/4+epsilon)^2 + lambda^3 epsilon/64 + <= (129/512)^2 + 1/32768 + = 16649/262144 < 1/4. (3) + +Thus the opposite error promise used in (1) applies to its actual input. +Its return norm is strictly below + + lambda(16649/262144) + lambda^3 epsilon + <= 17161/262144 < 1/2. + +These are the same interface radii required by #6993. In particular Gamma=0 +requires no separate limiting argument. The native half-disk carrier +checks remain applicable, and the pointwise quarter-disk guard is preserved. + +## Recover the integers at the unchanged scale + +Keep both exact S multiplications and the complete shift 2b+4+3Gamma. +By (2), the error after this restoration satisfies + + E S^2 2^(2b+4+3Gamma) + < 2epsilon S^2 2^(2b+4) + = S^2 2^(-2h-2) <= 1/4. + +The first inequality is strict even when S=2^h. The exact convolution +coefficient is real, so projection to its real component cannot increase +the error. Nearest-integer recovery is unambiguous. The source identity, +original-coordinate extraction, CRT and carry obligations remain inherited. + +## Translate the improvement into stage requests + +The three public stages of each transform are expansion, middle and +compression. Use the same source-interface implication as #6993, section 3: +if each stage has restored error below 2^-tau, then the complete normalized +map error is below 3*2^(-tau-Gamma). Every actual finite applicability guard +in that implication must still pass for that call. + +The previous request for every call was tau_old=a+2Gamma+2. Replace it by + + tau_forward = a+2, for each of the two forward calls, + tau_opposite = a+2Gamma+2, for the opposite call. + +Then the forward-stage sum is below 3lambda epsilon/4, and the opposite-stage +sum is below 3lambda^3 epsilon/4. Both fit the map budgets used above. Each +forward stage therefore requests exactly 2Gamma fewer accuracy bits. At +Gamma=0 the requests coincide. + +For each forward call independently, the same substitutions in #6993 give + + z_forward = tau_forward + Gamma + ceil(log2 m) + 1, + chi_forward = Gamma + tau_forward, + tau_comp_forward = tau_forward + K_f. + +The last equality preserves the compression-only normalization K_c, since +Gamma=K_f+K_c. The analogous opposite requests retain tau_opposite. These +are requests to separately prepared stage implementations, not a license +to reuse an old phase bank at a different declared accuracy. Preserve the +source-first ordering and all finite radius, normalizer, coefficient, q and +reference gates. A changed reference can change its derived parameters; +this proof does not assert that a previously admitted reference remains +admitted without checking its new declaration. + +The old q lower bound remains sufficient for the new forward source rule +q >= Gamma+tau_forward+5, because it is stronger by 2Gamma. Other guards +can still dominate. A maximum with the fixed q or another width can erase +a physical width reduction. The proved improvement is in requested +accuracy, with no unconditional storage, runtime or kappa improvement. + +## Why the opposite tolerance is retained + +The distinction is necessary in this error-only model. Take S=1, b=1, +Gamma=1, zero inputs, exact forward and pointwise operations, and an +opposite return error lambda epsilon. These satisfy the hypothetical +looser opposite tolerance. Here a=9 and restoration multiplies by 512, so +the final error is exactly 1/2. It fails the strict 1/4 recovery contract. +The retained opposite tolerance lambda^3 epsilon excludes this example. +This is a counterexample to relaxing all calls alike, not an error in #6993. + +Equation (1) is also exact in the scalar abstract additive-defect model: +use input values 1/4, ideal scalar maps multiplication by lambda, and align +all four nonnegative defects on the real axis. This equality only concerns +that abstract model. A freely signed pointwise defect is more permissive +than the actual inward truncator, and no sharpness claim for that truncator +or physical native algorithms follows. + +## Scope and verification + +The universal conclusion follows from the written inequalities. The +standard-library verifier supplies finite rational corroboration. It checks +separate budgets, exact length-1/2/4 convolution fixtures with literal +componentwise inward truncation, abstract scalar equalities and controls. +Its length-2/4 fixtures illustrate the norm contract; they are not the odd +production source domains. It imports no predecessor scientific verifier. + +All five selected framework assumptions remain. There is no production +transform, new native word, physical controller, supplier admission, +complete multiplication theorem or selected-frontier change. Independent +human and formal proof-kernel review are unclaimed. diff --git a/research/asymmetric-gaussian-precision/README.md b/research/asymmetric-gaussian-precision/README.md new file mode 100644 index 0000000000..c05bd13d54 --- /dev/null +++ b/research/asymmetric-gaussian-precision/README.md @@ -0,0 +1,98 @@ +# Relax normalized forward accuracy by 2Gamma bits + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. In the +normalized convolution channel of Jerry Chen / CubeJerry's +[#6993](https://github.com/CrocSwap/integer-mult-bounds/pull/6993), the two +forward transforms may each have map error `2^(-a-Gamma)` instead of +`2^(-a-3Gamma)`. The opposite-transform budget and common q grid stay as in +that interface. All actual-input radius guards and the final strict +integer-recovery error `<1/4` still hold under the stated source contracts. + +With `a=2ceil(log2 S)+2b+7`, `1<=S<2^b`, and integer `Gamma>=0`, the stage +requests become + +```text +forward expansion/middle/compression: tau = a+2 +opposite expansion/middle/compression: tau = a+2Gamma+2 +common grid: q >= a+3Gamma+7, plus actual source and ledger guards +``` + +This saves exactly `2Gamma` requested accuracy bits at each forward stage. +It does not guarantee smaller physical widths. Fixed q, other finite +source guards and preparation can dominate. There is no new kappa or +completed physical supplier. + +[PROOF.md](PROOF.md) gives the separate error polynomial, every reached +radius, the unchanged recovery scale and source-request substitutions. +The new step is this asymmetric allocation. The normalized identity, +S-squared scale and physical scalar endpoint belong to the predecessors. +Credit #6993, Cinna Davis #4100, Ryanson Jonathan #4320/#4415 and all retained +native, scalar, source, codec and Fourier contributors in #6993's NOTICE. +The classical product perturbation inequality is not claimed as a new +mathematical discovery. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/asymmetric-gaussian-precision +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/asymmetric-gaussian-precision/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/asymmetric-gaussian-precision/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/asymmetric-gaussian-precision --check-source-history +``` + +Replace the absolute interpreter with another CPython 3.12 installation +when reproducing elsewhere. Both registered commands print +`PASS_ASYMMETRIC_GAUSSIAN_PRECISION` in a generated JSON receipt bound to the +six package files. Optional `--receipt /absolute/external/path.json` saves +the same receipt outside the package. No receipt is hand-written or +required as a committed input. + +Local normal and optimized checks pass 315 budget cases, 1,152 convolution +executions, six abstract scalar equalities and ten controls. Both direct +commands took 0.17 seconds locally; these are validation durations, not a +runtime improvement. The registered replay also passes both commands. + +The verifier checks all its declared finite cases, not all mathematical +parameters. It includes literal inward rounding and an independent direct +convolution oracle for lengths 1, 2 and 4. These dyadic fixtures illustrate +the contract; they are not production odd-source transforms. The proof +covers arbitrary admitted source length under the inherited norm and +identity contracts. No predecessor scientific replay is run. + +## Limits + +Independent human and formal proof-kernel review are unclaimed. The selected +#7000 record, five framework assumptions, complete native/scalar costs, +original-coordinate extraction, CRT, carry/output and production source +admission are unchanged. New stage requests require their own source-first +preparation and finite applicability gates. No physical runtime, storage, +common-grid reduction or multiplication theorem is inferred. + +The verifier uses bounded finite loops and functions below 60 physical +lines. Python's Fraction and container operations require runtime allocation. +This is the managed-runtime deviation from Power of Ten rule 3, confined to +this offline checker. Fixture vectors have at most four entries; scalar +allocation inputs enforce b and Gamma at most 128, and dyadic helpers cap +exponents at 2048. Hashing reads at most one MiB per package file. There is +no recursion, dynamic code evaluation, solver, +network access or predecessor import. Warning-strict normal/optimized runs +and source compilation are the diagnostic checks. Any larger finite sweep +must explicitly revise those bounds; arbitrary-parameter correctness rests +on the proof rather than an unbounded checker loop. + +## Open next questions + +- Can an actual separately prepared forward controller use these relaxed + requests to lower a binding source or phase width? Pin its normalizers, + recompute its finite reference guards and compare complete paid costs. + No such controller is implemented here. +- Can a separately admitted pointwise precision schedule reduce the shared + q guard without adding conversion errors? Start from the four separate + terms in equation (1), include each grid adapter and retain the opposite + error budget. This package keeps the original common grid. + +The structured versions and blockers are in [TASK.json](TASK.json). diff --git a/research/asymmetric-gaussian-precision/SOURCES.json b/research/asymmetric-gaussian-precision/SOURCES.json new file mode 100644 index 0000000000..c271e117d9 --- /dev/null +++ b/research/asymmetric-gaussian-precision/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/deferred-gaussian-recovery/PROOF.md", + "usage": "provenance", + "git_blob": "83cd53079a804fd40a87b50324fdcec45de2e59d", + "sha256": "870fcf901001aad2b6380f57ce3ba38f31da0bd3bd36abac933a180d29f48db6" + }, + { + "path": "research/deferred-gaussian-recovery/README.md", + "usage": "provenance", + "git_blob": "11b78f5d5d5e82a2f29e858c18a93c99aa43d8a5", + "sha256": "3c2a17d1dd507e782ee974c870cfb5616e4c590fb36f1455ada782c92a307791" + }, + { + "path": "research/deferred-gaussian-recovery/NOTICE.md", + "usage": "provenance", + "git_blob": "0e91eaab44193c65f33f73bb7db54587cab7bda1", + "sha256": "f3c0d4d53fdd2a91d8b371d4f65820ed7ccf7fe93d381a3e7553aeeb0293f932" + } + ] +} diff --git a/research/asymmetric-gaussian-precision/TASK.json b/research/asymmetric-gaussian-precision/TASK.json new file mode 100644 index 0000000000..6778629f9a --- /dev/null +++ b/research/asymmetric-gaussian-precision/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "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" + ], + "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." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "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." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability 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." + ], + "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." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "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.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "A conditional asymmetric accuracy allocation for the normalized convolution channel, relaxing each forward map by exactly 2Gamma bits and preserving all radius and strict integer-recovery guards.", + "scope_change_reason": "The supplied task asks for one original result rather than an audit. This changes the supplier-admission card to a new analytic interface improvement at the cited PR6993 channel.", + "bottleneck_link": "Looser requested forward accuracy can reduce a binding source or phase preparation width. This proof does not infer a physical cost reduction when common q or other guards dominate.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified asymmetric precision improvement; do not optimize the remaining terms.", + "outcome": "completed", + "evidence": "PROOF.md and a standalone standard-library exact rational verifier with separate budgets, inward-rounded convolution fixtures, scalar equality witnesses and controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual forward controller lower a binding physical width with these relaxed stage requests?", + "why_it_matters": "A requested accuracy reduction improves cost only when it changes a fully paid physical implementation.", + "first_step": "Pin one controller, prepare its new references and phase bank, check all finite applicability guards, and compare the complete bill.", + "blocked_by": "No separately prepared production controller or full physical invoice is supplied." + }, + { + "question": "Can a separately admitted pointwise precision schedule lower common q while retaining the opposite accuracy budget?", + "why_it_matters": "The current common q can dominate widths and mask the requested forward accuracy gain.", + "first_step": "Use equation (1) with independently charged grid conversions and actual input radii.", + "blocked_by": "This proof retains the original common grid; new conversion errors and complete costs remain unpriced." + } + ], + "claim_type": "scoped written proof with finite exact corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542470", + "no_new_kappa": true, + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only" + }, + "finite_domain": "315 allocations: b=1..16, each valid distinct S in {1,2^b-1,2^(b-1)+1}, Gamma in {0,1,2,4,8,31,127}; 1152 convolution executions: lengths {1,2,4}, Gamma {0,1,2,7}, 24 deterministic input seeds, four defect directions; six abstract scalar equalities and ten controls." +} diff --git a/research/asymmetric-gaussian-precision/VERIFY.json b/research/asymmetric-gaussian-precision/VERIFY.json new file mode 100644 index 0000000000..ef07f403c1 --- /dev/null +++ b/research/asymmetric-gaussian-precision/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational budgets, literal inward-rounded convolution, independent direct convolution, scalar envelope equality and invalid/semantic controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact rational budgets, literal inward-rounded convolution, independent direct convolution, scalar envelope equality and invalid/semantic controls." + } + ] +} diff --git a/research/asymmetric-gaussian-precision/verify.py b/research/asymmetric-gaussian-precision/verify.py new file mode 100644 index 0000000000..bd8e86e953 --- /dev/null +++ b/research/asymmetric-gaussian-precision/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the asymmetric normalized-channel proof.""" + +import argparse +import hashlib +import json +import sys +from fractions import Fraction as F +from pathlib import Path + +type Complex = tuple[F, F] + +ZERO: Complex = (F(0), F(0)) +ROOTS: tuple[Complex, ...] = ((F(1), F(0)), (F(0), F(1)), + (F(-1), F(0)), (F(0), F(-1))) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def power(exponent: int) -> F: + require(type(exponent) is int and 0 <= exponent <= 2048, "exponent domain") + return F(1, 1 << exponent) + + +def allocation(b: int, size: int, gamma: int) -> tuple[int, int, int, int]: + require(all(type(x) is int for x in (b, size, gamma)), "integer parameters") + require(1 <= b <= 128 and 0 <= gamma <= 128, "finite verifier domain") + require(1 <= size < 1 << b, "source-size guard") + height = (size - 1).bit_length() + accuracy = 2 * height + 2 * b + 7 + return accuracy, accuracy + 3 * gamma + 7, accuracy + 2, accuracy + 2 * gamma + 2 + + +def error_bound(lam: F, left: F, right: F, product: F, opposite: F) -> F: + require(0 < lam <= 1, "normalizer domain") + require(min(left, right, product, opposite) >= 0, "nonnegative errors") + return lam * (lam * (left + right) / 4 + left * right + product) + opposite + + +def add(x: Complex, y: Complex) -> Complex: + return x[0] + y[0], x[1] + y[1] + + +def mul(x: Complex, y: Complex) -> Complex: + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def scale(x: Complex, factor: F) -> Complex: + return x[0] * factor, x[1] * factor + + +def norm1(x: Complex) -> F: + return abs(x[0]) + abs(x[1]) + + +def transform(data: tuple[Complex, ...], lam: F, sign: int) -> tuple[Complex, ...]: + n = len(data) + require(n in (1, 2, 4) and sign in (-1, 1), "finite transform domain") + output = [] + for row in range(n): + total = ZERO + for column in range(n): + root = ROOTS[(sign * row * column * (4 // n)) % 4] + total = add(total, mul(root, data[column])) + output.append(scale(total, lam / n)) + return tuple(output) + + +def convolution(left: tuple[Complex, ...], right: tuple[Complex, ...]) -> tuple[Complex, ...]: + n = len(left) + require(n == len(right) and n in (1, 2, 4), "finite convolution domain") + output = [] + for row in range(n): + total = ZERO + for column in range(n): + total = add(total, mul(left[column], right[(row - column) % n])) + output.append(total) + return tuple(output) + + +def truncate(value: F, bits: int) -> F: + require(type(bits) is int and 0 <= bits <= 2048, "grid domain") + numerator = abs(value.numerator) * (1 << bits) // value.denominator + if value < 0: + numerator = -numerator + return F(numerator, 1 << bits) + + +def budget_cases() -> int: + count = 0 + for b in range(1, 17): + sizes = sorted({1, (1 << b) - 1, (1 << (b - 1)) + 1} - {1 << b}) + for size in sizes: + for gamma in (0, 1, 2, 4, 8, 31, 127): + a, q, forward, opposite = allocation(b, size, gamma) + eps, lam = power(a), power(gamma) + eta_f, eta_o = lam * eps, lam**3 * eps + delta_cap = 2 * power(q) + bound = error_bound(lam, eta_f, eta_f, delta_cap, eta_o) + require(bound / lam**3 < 2 * eps, "restored error budget") + recovery = size**2 * (1 << (2 * b + 4 + 3 * gamma)) + require(bound * recovery < F(1, 4), "integer recovery margin") + require(lam * (F(1, 4) + eps) < F(1, 2), "forward radius") + product_radius = (lam * (F(1, 4) + eps))**2 + delta_cap + require(product_radius < F(1, 4), "opposite input radius") + require(lam * product_radius + eta_o < F(1, 2), "return radius") + require(opposite - forward == 2 * gamma, "requested bit improvement") + require(3 * power(forward + gamma) < eta_f, "forward stage sum") + require(3 * power(opposite + gamma) < eta_o, "opposite stage sum") + require(power(a + 3 * gamma) / eta_f == power(2 * gamma), "gain factor") + count += 1 + return count + + +def one_fixture(n: int, gamma: int, seed: int, direction: int) -> None: + b = n.bit_length() + a, q, _, _ = allocation(b, n, gamma) + lam, eps = power(gamma), power(a) + left = tuple(scale(ROOTS[(seed + j) % 4], F(1 + (seed + j) % 2, 8)) + for j in range(n)) + right = tuple(scale(ROOTS[(seed // 4 + 3 * j) % 4], F(1 + (seed + 2 * j) % 2, 8)) + for j in range(n)) + exact_left, exact_right = transform(left, lam, -1), transform(right, lam, -1) + actual_left = tuple(add(x, scale(ROOTS[(direction + j) % 4], lam * eps)) + for j, x in enumerate(exact_left)) + actual_right = tuple(add(x, scale(ROOTS[(direction + 2 * j) % 4], lam * eps)) + for j, x in enumerate(exact_right)) + product = tuple(mul(x, y) for x, y in zip(actual_left, actual_right, strict=True)) + rounded = tuple((truncate(x[0], q), truncate(x[1], q)) for x in product) + actual = tuple(add(x, scale(ROOTS[(direction + 3 * j) % 4], lam**3 * eps)) + for j, x in enumerate(transform(rounded, lam, 1))) + direct = tuple(scale(x, lam**3 / n**2) for x in convolution(left, right)) + exact_product = tuple(mul(x, y) for x, y in zip(exact_left, exact_right, strict=True)) + require(transform(exact_product, lam, 1) == direct, "independent convolution identity") + for first, second, raw, rounded_value, value, target in zip( + actual_left, actual_right, product, rounded, actual, direct, strict=True): + require(norm1(first) < F(1, 2) and norm1(second) < F(1, 2), "fixture forward guard") + require(norm1(add(rounded_value, scale(raw, F(-1)))) < 2 * power(q), "inward grid error") + require(norm1(rounded_value) < F(1, 4), "fixture opposite guard") + require(norm1(value) < F(1, 2), "fixture return guard") + defect = norm1(add(value, scale(target, F(-1)))) + bound = error_bound(lam, lam * eps, lam * eps, 2 * power(q), lam**3 * eps) + require(defect <= bound, "fixture error polynomial") + recovery = n**2 * (1 << (2 * b + 4 + 3 * gamma)) + require(defect * recovery < F(1, 4), "fixture recovery error") + + +def fixture_cases() -> int: + count = 0 + for n in (1, 2, 4): + for gamma in (0, 1, 2, 7): + for seed in range(24): + for direction in range(4): + one_fixture(n, gamma, seed, direction) + count += 1 + return count + + +def sharp_envelope_cases() -> int: + count = 0 + for gamma in (0, 1, 3): + lam = power(gamma) + for left, right in ((F(1, 1024), F(1, 2048)), (F(0), F(1, 4096))): + product, opposite = F(1, 8192), F(1, 16384) + actual = lam * ((lam / 4 + left) * (lam / 4 + right) + product) + opposite + ideal = lam**3 / 16 + require(actual - ideal == error_bound(lam, left, right, product, opposite), + "scalar equality in the abstract defect model") + count += 1 + return count + + +def controls() -> int: + count = 0 + for args in ((0, 1, 0), (1, 0, 0), (1, 2, 0), (2, 1, -1), + (129, 1, 0), (1, 1, 129), (True, 1, 0), (2, F(1), 0)): + try: + allocation(*args) + except ValueError: + count += 1 + else: + raise ValueError("invalid allocation admitted") + a, _, _, _ = allocation(1, 1, 1) + lam, eps = power(1), power(a) + loose_opposite_error = lam * eps + recovery = 1 << (2 + 4 + 3) + require(loose_opposite_error * recovery == F(1, 2), "opposite-loosening counterexample") + require(loose_opposite_error > lam**3 * eps, "counterexample violates retained opposite budget") + count += 1 + ideal_channel = lam**3 / 16 + require(ideal_channel * (1 << 9) == 4, "three-normalizer recovery control") + require(ideal_channel * (1 << 6) == F(1, 2), "omitted-normalizer control") + count += 1 + return count + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write generated JSON outside the package") + args = parser.parse_args() + package = Path(__file__).resolve().parent + if args.receipt is not None: + require(not args.receipt.resolve().is_relative_to(package), "receipt must remain outside package") + counts = {"budget_cases": budget_cases(), "convolution_fixtures": fixture_cases(), + "abstract_envelope_equalities": sharp_envelope_cases(), "controls": controls()} + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in files: + with (package / name).open("rb") as handle: + data = handle.read((1 << 20) + 1) + require(len(data) <= 1 << 20, "package file size limit") + hashes[name] = hashlib.sha256(data).hexdigest() + receipt = {"status": "PASS_ASYMMETRIC_GAUSSIAN_PRECISION", "counts": counts, + "python": sys.version.split()[0], "source_sha256": hashes, + "claim_type": "scoped written proof with finite exact corroboration"} + encoded = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + written = args.receipt.write_text(encoded) + require(written == len(encoded), "complete receipt write") + print(encoded, end="") + + +if __name__ == "__main__": + main()