diff --git a/research/closed-word-rounding-guard/PROOF.md b/research/closed-word-rounding-guard/PROOF.md new file mode 100644 index 0000000000..e45deaa5d6 --- /dev/null +++ b/research/closed-word-rounding-guard/PROOF.md @@ -0,0 +1,173 @@ +# Endpoint-conditioned simultaneous rounding + +## Statement + +Let `A_1,...,A_K` be invertible matrices over the real or complex numbers, +in execution order. Use any induced matrix norm and its compatible vector norm. +Set `F_0=I` and `F_j=A_j...A_1`. Assume + +``` +max_{0<=j<=K} max(||F_j||, ||F_j^-1||) <= B, B>=1. +``` + +Let `C>=1` be a separate upper bound for `||F_K||`. For perturbations +`Delta_j`, define + +``` +D_j = F_j^-1 Delta_j F_(j-1), +rho = sum_j ||D_j|| < 1, +U = sum_j ||u_j||. +``` + +The actual trajectory obeys +`y_j=(A_j+Delta_j)y_(j-1)+u_j`, with `||y_0||<=M`. Then + +``` +||y_K-F_K y_0|| <= C (rho M + B U)/(1-rho). (1) +``` + +In particular, the coefficient-only operator defect is at most +`C rho/(1-rho)`. For two-wire gates with `||Delta_j||<=2 eta`, +`||u_j||<=2 eta`, `M<=1`, and target `p>=0`, the sufficient guard is + +``` +P = p + ceil(log2(8 K C B^2)), eta=2^-P. (2) +``` + +This improves the generic `8 K B^3` prescription of ywz65's PR2701 whenever +the endpoint has a smaller certified norm. For `F_K=I`, or a unitary endpoint +in Euclidean norm, one may take `C=1`. The exponent of `B` drops from three +to two. This controls the final output; intermediate outputs still use their +own endpoint norms and need not admit the same reduction. + +## Proof of the upper bound + +Set `z_j=F_j^-1 y_j`. Keeping the multiplication order gives + +``` +z_j=(I+D_j)z_(j-1)+F_j^-1 u_j. +``` + +Every consecutive interaction product has norm at most +`product_i(1+||D_i||) <= 1/(1-rho)`. To see the second inequality, expand +the finite product in elementary symmetric sums. Its degree-r sum is at +most `rho^r`; summing the geometric series gives the bound. Removing the +constant term bounds the full product's difference from `I` by +`rho/(1-rho)`. Each forcing term has norm at most `B||u_j||`, and all +later interaction products satisfy the same bound. Thus + +``` +||z_K-y_0|| <= (rho M+B U)/(1-rho). +``` + +Multiplying by the final `F_K` uses `C`, rather than the largest norm of +any intermediate prefix. This proves (1). This is the same standard +interaction-coordinate argument credited to PR2701, with its endpoint +factor retained separately; no new general perturbation method is claimed. + +For (2), `rho<=2 K B^2 eta<=1/4`, and `U<=2K eta`. Therefore + +``` +||y_K-F_K y_0|| + <= (8/3) K C (B^2+B) eta + <= (16/3) K C B^2 eta + <= (2/3) 2^-p + <= 2^-p. +``` + +The local bounds `2 eta` follow, for example, from the Frobenius estimate +for two complex entry errors per row and from two coordinate arithmetic +errors of magnitude at most `eta`. A production arithmetic kernel must +supply those bounds; the theorem does not implement it. + +## Matching elementary words + +The following all-size construction shows that the improved quadratic +dependence cannot be replaced by a smaller power in this error model. +It also shows that the original cubic dependence is necessary when the +endpoint norm is allowed to grow with `B`. + +Use the induced infinity norm. For integers `q,L>=1`, put + +``` +b=2^q, T=diag(2,1/2), D=T^q, +S(t)=I+t E_21, S_+=S(1/2), S_-=S(-1/2). +``` + +Execute `q` copies of `T`, then `L` pairs `S_+,S_-`, then `q` copies of +`T^-1`. The exact endpoint is `I`. Every exact prefix and its inverse has +norm at most + +``` +B_* = 3b/2. (3) +``` + +This is the exact maximum. During the scale runs the prefixes are diagonal +with entries between `1/b` and `b`. During the shear pairs they are `D` or + +``` +S(1/2)D = [[b,0],[b/2,1/b]], +[S(1/2)D]^-1 = [[1/b,0],[-b/2,b]]. +``` + +The latter inverse has row sum `3b/2`; all other row sums are no larger +because `b>=2`. Every exact gate and its inverse has norm at most two. +All exact gates have determinant one and dyadic entries. + +Perturb each of the `2L` active shear coefficients by the same positive +dyadic `eta<=1/4`, leaving all scale gates exact. These are errors in the +already nonzero coefficients, each of norm `eta`. The perturbed gates +also have determinant one and norm at most two. The shear identity +`S(s)S(t)=S(s+t)` gives, with no discarded higher-order terms, + +``` +Q_closed = D^-1 S(2L eta) D + = I + 2L b^2 eta E_21. (4) +``` + +Hence unit input `e_1` has exact endpoint error `2L b^2 eta`. The +interaction matrices are all `b^2 eta E_21` at the perturbed sites, so +`rho=2L b^2 eta`. This identity holds at every positive dyadic `eta`; +choosing a smaller one enforces any prescribed small-radius premise. + +For the unrestricted-endpoint version, execute `2q` copies of `T^-1` +after the shear pairs. The exact endpoint is `D^-1`, whose norm is `b`; +the exact common prefix bound is still (3). Now + +``` +Q_open = D^-2 S(2L eta) D + = D^-1 + 2L b^3 eta E_21. (5) +``` + +All gates retain the same norm and determinant bounds. Thus the additional +factor of the endpoint norm is necessary, even for elementary two-wire +words with uniformly bounded exact gates and inverses. + +To compare powers including the gate count, take `L=q` and +`eta=2^(-4q-12)`. Then `K_closed=4q`, `K_open=5q`, and `rho<1/4` for +every `q>=1`. For every fixed `alpha<2`, the ratio of (4)'s error to +`K_closed B_*^alpha eta` grows without bound as `q` grows. Likewise for +every `alpha<3`, the ratio of (5)'s error to +`K_open B_*^alpha eta` grows without bound. Consequently no uniform +constant can replace the quadratic closed-word or cubic unrestricted +power by a smaller one under only these hypotheses. Optimal numerical +constants are not asserted. + +The perturbations are admissible bounded coefficient errors. This does not +say that a particular deterministic nearest-rounding rule creates these +errors on these dyadic coefficients. Exploiting such a rule's additional +structure would change the model and is left open. + +## Verification boundary + +The formulas above prove the all-size claims. Exact finite matrix products +corroborate them, including both independent input columns, every intermediate +prefix, inverse prefixes, simultaneous noncommuting perturbations and +arithmetic forcing. A two-by-two matrix of forcing terms records the two +individual column trajectories in the finite checks. It is not a model of +independent random errors. The replay uses rational infinity norms; it does +not measure Euclidean norms of a production complex compiler. + +No production caller, reversible rounded instruction sequence, integer-bit +budget, overflow proof, physical tariff, supplier admission, complete +multiplication theorem or new kappa follows from this result alone. diff --git a/research/closed-word-rounding-guard/README.md b/research/closed-word-rounding-guard/README.md new file mode 100644 index 0000000000..5d9bf414ac --- /dev/null +++ b/research/closed-word-rounding-guard/README.md @@ -0,0 +1,117 @@ +# A sharp quadratic rounding guard for closed words + +This contribution was produced by Nick Petalas. Claim type: scoped mathematical +proof with exact finite corroboration. No new kappa is claimed. + +The generic simultaneous-rounding prescription in +[ywz65's PR2701](https://github.com/CrocSwap/integer-mult-bounds/pull/2701) +uses `p+ceil(log2(8 K B^3))` fractional bits, where `B` bounds every exact +prefix and its inverse. Retaining a separate endpoint norm `C>=1` gives + +``` +P = p + ceil(log2(8 K C B^2)). +``` + +For an exact closed word, `C=1` and the sufficient power falls from `B^3` +to `B^2`. For dyadic `B=2^q`, this saves exactly `q` fractional bits in +the displayed guard. The required endpoint and prefix certificates remain +hypotheses. This is an improvement to the final-output bound, not a smaller +uniform bound for every intermediate state. + +The [proof](PROOF.md) gives the full trajectory estimate + +``` +||y_K-F_K y_0|| <= C (rho M+B sum_j ||u_j||)/(1-rho), +rho=sum_j ||F_j^-1 Delta_j F_(j-1)|| < 1. +``` + +It also gives matching all-size elementary words. With `b=2^q`, `L` +opposite shear pairs, and common prefix/inverse maximum `B_*=3b/2`, their +exact errors are `2L b^2 eta` at a closed endpoint and `2L b^3 eta` at an +endpoint of norm `b`. Every exact gate and inverse has norm at most two; +every exact and perturbed gate has determinant one. Taking `L=q` proves +that the respective quadratic and cubic powers cannot be lowered, including +the gate-count factor, in the stated bounded coefficient-error model. +Optimal numerical constants are not claimed. + +## Evidence and reproduction + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/closed-word-rounding-guard/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/closed-word-rounding-guard +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/closed-word-rounding-guard --check-source-history +``` + +The interpreter path is the local reproduction environment. On another machine, +substitute a CPython 3.12 interpreter. `VERIFY.json` registers warning-strict +normal and optimized runs. Every mathematical check uses explicit branches and +remains active under `-O`. The verifier writes no files. `--emit` prints a +computed receipt bound to the package file hashes; redirect it outside the +checkout if desired. + +Exact rational checks multiply the two independent input columns directly and +also use a separate interaction recurrence. They check the sharp identities, +literal prefix/inverse envelopes, bounded gates and determinant preservation. +The simultaneous guard checks add a noncommuting detour and perturb every +gate while injecting arithmetic errors. Controls reject a smaller power, +an endpoint-only premise, singular matrices, malformed/capped requests and +an exhausted small-error premise. The printed counts are finite corroboration; +the written proof supplies all-size coverage. + +The checker caps a trajectory at 256 two-by-two gates, an excursion at +`q<=16,L<=32`, and the guard search at 128 candidates. Its fixed finite +calibrations use smaller limits. Functions fit within 60 physical lines. +Rational arithmetic uses managed allocation rather than preallocated storage; +the fixed matrices and bounded loops constrain the live data. Five fixed +rejection callbacks are a test-only indirect-call exception. Warning-strict +normal and optimized execution supply the available interpreter diagnostics. + +## Scope and limitations + +The lower examples describe admissible bounded coefficient perturbations, +including errors in nonzero dyadic shear coefficients. They do not assert that +nearest rounding on those coefficients generates those errors. A specified +rounding rule could impose additional restrictions. + +This package does not bind a production emitted caller, implement reversible +rounded arithmetic, certify integer bits or overflow, price physical movement, +admit a supplier, or prove the complete multiplication theorem. No selected +cold replay, native replay, Lean or Docker build is required or claimed. +Independent human and formal proof-kernel review are unclaimed. + +The card `formal-interface-lemma` is changed to this original written +precision-interface result. The selected source-binding positive control was +run before the algebraic work; its metadata check is not an operator replay. +The first proved improvement ends this investigation. + +## Sources and overlap + +Credit ywz65's PR2701 for the simultaneous interaction-coordinate theorem and +the original `8 K B^3` guard, and Vlado Vojdanovski's PR1673 for its capped +Toeplitz precision interface and retained predecessor lineage. Standard +product perturbation mathematics is not claimed as new. The contribution is +the endpoint-conditioned guard and the matching bounded elementary-word +obstruction. No predecessor executable is imported or rerun as the result. +The source README is pinned by Git blob and SHA256 in `SOURCES.json`. + +The base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7. +Before the claim, the overlap helper covered 306 open PRs and 4,307 Discussion +records with complete remote pagination. The local sparse note scan covered +154 of 6,918 HEAD note paths; all-main distinctive-term searches supplemented +it. Live recent account work, handoffs, active Discussions and merged PRs were +also checked. These checks do not cover unpublished work or arbitrary diffs. + +## Open next questions + +1. Which production caller has a certified endpoint norm `C` much smaller + than its prefix bound `B`? Pin one emitted word and prove its endpoint + norm before applying the guard. A caller binding and arithmetic kernel + remain missing. +2. Can a specified deterministic rounding rule improve the guard further? + Start by identifying which correlated shear errors that rule can realize. + The present arbitrary bounded-error model does not answer that question. + +Structured versions, including relevance and blockers, are in `TASK.json`. +Apache-2.0. diff --git a/research/closed-word-rounding-guard/SOURCES.json b/research/closed-word-rounding-guard/SOURCES.json new file mode 100644 index 0000000000..b8340c4234 --- /dev/null +++ b/research/closed-word-rounding-guard/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/simultaneous-gate-rounding/README.md", + "usage": "input", + "git_blob": "eaad013627f7ded744f032eea77fed6f121fc01c", + "sha256": "4bd564aa762f07d67127cba668b370bab3c1407c733f873c756cf2f62e906f2a" + } + ] +} diff --git a/research/closed-word-rounding-guard/TASK.json b/research/closed-word-rounding-guard/TASK.json new file mode 100644 index 0000000000..600acb4b69 --- /dev/null +++ b/research/closed-word-rounding-guard/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Endpoint-conditioned simultaneous rounding guard with matching closed and unrestricted dyadic-word amplification examples.", + "scope_change_reason": "The original formal-interface card is changed to a written precision-interface theorem extending PR2701; no proof-assistant build or predecessor audit is the deliverable.", + "bottleneck_link": "A smaller final-output guard can reduce fractional precision for a caller with a certified small exact endpoint norm. This is a local interface result; no concrete selected caller is admitted.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved endpoint guard improvement and its matching power obstruction; do not extend into production caller synthesis.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal theorem and sharpness construction; verify.py checks literal exact products, simultaneous-error guards and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which emitted production caller has a certified endpoint norm C much smaller than its common prefix bound B?", + "why_it_matters": "It determines whether the saved guard bits apply to actual retained work.", + "first_step": "Pin one emitted word, compute or prove its endpoint norm and existing prefix envelope, then instantiate formula (2).", + "blocked_by": "No actual caller or arithmetic kernel is bound by this package." + }, + { + "question": "Can the guard improve further for a specified deterministic rounding rule?", + "why_it_matters": "The lower examples use admissible bounded perturbations rather than a particular rounding policy.", + "first_step": "State the coefficient and arithmetic rounding policy, then determine which correlated shear errors are realizable.", + "blocked_by": "The present contract allows arbitrary bounded coefficient perturbations." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/closed-word-rounding-guard/VERIFY.json b/research/closed-word-rounding-guard/VERIFY.json new file mode 100644 index 0000000000..cd59edd5a8 --- /dev/null +++ b/research/closed-word-rounding-guard/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/simultaneous-gate-rounding/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact closed/open shear excursion identities, prefix envelopes, endpoint guards with simultaneous forcing, and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same mathematical checks with Python assertions disabled; all requirements use explicit checked branches." + } + ] +} diff --git a/research/closed-word-rounding-guard/verify.py b/research/closed-word-rounding-guard/verify.py new file mode 100644 index 0000000000..b344c111c4 --- /dev/null +++ b/research/closed-word-rounding-guard/verify.py @@ -0,0 +1,216 @@ +"""Exact bounded corroboration for the endpoint-conditioned error theorem.""" + +from __future__ import annotations + +import argparse +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path + + +Matrix = tuple[tuple[F, F], tuple[F, F]] +I: Matrix = ((F(1), F(0)), (F(0), F(1))) +ZERO: Matrix = ((F(0), F(0)), (F(0), F(0))) + + +def need(ok: bool, message: str) -> None: + if not ok: + raise ValueError(message) + + +def mul(a: Matrix, b: Matrix) -> Matrix: + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + + +def add(a: Matrix, b: Matrix) -> Matrix: + return tuple(tuple(a[i][j] + b[i][j] for j in range(2)) + for i in range(2)) + + +def sub(a: Matrix, b: Matrix) -> Matrix: + return tuple(tuple(a[i][j] - b[i][j] for j in range(2)) + for i in range(2)) + + +def inv(a: Matrix) -> Matrix: + det = a[0][0] * a[1][1] - a[0][1] * a[1][0] + need(det != 0, "singular matrix") + return ((a[1][1] / det, -a[0][1] / det), + (-a[1][0] / det, a[0][0] / det)) + + +def norm(a: Matrix) -> F: + return max(sum(abs(x) for x in row) for row in a) + + +def shear(t: F) -> Matrix: + return ((F(1), F(0)), (t, F(1))) + + +def scale(t: F) -> Matrix: + need(t > 0, "scale must be positive") + return ((t, F(0)), (F(0), 1 / t)) + + +def trajectory(gates: list[Matrix], errors: list[Matrix], noise: list[Matrix]): + """Propagate both input columns and their additive forcing together.""" + need(1 <= len(gates) <= 256, "gate count outside bounded replay") + need(len(gates) == len(errors) == len(noise), "unaligned trajectory") + exact, rounded, forced, interaction, forcing = I, I, I, I, ZERO + radius, envelope = F(0), F(1) + for a, error, u in zip(gates, errors, noise, strict=True): + previous = exact + exact = mul(a, previous) + rounded = mul(add(a, error), rounded) + forced = add(mul(add(a, error), forced), u) + d = mul(mul(inv(exact), error), previous) + interaction = mul(add(I, d), interaction) + forcing = add(mul(add(I, d), forcing), mul(inv(exact), u)) + radius += norm(d) + envelope = max(envelope, norm(exact), norm(inv(exact))) + need(rounded == mul(exact, interaction), "interaction order/index") + need(forced == mul(exact, add(interaction, forcing)), "forcing order") + return exact, rounded, forced, radius, envelope + + +def check_bound(gates, errors, noise) -> tuple[F, F, F]: + exact, rounded, forced, rho, b = trajectory(gates, errors, noise) + need(rho < 1, "small interaction budget required") + c = norm(exact) + budget = c * (rho + b * sum(norm(u) for u in noise)) / (1 - rho) + need(norm(sub(forced, exact)) <= budget, "endpoint trajectory bound") + need(norm(sub(rounded, exact)) <= c * rho / (1 - rho), + "endpoint coefficient bound") + return rho, b, c + + +def excursion(q: int, pairs: int, closed: bool, eta: F): + need(1 <= q <= 16 and 1 <= pairs <= 32, "excursion outside replay caps") + need(type(closed) is bool and 0 < eta <= F(1, 4), "bad excursion data") + up, down = scale(F(2)), scale(F(1, 2)) + gates = [up] * q + [shear(F(1, 2)), shear(F(-1, 2))] * pairs + gates += [down] * (q if closed else 2 * q) + error = sub(shear(eta), I) + errors = [ZERO] * q + [error] * (2 * pairs) + errors += [ZERO] * (q if closed else 2 * q) + return gates, errors + + +def check_excursions() -> dict: + cases = prefixes = sharp_controls = 0 + for q in range(1, 13): + b = F(2**q) + for pairs in (1, q, 16): + for closed in (True, False): + eta = F(1, 2 ** (4 * q + 12)) + gates, errors = excursion(q, pairs, closed, eta) + exact, rounded, _, rho, envelope = trajectory( + gates, errors, [ZERO] * len(gates)) + c = F(1) if closed else b + expected = I if closed else scale(1 / b) + defect = ((F(0), F(0)), (2 * pairs * b**2 * c * eta, F(0))) + need(exact == expected, "exact endpoint") + need(sub(rounded, exact) == defect, "sharp defect identity") + need(rho == 2 * pairs * b**2 * eta, "exact interaction radius") + need(envelope == 3 * b / 2, "exact prefix envelope") + need(max(norm(a) for a in gates) <= 2, "bounded exact gates") + need(max(norm(inv(a)) for a in gates) <= 2, "bounded inverses") + for a, e in zip(gates, errors, strict=True): + r = add(a, e) + need(r[0][0] * r[1][1] - r[0][1] * r[1][0] == 1, + "rounded shear determinant") + check_bound(gates, errors, [ZERO] * len(gates)) + if q >= 4 and pairs == q: + need(norm(defect) > len(gates) * envelope * c * eta, + "quadratic power cannot be replaced by linear") + sharp_controls += 1 + cases += 1 + prefixes += len(gates) + return {"sharp_families": cases, "literal_prefixes": prefixes, + "lower_power_rejections": sharp_controls} + + +def check_guard() -> dict: + cases = 0 + noncommuting = [shear(F(1, 2)), ((F(1), F(1, 2)), (F(0), F(1)))] + for q in range(1, 7): + gates, _ = excursion(q, q, True, F(1, 16)) + gates[q:q] = noncommuting + [inv(a) for a in reversed(noncommuting)] + _, _, _, _, b = trajectory(gates, [ZERO] * len(gates), [ZERO] * len(gates)) + for p in (0, 1, 8, 32): + k = len(gates) + guard = 0 + for exponent in range(128): + if 2**exponent >= 8 * k * b**2: + guard = exponent + break + need(guard > 0, "guard search exhausted") + eta = F(1, 2 ** (p + guard)) + errors = [((eta, -eta), (eta, eta))] * k + noise = [((eta, F(0)), (-eta, F(0)))] * k + rho, _, c = check_bound(gates, errors, noise) + exact, _, forced, _, _ = trajectory(gates, errors, noise) + need(c == 1 and rho <= F(1, 4), "closed guard prerequisites") + need(norm(sub(forced, exact)) <= F(1, 2**p), "precision target") + cases += 1 + return {"simultaneous_guard_cases": cases} + + +def check_controls() -> dict: + rejected = 0 + for operation in ( + lambda: inv(ZERO), + lambda: excursion(0, 1, True, F(1, 8)), + lambda: excursion(1, 33, True, F(1, 8)), + lambda: trajectory([I], [], [ZERO]), + lambda: check_bound([I], [sub(shear(F(1)), I)], [ZERO]), + ): + try: + operation() + except ValueError: + rejected += 1 + else: + raise ValueError("invalid input accepted") + gates, errors = excursion(2, 2, True, F(1, 2**12)) + exact, rounded, _, _, _ = trajectory(gates, errors, [ZERO] * len(gates)) + need(norm(sub(rounded, exact)) > sum(norm(e) for e in errors), + "endpoint-only premise control") + for q in range(1, 7): + b = F(2**q) + a = scale(1 / b**2) + delta = ((-1 / b**2, F(0)), (F(0), F(0))) + try: + inv(add(a, delta)) + except ValueError: + rejected += 1 + else: + raise ValueError("singular perturbation accepted") + return {"invalid_input_rejections": rejected, "endpoint_only_rejections": 1} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print generated receipt") + args = parser.parse_args() + package = Path(__file__).resolve().parent + source = package.parents[1] / "research/simultaneous-gate-rounding/README.md" + pins = json.loads((package / "SOURCES.json").read_text()) + pin = next(row for row in pins["files"] if row["usage"] == "input") + need(hashlib.sha256(source.read_bytes()).hexdigest() == pin["sha256"], + "predecessor source bytes differ") + result = {"status": "PASS_CLOSED_WORD_ROUNDING_GUARD", "claim_type": "scoped proof"} + result.update(check_excursions()) + result.update(check_guard()) + result.update(check_controls()) + if args.emit: + result["files_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + } + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()