Research: sharp inverse-square rounding bound for cyclic scans

research/cyclic-scan-sharp-bound/PROOF.md

@@ -0,0 +1,177 @@
+# A sharp stability-margin power for periodic scan rounding
+
+The two-pass periodic scan in [PR628](https://github.com/CrocSwap/integer-mult-bounds/pull/628)
+is sound under its stated hypotheses. Its proof gives the sufficient bound
+`6(B+1)u/beta^3` and requires `u <= beta^2/2`.
+Keeping a common geometric factor improves both conclusions.
+This result concerns that scan, including its varying-coefficient extension.
+It does not change the selected multiplication construction.
+
+## Statement
+
+Let `L >= 1`, `0 < beta <= 1`, and `B >= 0`.
+For every cyclic sequence of exact complex coefficients and inputs, assume
+
+```
+|b_i| <= 1-beta,       |x_i| <= B.
+```
+
+Choose either cyclic orientation. Compute the zero-seed pass, the running
+product, the closure division, and the second pass as in PR628.
+Each completed complex operation has absolute rounding error at most `u`.
+Assume `0 < u <= beta/2`. Then the rounded closure denominator is nonzero and
+
+```
+max_i |yhat_i - y_i| <= u (2B/beta^2 + 3/beta + 1)
+                     <= 4(B+1)u/beta^2,
+```
+
+where `y_i-b_i y_(i-d)=x_i` is the unique periodic solution.
+The bound is uniform in `L`, the orientation, and the coefficient pattern.
+Nearest rounding of both components on a grid of spacing `u` meets the
+operation-error hypothesis, since its complex error is at most `u/sqrt(2)`.
+Coefficients are exact; coefficient approximation requires a separate budget.
+
+## Proof
+
+Relabel the chosen traversal as `1,...,L`.
+Put `q_i=|b_i|`, `Q=product_i q_i`, and
+
+```
+G = sum_(j=1)^L product_(k=j+1)^L q_k.
+```
+
+An empty product is one. The exact affine return map is `s -> z+c*s`,
+where `c=product_i b_i` and `z` is the last zero-seed value.
+Thus the exact closure denominator is `d=1-c`.
+The following identity is the key estimate:
+
+```
+1-Q = sum_(j=1)^L (1-q_j) product_(k=j+1)^L q_k >= beta*G.
+```
+
+Also `|d| >= 1-Q > 0`. Both rounded first-pass recurrences multiply
+their previous errors by `b_i` and add one error of modulus at most `u`.
+Consequently
+
+```
+|zhat-z| <= u*G,       |chat-c| <= u*G <= (u/beta)|d|.
+```
+
+With `dhat=1-chat`, the hypothesis `u <= beta/2` gives
+`|dhat| >= |d|/2`. Computing `1-chat` is exact on the dyadic grid.
+This is the step that avoids bounding the numerator and denominator with
+two unrelated worst-case geometric sums.
+
+The cyclic weighted shift has norm at most `1-beta` in the maximum norm.
+Its Neumann inverse therefore has norm at most `1/beta`.
+In particular, the exact periodic seed `s=z/d` satisfies `|s| <= B/beta`.
+Before rounding the closure division,
+
+```
+|zhat/dhat-s|
+  <= (|zhat-z| + |s| |dhat-d|)/|dhat|
+  <= 2u/beta + 2B*u/beta^2.
+```
+
+Division rounding adds at most `u`.
+At each output, the second pass attenuates the seed error by a factor at
+most one and contributes at most `u/beta` from its own rounding errors.
+This proves the first bound. The second follows from `beta <= 1`:
+
+```
+2B/beta^2 + 3/beta + 1 <= (2B+4)/beta^2 <= 4(B+1)/beta^2.
+```
+
+All statements include `L=1` and zero coefficients. No diagonalization,
+probabilistic rounding assumption, or limit in `L` enters the proof.
+
+## The inverse-square dependence is necessary for this algorithm
+
+For every integer `k >= 2`, take a real one-entry input with
+
+```
+L=1, x=1, u=2^(-3k), a=2^(-k), beta=a+u/2, b=1-beta.
+```
+
+Use the implemented nearest rule, with ties toward positive infinity.
+All inputs and coefficients are exact dyadics. The working grid is `u`.
+The first-pass value is exactly one. Rounding the product `b*1` gives
+`chat=1-a`, because `b` is exactly halfway between adjacent grid points.
+The closure seed is exactly `1/a=2^k`.
+The second-pass value is also exactly on the grid:
+
+```
+yhat = 1+b/a = 2^k-2^(k-1)u,       y = 1/beta.
+yhat-y = b*u/(2*a*beta) >= u/(4*beta^2).
+```
+
+The inequality uses `a <= beta` and `b >= 1/2`.
+Moreover `u <= beta^2/2`, so every example satisfies even PR628's older
+precision admission. As `k` increases, `beta` tends to zero.
+For any `q < 2`, no constant independent of `beta` can replace the error
+bound by `C*u/beta^q` for this algorithm, even with `B=1` and `L=1`.
+This is not a lower bound for other periodic solvers or a claim about an
+optimally rounded exact closure product.
+
+## Consequence for the existing factor cascade
+
+Retain PR628's hypotheses and its exact certified factors.
+An outer scalar or inner unit phase contributes at most one extra rounding
+error `u` and has modulus at most one.
+Thus each factor has error at most `5(B+1)u/beta^2`.
+Put `n=r-1`, as in PR628. The unchanged exact prefix norm is bounded by
+`r*beta^(-j)` after `j` factors. If `E_j` is the accumulated error, then
+
+```
+E_j <= E_(j-1)/beta
+       + 5(r*beta^(-(j-1)) + E_(j-1) + 1)u/beta^2.
+T_j = beta^j E_j
+    <= (1+5u/beta)T_(j-1) + 5(r+1)u/beta.
+```
+
+For `u <= beta/(10n)`, the growth factor over `n` stages is at most
+`(1+1/(2n))^n < 2`.
+One elementary proof expands the binomial and bounds the degree-`j`
+coefficient by `1/(2^j j!)`; the finite sum is strictly below
+`sum_(j>=0) 2^(-j)=2`.
+It follows that
+
+```
+E_n <= 10n(r+1)u*beta^(-(n+1)).
+```
+
+For `beta=2^-g`, the following sufficient fractional precision replaces
+the execution budget in PR628's PROOF.md:
+
+```
+w_new = max(g + ceil(log2(10n)),
+            p + (n+1)g + ceil(log2(20n(r+1)))).
+```
+
+It ensures `E_n <= 2^(-p-1)`. All coefficient, root, phase-oracle and
+inverse-perturbation budgets stay as stated in PR628.
+The original execution budget is
+
+```
+w_old = max(2g + ceil(log2(14n)),
+            p + (n+2)g + ceil(log2(28n(r+1)))).
+```
+
+Both new terms are at most their old counterparts minus `g`.
+Thus `w_new <= w_old-g`. This is a proved saving in a sufficient
+execution-grid budget. It is not a measured speedup or a change to the
+`O(p+r^4)` asymptotic precision and preparation bound.
+The factor-cascade consequence inherits PR628's exact-factor and phase
+assumptions; this package does not independently validate its factorizer.
+
+## Attribution and status
+
+PR628 by Chafik Boukhalfa supplies the algorithm, the original rounding
+argument, its varying-phase extension, and the surrounding factor cascade.
+Periodic affine closure and geometric error bounds are standard methods.
+This note adds the shared-factor bound, the sharp family for this algorithm,
+and the consequent execution guard. No literature-priority claim is made.
+Prepared for Charles Bethin with substantial OpenAI Codex assistance.
+No human peer review or proof-assistant verification is claimed.
+New material uses Apache-2.0. Vendored notices remain intact.

research/cyclic-scan-sharp-bound/README.md

@@ -0,0 +1,97 @@
+# Sharp rounding bounds for cyclic scans
+
+**Mathematical refinement, no new kappa.** The clean two-pass periodic scan
+from [PR628](https://github.com/CrocSwap/integer-mult-bounds/pull/628) has
+length-independent error at most `4(B+1)u/beta^2`, under `u <= beta/2`.
+The existing sufficient bound is `6(B+1)u/beta^3`, under `u <= beta^2/2`.
+Here `u` is the working grid spacing, `B` bounds the input magnitude,
+and all exact complex coefficients have modulus at most `1-beta`.
+
+[PROOF.md](PROOF.md) proves the result for every cycle length, either
+orientation, and arbitrary varying coefficients within the margin.
+A one-entry dyadic family has error at least `u/(4*beta^2)` for the same
+algorithm and rounding rule. Thus the inverse-square margin dependence is
+necessary for a uniform bound on this algorithm.
+
+The proof also lowers PR628's sufficient factor-cascade execution precision
+by at least `g` bits when `beta=2^-g`. It preserves the coefficient and
+phase-preparation assumptions. The asymptotic `O(p+r^4)` precision bound
+stays the same. No runtime improvement, factorization implementation,
+supplier admission, selected frontier change, or full multiplication proof
+follows. This package proposes a guard refinement; it does not activate it
+inside PR628 or modify that contribution's files.
+
+## Reproduce
+
+From any working directory, run with Python 3.11 or later:
+
+```sh
+python3 -B /path/to/repository/research/cyclic-scan-sharp-bound/verify.py
+```
+
+Expected status: `PASS_SHARP_CYCLIC_SCAN_BOUND`.
+The command checks source hashes and compares its full result with
+[EXPECTED.json](EXPECTED.json). It uses only the standard library.
+To preserve a fresh receipt, use `--write /absolute/new/result.json`.
+The output path must not exist. The default command never overwrites evidence.
+
+## Evidence and independence
+
+- 5,024 cases compare the rounded output with an independently evaluated
+  finite geometric inverse. This oracle evaluates each matrix row directly.
+- 24 longer cases, through length 2,048, use exact residual certificates.
+  Dividing the residual norm by `beta` bounds the forward error.
+- 3,362 cases match PR628's unchanged varying-coefficient scan exactly.
+  Of these, 482 also match its unchanged constant-coefficient scan.
+- 1,686 cases meet the new guard but lie outside the original admission.
+  The new integer-grid implementation executes these cases.
+- 64 exact members of the sharp family match the symbolic output and error
+  formulas in the original scan and the integer-grid implementation.
+- 384 exact cascade recurrences and 276 inherited-budget comparisons check
+  the precision formulas. The written inequalities establish their scope.
+- Seven controls reject missing closure, wrong denominator sign, substituted
+  coefficients, wrong orientation, unstable coefficients, insufficient
+  admitted precision, and a false inverse-linear margin bound.
+
+The original-scan comparisons establish implementation agreement, not
+independent validation of a shared traversal. The direct finite inverse,
+residual certificates, and symbolic one-entry family provide separate
+mathematical checks. None of these finite checks proves the all-length
+theorem by enumeration. There is no independent human or formal review.
+
+The exhaustive domain uses lengths 1–3, all real coefficient sequences over
+`{-1/2,0,1/2}`, all inputs over `{-1,0,1}`, both orientations, and three grids.
+Additional complex cases use the recorded seed 68 and exact rational unit
+directions. Long cases use two margins, two grids, and both orientations.
+These are fixed validation domains, not an optimization search.
+
+## Sources and scope
+
+[SOURCE.json](SOURCE.json) pins PR628 at
+`0768f97d06c623b8211e651543c66135796b62bf`, with construction base
+`66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+The vendored files match that Git source byte for byte.
+`verify.py` executes the unchanged `scan` function AST from `weighted.py`
+with its original arithmetic module. It does not execute the unrelated
+kernel factorization imports or claim their validation.
+The vendored weighted file is an archival source, not a standalone command
+inside this reduced package.
+
+PR663's nonlinear restoration audit and PR673's dirty-echo construction and
+alias repair address separate questions. Their results are not dependencies
+of this clean-array rounding theorem. Existing dirty restoration, arbitrary
+stride routing, factor preparation, and full-transform obligations remain.
+
+Joshua Snider's [PR692](https://github.com/CrocSwap/integer-mult-bounds/pull/692),
+at `c5b53a5e80372a1fae9830d8dcf21aaabce3f729`, already uses the standard finite
+geometric inverse to audit weighted stride cycles and their bilinear dual.
+This package does not claim that oracle identity or method as new.
+Its distinct result is the uniform sharp rounding bound and execution guard.
+The oracle here was written independently; no PR692 code is consumed.
+
+Chafik Boukhalfa's PR628 supplies the scan and its prior proof.
+Its predecessor attribution is preserved in [vendor/NOTICE.md](vendor/NOTICE.md).
+The shared-factor estimate, matching family, guard derivation, and new
+validation code were prepared for Charles Bethin with substantial OpenAI
+Codex assistance. No literature-priority claim is made.
+New material is Apache-2.0, under the repository license.

research/cyclic-scan-sharp-bound/SOURCE.json

@@ -0,0 +1,29 @@
+{
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "pr": 628,
+  "head": "0768f97d06c623b8211e651543c66135796b62bf",
+  "vendor": {
+    "vendor/NOTICE.md": {
+      "source_path": "research/prime-power-cyclic-scan/NOTICE.md",
+      "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68"
+    },
+    "vendor/check_budgets.py": {
+      "source_path": "research/prime-power-cyclic-scan/check_budgets.py",
+      "sha256": "581ba58a30e05cb09dadb35be6e25bd92232b2137a0cc7eb5b83e2ee20c0bf02"
+    },
+    "vendor/scan.py": {
+      "source_path": "research/prime-power-cyclic-scan/scan.py",
+      "sha256": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e"
+    },
+    "vendor/weighted.py": {
+      "source_path": "research/prime-power-cyclic-scan/weighted.py",
+      "sha256": "8b0f93d131a30e64eb0ccd893779daffea79c0c00f1d2a30a91d23eb2bf0bff5"
+    }
+  },
+  "proof_sources": {
+    "research/prime-power-cyclic-scan/PROOF.md": "595893609764c64a90d9b21b9cbd6d9e61980703f3deb43361105cf8c3d1d093",
+    "research/prime-power-cyclic-scan/SCAN-PROOF.md": "6be99f0dce58d82ecb07967664e4a23f202ae3858f124a1bdcdcac3e660548db",
+    "research/prime-power-cyclic-scan/WEIGHTED-PROOF.md": "b0643ad6ae448ca2fe11ee9a9597b5656e5e2feaaa89b16939e1d1bc7ba7437d"
+  },
+  "seed": 68
+}