Prove sharp quadratic rounding guards for closed words (no new κ)

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.

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.

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"
+    }
+  ]
+}