Prove sharp Walsh rounding error with one interleaved integer shear (No new κ)

research/walsh-interleaved-shear/PROOF.md

@@ -0,0 +1,180 @@
+# A sharp error bound for one interleaved integer shear
+
+Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Exact statement and conventions
+
+Let h > 0, m be any integer, and t,s be distinct elements of {0,1,2,3}.
+Let R round a real number to its nearest integer, with ties to the even integer,
+and apply it componentwise. Coordinates are numbered by their binary indices.
+Define the two **normalized** real Walsh factors
+
+```
+A = (1/2) [[1, 1, 0, 0],       B = (1/2) [[1, 0, 1, 0],
+           [1,-1, 0, 0],                  [0, 1, 0, 1],
+           [0, 0, 1, 1],                  [1, 0,-1, 0],
+           [0, 0, 1,-1]]                  [0, 1, 0,-1]].
+```
+
+Let S = I + m e_t e_s^T. In grid units the literal program is
+
+```
+y = R(Ax);  z = S y;  F_m(x) = R(Bz),       x in Z^4.
+```
+
+The shear is exact on this integer grid. Rounding after it would be the
+identity. Both values in each butterfly are read before either is written.
+The **exact comparison operator includes the same shear**: T_m = B S A.
+Then, for each of the twelve ordered pairs (t,s),
+
+```
+sup_(x in Z^4) ||F_m(x) - T_m x||_infinity = (|m|+3)/4.       (1)
+```
+
+For inputs on h Z, multiply the right side by h. Reversing the two axes
+preserves (1), by conjugating all coordinates and the shear by the permutation
+(1 2). Independent spectator fibers preserve the bound when the shear is
+within a fiber. Cross-fiber shears are not asserted here.
+
+For m=0, (1) recovers Nick Petalas's PR6129 value a_2=3/4. For every nonzero
+integer m, that unsheared value is exceeded. This answers the two-stage,
+integer-shear instance of Josie Elliston's explicit PR6140 open question.
+Neither predecessor claimed that its theorem covered interleaved gates.
+
+## Upper bound for all inputs and all integer coefficients
+
+Scale h to one. Put delta = y - Ax. Every component of Ax is a half integer,
+so each delta_i belongs to {-1/2,0,1/2}. A crucial implication is
+
+```
+delta_i != 0  =>  y_i is even.                            (2)
+```
+
+This is the nearest-even tie rule. Let eta = R(B S y) - B S y.
+Every component of S y is an integer, so eta_i is again 0 or +/-1/2.
+The error is exactly
+
+```
+F_m(x) - T_m x = B S delta + eta.                       (3)
+```
+
+An unaffected output combines the first errors of one second-stage pair
+with signs and a factor 1/2. If eta_i=0, its absolute error is at most 1/2.
+If eta_i!=0, the two stored inputs have odd sum/difference. They cannot both
+be even, so (2) implies that at least one of their first errors is zero.
+The error is then at most 1/4+1/2=3/4.
+
+For an affected output let p=t xor 2 be t's partner in B. Its propagated
+first error has the form
+
+```
+(alpha delta_t + beta delta_p + alpha m delta_s)/2,
+alpha,beta in {+1,-1}.
+```
+
+The two signs are the actual row signs of B; no independence of delta terms
+is assumed. The source may equal p, in which case terms refer to the same
+error and the triangle inequality remains valid.
+
+First suppose |m|>=1. If eta_i=0, the absolute total error is at most
+(|m|+2)/4, which is smaller than (1). If eta_i!=0, at least one of
+**delta_t, delta_p, delta_s is zero**. Otherwise (2) would make all of
+ y_t, y_p, y_s even; y_t+m y_s and y_p would be even, forcing eta_i=0.
+Removing any one of these three terms decreases the triangle bound by at
+least 1/2 before the outer division: its weight is either 1 or |m|>=1.
+Therefore
+
+```
+|error_i| <= (|m|+1)/4 + 1/2 = (|m|+3)/4.
+```
+
+If the same variable appears twice, its vanishing removes both terms and
+only strengthens this estimate. For m=0 there are just two relevant terms;
+the unaffected-output argument gives 3/4. This proves the upper bound
+without a bounded search, residue assumption or inherited Walsh recurrence.
+
+## Attainment by fixed small inputs
+
+[WITNESSES.json](WITNESSES.json) has two rows per (t,s), one for each
+c in {-1,+1}. A row records (t,s,c,j,x0,x1,x2,x3), with x in {-1,0,1}^4.
+Each row satisfies three exact identities:
+
+```
+(R(Ax))_s = 0,
+4(F_0(x)_j - (T_0 x)_j) = 3,
+4((T_0 - T_1)x)_j = c.                                (4)
+```
+
+Because the stored shear source is zero, **F_m(x)=F_0(x) for every m**.
+The exact operator is affine in m. Hence (4) proves the identity
+
+```
+4(F_m(x)_j - (T_m x)_j) = 3 + c m                    (all integer m).
+```
+
+For nonzero m choose c=sign(m); either sign works for m=0. This attains (1).
+The 24 finite identities in (4), combined with this algebraic argument,
+prove attainment for the unbounded coefficient domain. They are checked
+using explicit dense matrices and exact Fraction rounding, independently of
+the loop-based integer butterfly interpreter. The certificate is not a claim
+that a finite coefficient sweep alone proves (1).
+
+For example, take t=0, s=1, m=-1 and x=(0,-1,-1,-1). The first stored vector
+is (0,0,-1,0), so the shear leaves it unchanged and F_m(x)=(0,0,0,0).
+The exact output is (-1,1/4,0,1/4), giving error exactly 1. Removing the
+shear yields exact output (-3/4,1/4,1/4,1/4) and error 3/4.
+At h=1/4 the input is (0,-1/4,-1/4,-1/4), and the two sharp errors are
+1/4 and 3/16 respectively. This is a changed four-coordinate program;
+it is not a defect in CubeJerry's unchanged PR6119 surrogate.
+
+## Why the finite corroboration is complete in its stated domain
+
+Two elementary reductions make the secondary census meaningful:
+
+1. **Input period eight.** Replace x by x+8v with arbitrary integer v.
+   The first exact displacement 8Av has coordinates divisible by four.
+   Since R(u+2k)=R(u)+2k, the stored displacement is exactly 8Av.
+   The integer shear preserves divisibility by four. After B the displacement
+   has even coordinates, so the second rounding also commutes with it.
+   Thus F_m(x+8v)-T_m(x+8v)=F_m(x)-T_m x for every integer m.
+2. **Coefficient residues modulo four.** At fixed x, replace m=r by r+4q.
+   The pre-final-round displacement is 4q B e_t y_s, whose components are
+   even integers. The rounded output shifts by this exact displacement.
+   Consequently four-times the error in output j changes by 4q c_j, where
+   c_j = 4 B[j,t] delta_s is in {-1,0,1}. Thus it is an affine function
+   c_j m + a_j within each coefficient residue class.
+
+The verifier compares **both complete output vectors and the first stored
+vector** between its two engines for all 8^4 inputs, all twelve directed
+shears and r=0,1,2,3: 196,608 cases, 786,432 final coordinates. For each
+pair/residue and slope -1,0,+1, the intercept minimum and maximum are -3,+3.
+This independently corroborates the formula under the two proved reductions.
+It does not replace the universal upper-bound argument above.
+
+Large signed period/coefficient tests and the reverse-axis checks are finite
+controls. The unrestricted h and spectator statements follow by scaling and
+fiberwise application, not numerical testing of every grid or dimension.
+
+## Scope, inherited obligations and credit
+
+The theorem assumes real arithmetic, grid inputs, exactly two distinct axes,
+one integral off-diagonal shear, exact pre-rounding arithmetic, and sufficient
+range. It supplies no finite-width implementation, overflow bound, bit/tape
+cost, reversible history, clean-scratch service or accelerated recursive child.
+More stages, nonintegral shears, complex Gaussian mixing, multiple interleaved
+gates and cross-fiber shears need their own analysis.
+
+This is a source-context-bound mathematical side result. It does not discharge
+the selected PR6030 assumptions native_all_columns, owned_erasure, compiler,
+precision_tape or analytic_recovery, and gives **No new κ**. No selected cold
+replay, Lean kernel proof or independent human review is claimed.
+
+The pure-stage sharp bound and its proof are Nick Petalas's PR6129. The
+independent audit and interleaved-shear question are Josie Elliston's PR6140.
+The two-phase numerical surrogate is CubeJerry's PR6119; the deferred-row/H0
+context is Vlado Vojdanovski's PR1673, with the retained native/BIT/analytic
+lineage credited by those packages. The exact-history result PR5912 and
+Sricharan Vagvala's PR1631 shear-equivariance obstruction address different
+contracts: neither is a two-stage Walsh error classification. No predecessor
+code is imported or modified. The verbatim context documents retain their
+notices and exact source pins in SOURCES.json.

research/walsh-interleaved-shear/README.md

@@ -0,0 +1,173 @@
+# Sharp rounding error with one interleaved integer shear
+
+**Scoped theorem and independent verification. No new κ.**
+
+Inserting an exact grid-preserving addition between two rounded Walsh stages
+can invalidate the error guarantee for pure Walsh stages. For every integer
+coefficient `m` and all twelve directed off-diagonal shears on four coordinates,
+the exact worst-case sup-norm error is
+
+```
+h * (|m| + 3) / 4.
+```
+
+Here `h` is the grid spacing. Each stage is one distinct **normalized** real
+Walsh factor `H0=(1/2)[[1,1],[1,-1]]`, rounded to nearest with ties to even.
+The intervening operation is `y[target] += m*y[source]`. The exact comparison
+map contains **the same shear**. This is not an error comparison against a
+different, shear-free transform.
+
+The unsheared case is `3h/4`; even a unit shear increases the sharp error to
+`h`. For `m=-1`, target 0, source 1 and grid-unit input `(0,-1,-1,-1)`, the
+rounded output is zero while the exact output is `(-1,1/4,0,1/4)`.
+
+[PROOF.md](PROOF.md) gives the universal upper bound using nearest-even parity,
+then proves sharpness for all integer coefficients from 24 fixed small inputs
+in [WITNESSES.json](WITNESSES.json). The certificate rows are finite exact
+identities; their affine dependence on `m` proves attainment for the unbounded
+coefficient domain. No finite search is presented as a full theorem proof.
+
+## What is new
+
+Nick Petalas's [PR6129](https://github.com/CrocSwap/integer-mult-bounds/pull/6129)
+proves the sharp law for distinct pure Walsh stages and explicitly excludes
+intervening gates. Josie Elliston's
+[PR6140](https://github.com/CrocSwap/integer-mult-bounds/pull/6140) independently
+audits that law and asks whether it survives an intervening grid shear. This
+package answers the complete **two-stage, one-integer-shear** instance, using
+new implementations and a proof that does not assume the pure-stage recurrence.
+It finds no defect in either predecessor or in CubeJerry's unchanged PR6119
+surrogate.
+
+The existing nearest-even shear-history and shear-equivariance obstructions
+concern different contracts. This contribution is a precision side result,
+not a new paid supplier or a selected-caller proof. The assigned track is
+independent verification/formalization, OS random integer **83**. The original
+catalogue card is retained in [TASK.json](TASK.json), with the scope change to
+a written theorem explicitly disclosed. No proof-assistant formalization is
+claimed.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and no third-party dependencies:
+
+```sh
+python3.12 -I -W error -B research/walsh-interleaved-shear/verify.py
+```
+
+Expected: JSON with `status: PASS_WALSH_INTERLEAVED_SHEAR`,
+`complete_residue_inputs: 196608`, `witnesses: 24`, sixteen rejected controls
+and `no_new_kappa: true`, exactly matching [RESULT.json](RESULT.json).
+The direct command also works from a relocated copy of this package without
+Git or the rest of the repository. Context files are checked against their
+recorded SHA256 and Git blob IDs; they are not executable dependencies.
+
+The registered runner checks the historical task/source bindings and runs the
+same complete replay in ordinary and optimized Python, then the portable CLI
+and damaged-artifact controls:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/walsh-interleaved-shear
+```
+
+Expected final marker: `PASS_REGISTERED_RESEARCH_PACKAGE`, outcome `completed`.
+Full repository history is needed for those provenance checks. `VERIFY.json`
+declares no external live inputs; both context documents are included locally.
+
+`verify.py --emit-witnesses` deterministically reconstructs the certificate,
+searching `{-1,0,1}^4` in lexicographic order and stopping at the first witness
+for each of the 24 pair/sign keys. `verify.py --emit-result` performs the full
+replay and prints the receipt without comparing it to the committed receipt.
+Both options print to stdout and never overwrite a frozen file.
+
+## Evidence and failure coverage
+
+The integer engine uses signed floor quotients for nearest-even rounding and
+literal butterfly loops. Its independent oracle uses explicit dense matrices
+and `Fraction` rounding; neither imports predecessor code. They compare every
+rounded output, every exact output and the first stored vector, not merely a
+common maximum.
+
+| Check | Completed coverage |
+| --- | --- |
+| Residue census | `8^4 * 12 * 4 = 196608` inputs; 786432 output coordinates |
+| Fixed-source affine witnesses | 24 rows; both coefficient signs, including signed 201-bit coefficients |
+| Signed half-integer rounding | 2051 cases against exact rational rounding |
+| Period/coefficient controls | 768 reproducible large signed cases, seed 83 |
+| Reversed stage order | 2916 cases plus the written coordinate-conjugacy argument |
+| Semantic mutations | Floor ties, missing shear, reversed shear, repeated axis, wrong difference sign, missing exact-comparator shear, and single-final-round all detected |
+| Certificate/domain controls | Missing, duplicate, zeroed, wrong-slope and Boolean witnesses; off-grid input, fractional coefficient and aliased ports all rejected |
+| Overextended predecessor bound | Explicit unit-shear input defeats `3h/4`; removing the shear restores `3h/4` |
+
+The written input-period-eight and coefficient-residue lemmas explain why the
+census covers its stated domain. The all-input upper proof is independent of
+that census. All verifier checks use explicit exceptions and remain active
+under `-O`. The transcript SHA256 in RESULT.json binds the ordered complete
+computed vectors; it is an integrity check, not a substitute for mathematics.
+
+`check_artifacts.py` additionally runs the actual optimized CLI in a relocated
+temporary package with an empty PATH and no Git. It checks that every file and
+mode remains unchanged, then rejects four private-copy corruptions: changed
+context bytes, missing context, a missing witness and a Boolean receipt field
+replaced by integer one. The last control catches the `True == 1` ambiguity of
+untyped Python dictionary comparison. These four controls are separate from
+the sixteen mathematical/domain controls in RESULT.json.
+
+Local validation used CPython 3.12.14 on Linux x86_64. Normal and optimized
+registered scientific checks passed in 30.827 seconds combined; this is a
+descriptive replay duration, not a performance improvement claim. The portable
+CLI and all four artifact controls also passed. Witness regeneration matches
+the committed certificate byte for byte. Full environment and checkpoint
+details are in TASK.json. Hosted CI is not claimed.
+
+## Pins and limitations
+
+Base: `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8.
+The accepted selected record at that base is PR6030, κ = `0.003125804`.
+The actual construction, source manifest and review are recorded in TASK.json;
+historical task-card numbers are not treated as current frontiers.
+
+[SOURCES.json](SOURCES.json) pins the historical selected record and catalogue,
+plus the exact predecessor context documents:
+
+- PR6129 head `f496734450c346468c66818c1c35521165b0cdda`, PROOF.md.
+- PR6140 head `1c97110e1f25e8345f8ee63c570b88e172d75be9`, README.md.
+
+The two small verbatim context documents preserve the excluded scope and open
+question for review; their original notices remain intact. No pending PR's
+code is imported and no pending commit is required in publication ancestry.
+The mathematical statement is self-contained in this package.
+
+Assumptions: real grid inputs, exactly two distinct axes, one integral
+off-diagonal shear, exact arithmetic before each specified rounding, and
+sufficient range. Scaling gives arbitrary `h>0`; conjugacy gives the reversed
+axis order. Independent spectator fibers are covered only for shears within
+each fiber. No complex mixing, cross-fiber shear, nonintegral coefficient,
+multiple shear, more-stage, finite-width or overflow theorem is asserted.
+
+No bit/tape cost, reversible restoration, clean-scratch service or accelerated
+recursive child is supplied. All selected assumptions—`native_all_columns`,
+`owned_erasure`, `compiler`, `precision_tape`, `analytic_recovery`—remain open
+here. No selected cold replay, Lean kernel proof, hosted CI result or independent
+human review is claimed. **No new κ; the selected frontier is unchanged.**
+
+## Open next questions
+
+Can this exact normalization and rounding contract be bound to an actual
+selected `precision_tape` caller? First extract one complete rounded trace and
+compare its grid, gates and exact comparison map against the unit-shear witness.
+That binding is needed before changing any precision allocation; contracts
+with more stages or nonintegral/complex gates need separate analysis. This
+question and its blocker are structured in TASK.json.
+
+## Credit
+
+Prepared for Jerry Chen (@CubeJerry) with substantial OpenAI Codex assistance
+in derivation, implementation, verification and writing. New work is Apache-2.0.
+Nick Petalas retains credit for PR6129's pure-stage theorem and PR5912's history
+analysis; Josie Elliston for PR6140's audit and explicit open question;
+CubeJerry for PR6119's surrogate; Vlado Vojdanovski for PR1673's deferred-row
+context; Sricharan Vagvala for PR1631's distinct equivariance obstruction.
+The retained source documents credit their underlying native/BIT/analytic
+lineage. Douglas Colkitt's package scaffold and the repository's source/export
+verification tools are reused without modification.

research/walsh-interleaved-shear/RESULT.json

@@ -0,0 +1,32 @@
+{
+  "complete_output_comparisons": 786432,
+  "complete_residue_inputs": 196608,
+  "context_documents": 2,
+  "exact_error_in_grid_units": "(|m|+3)/4",
+  "full_output_transcript_sha256": "13b65e9e6657d8740b5819405299d80128fd2fa84e733ae11e051f11fd6f8b8b",
+  "large_signed_period_and_coefficient_cases": 768,
+  "no_new_kappa": true,
+  "rejected_controls": [
+    "floor-ties",
+    "omit-shear",
+    "reverse-shear",
+    "repeat-axis",
+    "wrong-difference",
+    "omit-exact-shear",
+    "single-final-round",
+    "missing-witness",
+    "duplicate-witness",
+    "zeroed-witness",
+    "wrong-slope",
+    "boolean-certificate",
+    "off-grid",
+    "fractional-shear",
+    "aliased-shear",
+    "unchanged-three-quarter-bound"
+  ],
+  "reverse_axis_cases": 2916,
+  "rounding_cases": 2051,
+  "scope": "two distinct normalized real Walsh axes, one integer shear",
+  "status": "PASS_WALSH_INTERLEAVED_SHEAR",
+  "witnesses": 24
+}