Prove sharp 9h/8 error for a rounded half-shear (no κ)

research/rounded-half-shear-walsh/CODE-BOUNDS.md

@@ -0,0 +1,38 @@
+# Executable bounds
+
+The verifier is read-only and uses Python 3.12's standard library. No source
+module from another package is imported. Every mathematical acceptance check
+uses an explicit exception and survives optimized execution.
+
+- There is no recursion, subprocess, network request, dynamic evaluation or
+  callback registration. The normal exit prints one generated JSON receipt;
+  any failed invariant raises an exception and fails the command.
+- Every matrix has exactly four rows and columns. Every word has exactly
+  three stages. All products use fixed loops of length four or three.
+- Each census has twelve orientations and exactly 65,536 inputs per
+  orientation. It streams the inputs and stores twelve ten-bin histograms,
+  twelve witnesses and one hash state. It does not retain the input corpus.
+- The primary public evaluator checks exactly four integer inputs, with
+  absolute values below 2^128, and distinct integer indices in 0..3. Booleans
+  are rejected. Internal census calls have the stronger fixed domain 0..15.
+- The independent interpreter is a fixed-corpus executable, not a public
+  arbitrary-matrix API. Its matrices are constructed locally from twelve
+  fixed index pairs. Its Fraction oracle has 256 inputs per pair.
+- Receipt hashing reads exactly eight package files and one declared context
+  input, each guarded at one MiB. All filesystem read failures propagate.
+  The primary checks the context's pinned SHA256 before its census.
+- All functions are below sixty physical lines. Warning-strict normal and
+  optimized runs, source compilation and AST inspection are the available
+  local diagnostics. No separate linter or type checker is configured here.
+
+Power of Ten rule 3 has a managed-runtime deviation in both Python files.
+Python allocates integers, tuples, Fraction values and hash/JSON buffers
+dynamically. The fixed matrix/corpus sizes, streaming census, input bit bound
+and one-MiB receipt-input limits bound live state. These are certificate
+programs, not fixed-allocation runtime kernels. A fixed-capacity rewrite is
+required before deploying them in a setting that prohibits allocation.
+
+Python has no exposed raw-pointer dereference or compiler-preprocessing step
+on these paths. Direct local function calls and shallow immutable matrix rows
+are the corresponding inspected mechanisms. The only file writes are stdout
+receipts; callers put them outside the checkout.

research/rounded-half-shear-walsh/PROOF.md

@@ -0,0 +1,144 @@
+# Sharp error for one rounded half-shear
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let R be componentwise nearest-integer rounding with ties to even. Coordinates
+are numbered 0,1,2,3. Define
+
+```text
+2A = [[1, 1, 0, 0],       2B = [[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]].
+```
+
+For any distinct t,s in {0,1,2,3}, put S=I+E_ts/2 and
+
+```text
+y=R(Ax), z=R(Sy), F(x)=R(Bz), T=BSA, x in Z^4.
+```
+
+Then
+
+```text
+max_(x in Z^4) ||F(x)-Tx||_infinity = 9/8.
+```
+
+The middle rounding is part of the program. The comparator contains the same
+half-shear without rounding. On grid h Z^4, using R_h(v)=h R(v/h) at each
+rounding, the sharp error is 9h/8 for every h>0.
+
+## Universal upper bound
+
+Write delta=y-Ax, epsilon=z-Sy and eta=F(x)-Bz. Each coordinate of delta and
+eta is in {0,+1/2,-1/2}. Only epsilon_t can be nonzero, and it is in the
+same three-element set. The endpoint error is exactly
+
+```text
+F(x)-Tx = BS delta + B epsilon + eta.
+```
+
+Nearest-even rounding of a half-integer has the implication
+
+```text
+delta_i != 0 implies y_i is even.
+```
+
+For any output whose B-pair does not contain t, the middle update is absent.
+If eta_j=0, the error is at most 1/2. Otherwise that pair of stored integer
+inputs has odd sum or difference. At least one input is odd, so its delta
+is zero. The error is at most 1/4+1/2=3/4.
+
+For an affected output, put p=t xor 2. With the actual B-row signs
+alpha,beta in {+1,-1}, the error is
+
+```text
+(alpha delta_t + beta delta_p + alpha delta_s/2
+ + alpha epsilon_t)/2 + eta_j.
+```
+
+This identity also covers s=p. Its repeated occurrence does not create an
+independent error variable.
+
+If epsilon_t=0, the triangle bound is
+
+```text
+(1/2 + 1/2 + 1/4)/2 + 1/2 = 9/8.
+```
+
+Suppose epsilon_t is nonzero. Since y_t,y_s are integers, y_s must be odd.
+Consequently delta_s=0. The middle operation rounded a half-integer to even,
+so z_t is even. If eta_j=0, the remaining error is at most
+(1/2+1/2+1/2)/2=3/4. If eta_j is nonzero, z_t and z_p have opposite parity.
+Thus z_p=y_p is odd, and delta_p=0. The error is at most
+(1/2+1/2)/2+1/2=1. This proves the upper bound for every integer input,
+without a search assumption.
+
+## Attainment
+
+The following explicit inputs attain the bound. The final column is one
+coordinate of 8(F(x)-Tx). Every row is evaluated by both integer and dense
+interpreters during the full residue checks.
+
+| t | s | x | output coordinate j | error times eight |
+|---:|---:|---|---:|---:|
+| 0 | 1 | (1,4,0,1) | 0 | -9 |
+| 0 | 2 | (0,1,0,13) | 0 | -9 |
+| 0 | 3 | (0,1,0,3) | 2 | -9 |
+| 1 | 0 | (1,2,0,3) | 3 | 9 |
+| 1 | 2 | (0,1,0,3) | 3 | 9 |
+| 1 | 3 | (0,1,0,13) | 1 | 9 |
+| 2 | 0 | (0,3,0,7) | 0 | 9 |
+| 2 | 1 | (0,3,0,1) | 2 | 9 |
+| 2 | 3 | (0,1,1,4) | 0 | -9 |
+| 3 | 0 | (0,3,0,1) | 3 | -9 |
+| 3 | 1 | (0,3,0,7) | 1 | -9 |
+| 3 | 2 | (0,1,1,10) | 1 | 9 |
+
+For example, t=0,s=1,x=(1,4,0,1) gives
+y=(2,-2,0,0), z=(1,-2,0,0), F(x)=(0,-1,0,-1), and
+8Tx=(9,-8,5,-4). Hence the complete error times eight is (-9,0,-5,-4).
+The middle rounding is exact in this extremizer. Its possible nonzero
+error elsewhere still needs the preceding case analysis.
+
+## Complete finite reduction
+
+Nearest-even rounding commutes with every even integer translation. Replace
+x by x+16v, for arbitrary v in Z^4. At the first stage the displacement
+16Av is coordinatewise divisible by eight, so y shifts by exactly 16Av.
+After S, the displacement is divisible by four, so z shifts by exactly
+16SAv. After B, the displacement is even, so F shifts by exactly 16BSAv.
+The linear comparator has that same displacement. Thus the entire error
+vector is periodic modulo 16 in each input coordinate.
+
+Both verifiers enumerate all 12*16^4=786,432 pair/input cases. The primary
+uses explicit butterflies and a closed signed half-rounding formula. The
+separate interpreter multiplies three dense integer matrices and chooses
+the nearer integer by two distances. It also compares 3,072 complete output
+error vectors with Python Fraction rounding. The canonical stream of all
+3,145,728 signed eighth-unit error coordinates is hashed in both checks.
+This is a finite certificate, and the parity argument supplies an independent
+all-input upper bound. Neither is a formal-kernel proof.
+
+Period eight is insufficient. For t=0,s=1, the inputs (0,0,0,2) and
+(8,0,0,2) give error vectors times eight (-4,4,4,-4) and (4,4,-4,-4).
+The integer-shear period must therefore not be reused silently here.
+
+## Scope and predecessors
+
+Josie Elliston's #6140 poses the interleaved-grid-shear question. Jerry Chen /
+CubeJerry's #6146 proves the different exact-integer-shear law and supplies
+the two-axis model and parity context. Nick Petalas's #6129 pure-stage law
+is background. No predecessor theorem, scientific code or census is replayed
+as this contribution. The upper bound and half-shear witnesses above are new
+work for the stated program; nearest-even parity and translation facts are
+elementary and carry no literature-priority claim.
+
+The theorem covers one positive half-shear, two distinct real Walsh axes,
+exact arithmetic before each specified rounding and sufficient range.
+Negative/other rational coefficients, complex gates, additional stages,
+cross-fiber operations and a production compiler binding remain outside it.
+There is no physical cost, reversible-history implementation, native supplier,
+precision saving, kappa improvement or complete multiplication theorem.

research/rounded-half-shear-walsh/README.md

@@ -0,0 +1,111 @@
+# Sharp 9h/8 error for a rounded half-shear between Walsh axes
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with an exact finite certificate. For each
+of the twelve directed pairs of four coordinates, the literal program
+
+```text
+x in h Z^4
+y = R_h(Ax)
+z = R_h((I + E_ts/2)y)
+F(x) = R_h(Bz)
+T = B (I + E_ts/2) A
+```
+
+has sharp error `max_x ||F(x)-Tx||_infinity = 9h/8`. Here A and B are the
+two distinct normalized real Walsh axes defined in [PROOF.md](PROOF.md),
+and every R_h rounds to nearest with ties to even. This determines an exact
+value for a program outside the integer-shear law of
+[CubeJerry #6146](https://github.com/CrocSwap/integer-mult-bounds/pull/6146).
+The half-shear is rounded internally, so it adds a rounding site.
+
+The direct triangle bound is 11h/8. The parity proof improves it to 9h/8,
+and twelve explicit integer inputs attain that value. A nonzero rounding
+error at the middle shear forces its stored target to be even and its source
+to be odd. Those parities remove earlier error terms at a final half-tie.
+The complete error vector has input period 16h in each coordinate. An exact
+counterexample shows that the integer-shear period 8h is insufficient here.
+
+This answers a nonintegral part of the intervening-shear question in
+[Josie Elliston #6140](https://github.com/CrocSwap/integer-mult-bounds/pull/6140).
+The previous integer result and pure-stage results are cited context, not
+replay targets. No new kappa or selected-frontier change is claimed.
+
+## Evidence and reproduction
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-half-shear-walsh/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-half-shear-walsh/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rounded-half-shear-walsh/independent.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-half-shear-walsh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-half-shear-walsh --check-source-history
+```
+
+Another CPython 3.12 path may replace the absolute interpreter. The direct
+commands print `PASS_ROUNDED_HALF_SHEAR_WALSH` or
+`PASS_INDEPENDENT_HALF_SHEAR_WALSH` inside generated JSON stdout evidence.
+The primary receipt is bound to all eight package files and the one context
+input. No receipt is hand-written or consumed as an acceptance premise.
+
+Each interpreter enumerates all 786,432 directed-pair/input cases and hashes
+the complete stream of 3,145,728 signed eighth-unit errors. The primary uses
+literal butterfly arithmetic. The independent implementation uses dense
+integer matrices and another rounding algorithm, with 3,072 complete-vector
+Fraction comparisons. Seven named semantic controls cover the insufficient
+period, sharp endpoint, tie rule, omitted middle rounding, omitted shear,
+reversed word and signed ties. Eight invalid primary inputs are rejected.
+The primary also checks 515 signed half-rounds and 576 signed/large period
+translations. The mathematical theorem rests on the written parity proof
+and explicit attaining inputs, not an extrapolation of finite experiments.
+
+## Scope and provenance
+
+Base `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. The
+selected #7000 record gives conditional kappa `363005817/100000000000`.
+The source-binding positive control passed; it was not a scientific replay.
+[TASK.json](TASK.json) records the changed `uniform-transfer-audit` scope.
+[SOURCES.json](SOURCES.json) pins the catalogue, selected record and the
+unchanged integer-shear context. The package imports no predecessor code.
+
+The theorem assumes exact pre-round arithmetic and sufficient range. It
+does not cover another coefficient, complex mixing, extra stages or a
+production caller. There is no finite-width implementation, reversible
+history, physical coefficient service, storage/tape bill, compiler admission,
+native supplier or complete multiplication theorem. All five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed. Lean, Docker and the selected scientific cold replay
+are unrun. Executable bounds and the allocation deviation are recorded in
+[CODE-BOUNDS.md](CODE-BOUNDS.md).
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572871)
+preceded the new calculation. Live open/account PRs, recent handoffs, local
+reservations, complete cached open/closed source-reference checks, all-main
+README searches and merged keyword searches were checked. Those searches
+do not cover unpublished work or arbitrary historical diffs.
+
+## Open next questions
+
+- Which other rational coefficients have a sharp error law when the shear
+  is rounded internally? Fix one coefficient and first derive its valid
+  even-translation period. The general parity and attainment arguments are
+  absent. No further coefficient is claimed here.
+- Does an actual selected `precision_tape` caller contain this exact tile?
+  Extract one complete trace and match its grids, rounding sites and
+  comparator. Range, coefficient service, reversal, storage and the full
+  caller bill remain blockers to any precision change.
+
+## Credit
+
+Josie Elliston / JosieElliston #6140 supplies the interleaved-gate question.
+Jerry Chen / CubeJerry #6146 supplies the integer-shear model, parity context
+and its explicitly excluded coefficient domain. Nick Petalas #6129 supplies
+the pure-stage background; its theorem is not used as the new proof step.
+The deferred-row context belongs to Vlado Vojdanovski #1673, and the distinct
+shear-equivariance context to Sricharan Vagvala #1631, retaining the native,
+BIT and analytic lineage credited by those sources. Douglas Colkitt's package
+scaffold and the repository publication checks are reused without edits.
+The new half-shear theorem, attaining inputs and checkers were produced by
+Nick Petalas. Predecessor files and credit lines are unchanged.

research/rounded-half-shear-walsh/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/walsh-interleaved-shear/PROOF.md",
+      "usage": "input",
+      "git_blob": "c2b60aceb03d8a59e8e3d7cd71e51f70cc2a38da",
+      "sha256": "e16cb441209c6a093c2f21eeec96819b88a7f8a74bd7df103267ddf88c9f644a"
+    }
+  ]
+}