Prove sharp nearest-even Walsh-stage error (no new kappa)

research/nearest-even-walsh-error/PROOF.md

@@ -0,0 +1,178 @@
+# Sharp deterministic error for normalized Walsh stages
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Fix a grid spacing h>0 and an integer J>=0. On an array with J selected
+binary axes and any spectator axes, apply the J distinct factors
+
+    H0 = (1/2) [[1,1],[1,-1]],
+
+one axis at a time, in any fixed order. After every factor, round each
+coordinate to the nearest multiple of h, with ties to the even grid integer.
+The input is any array in h Z, without a magnitude restriction in the
+mathematical model. Every sum and difference before rounding is exact;
+overflow and other arithmetic defects are excluded.
+
+Let T be the exact normalized Walsh operator and F its rounded version.
+Then the sharp uniform coordinate bound is
+
+    sup_(x in (h Z)^(2^J)) ||F(x)-T x||_infinity = h a_J,
+    a_J = J/3 + (1-(-1/2)^J)/9.                         (1)
+
+Spectator fibers are independent, so the same bound holds for any number
+of spectators. Exact final recovery to the raw Walsh operator multiplies
+the error by 2^J. In particular its sharp bound is h 2^J a_J.
+
+The more precise statement for one output coordinate is as follows. If
+its stored output divided by h is even, the sharp absolute error is h a_J.
+If it is odd and J>=1, the sharp absolute error is h a_(J-1).
+At J=0 both errors are zero.
+
+The theorem concerns this deterministic quantizer. It is not a theorem for
+arbitrary bounded faults, non-grid initial data, repeated axes, intervening
+non-Walsh gates or the actual accelerated recursive supplier.
+
+## Reduction to a binary averaging tree
+
+Scale by h and work with integer grid values. Write R(s) for nearest-even
+rounding of a real number to an integer. It is odd, and
+
+    R(s+2k) = R(s)+2k                                   (2)
+
+for every integer k. Translation by an odd integer need not commute with R.
+
+Fix an output of the J-stage butterfly network. Its dependencies form a
+complete binary tree of depth J, with disjoint original inputs at its
+leaves. Each internal node is R((u+v)/2) or R((u-v)/2).
+Oddness lets us absorb every minus sign into the leaves and intermediate
+subtrees. Thus it suffices to analyze a complete tree of rounded averages.
+Its exact value is the average of its 2^J signed leaves. This reduction
+uses distinct axes; repeated use of an axis need not give disjoint leaves.
+
+## Parity-sensitive bounds
+
+Let a_j and b_j be the maximal absolute error at depth j conditioned on
+an even or odd integer output. Start with a_0=b_0=0. We prove inductively
+that the finite maxima exist and satisfy
+
+    b_j = a_(j-1),
+    a_j = 1/2 + (a_(j-1)+b_(j-1))/2.                    (3)
+
+Consider child outputs u,v. If u+v is even, the root division is exact.
+The child parities agree, and averaging their errors costs at most
+max(a_(j-1),b_(j-1))=a_(j-1).
+
+If u+v is odd, its half lies exactly between consecutive integers. The
+stored root is even, its local error has magnitude 1/2, and the child
+parities differ. The total error is therefore at most the second line
+of (3). An odd root can occur only in the exact-division case, proving
+the first line's upper bound.
+
+For completeness the second line dominates the exact-division bound.
+Put d_j=a_j-a_(j-1). The recurrences give d_1=1/2 and
+
+    d_j = (1-d_(j-1))/2,    j>=2.
+
+Induction gives 1/4<=d_j<=1/2 for every j>=1. Hence a_j is increasing and
+b_j<=a_j. This proves the comparisons used in the induction, without
+assuming a closed form in advance.
+
+## Attaining inputs
+
+Construct integer leaf lists E_j,O_j with rounded outputs 0 and 1.
+Their signed errors, stored output minus exact average, will be a_j,b_j.
+Use concatenation, and let adding an integer to a list mean entrywise
+addition. Define
+
+    E_0=[0],  O_0=[1],
+    E_j = E_(j-1) concatenated with (O_(j-1)-2),
+    O_j = E_(j-1) concatenated with (E_(j-1)+2).          (4)
+
+By (2), the children of E_j have stored outputs 0,-1 and errors
+a_(j-1),b_(j-1). Their root rounds -1/2 to 0, so its error is the second
+line of (3). The children of O_j have outputs 0,2 and both have error
+a_(j-1). Their root is exactly 1, proving the first line of (3).
+Negating a leaf list attains the negative extremum. Even translations
+give every other prescribed output of the same parity.
+
+The E_j entries lie in [-j,0]. In the ordinary low-bit-first Walsh
+schedule, concatenate the lists along the last processed axis. Then its
+zero-frequency output is exactly the averaging tree above. This proves
+attainment in the actual butterfly network, rather than in a relaxed
+independent-error model. Other fixed axis orders use the matching input
+axis permutation. Therefore the coordinate upper bound and the sup norm
+maximum in (1) are both sharp.
+
+Substituting b_j=a_(j-1) in (3), with a_0=0 and a_1=1/2, gives
+
+    a_j = 1/2 + (a_(j-1)+a_(j-2))/2,    j>=2.
+
+The expression (1) satisfies these initial conditions and recurrence,
+which proves the formula. The usual stagewise bound is J h/2. Equation
+(1) is strictly smaller for every J>=2, and its ratio to J h/2 tends to 2/3.
+These are exact algebraic comparisons, not measured speedups.
+
+## Complete residue domains
+
+For depth J the error is periodic in each integer input coordinate with
+period 2^(J+1). Indeed, add 2^(J+1) times an arbitrary integer array to
+the input. After k stages its exact displacement has coordinates
+divisible by 2^(J+1-k), which are even integers for all k<=J. Equation
+(2) therefore propagates precisely that displacement through every
+rounded stage. The final displacement equals the exact Walsh displacement,
+so their error arrays coincide. This also holds in the presence of signs.
+
+Consequently the verifier's 4^2 one-stage inputs and 8^4 two-stage inputs
+are complete residue-domain checks for those depths. Larger depths are
+corroborated by witnesses and a parity-state enumeration; the all-J
+conclusion rests on the proof above.
+
+## Application to PR #6119's numerical surrogate
+
+CubeJerry's PR #6119, head bdfe5a10d488b5f774e906d8d4588dc8da25e7ba,
+defines an eight-input surrogate with exposure, four temporary coordinates,
+the echo m=1/2,a=4, two distinct H0 axes and projection of the temporaries.
+It rounds after its six nominated noisy maps to the same h grid.
+Its arbitrary-defect theorem and its finite ternary-cube observation are
+credited prior results and context; neither is re-audited here.
+
+For every grid retained coordinate x=h k, its initially zero echo temporary
+becomes h R(k/2). The upper addition and its inverse are integer-grid
+operations and cancel exactly. The lower inverse leaves, before rounding,
+
+    h [R(k/2)-k/2],
+
+which is 0 or +/-h/2, and hence rounds to zero. Thus for every grid input
+the entire rounded echo is the identity on retained data and returns the
+temporary row to zero. The remaining retained computation is precisely
+two rounded Walsh axes. Exposure and its inverse are exact permutations.
+Its sharp normalized error is therefore 3h/4, for all eight grid inputs.
+
+At the predecessor's h=1/4 this is 3/16; exact raw recovery multiplies it
+by four, giving 3/4. One attaining original-coordinate input is
+
+    (0,0,-1/4,0,-1/2,0,0,0).
+
+The four entries of the first spectator fiber are E_2/4. This supplies an
+all-grid theorem and explicit witness beyond the predecessor's finite
+6,561-point cube. It is still a numerical surrogate, not a materialized
+PR6030 child or a physical disposal implementation.
+
+## Limits and credit
+
+CubeJerry supplies the explicit open distinction between independent
+defect boxes and deterministic quantizer errors, and the two-phase surrogate.
+Vlado Vojdanovski's PR1673 supplies the normalized H0/deferred-row context;
+the selected construction retains its original authors and five assumptions.
+JoyboyBrian's `native-rounded-butterfly-contract` supplies related pair-first
+nearest-even arithmetic and parity constraints for different complex Gaussian
+letters. The present averaging-tree parity recurrence and attaining all-J
+Walsh bound are the new result.
+
+No full selected replay, native admission, proof-kernel check or independent
+human review is claimed. The theorem assumes exact pre-rounding arithmetic,
+unbounded integer range and the specified grid ABI. Bit costs, intermediate
+range guards, tape movement, reversible history and an accelerated supplier
+remain separate obligations. Source files and the selected frontier are unchanged.

research/nearest-even-walsh-error/README.md

@@ -0,0 +1,139 @@
+# Sharp nearest-even Walsh-stage error
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For J distinct normalized Walsh stages, with exact sums and differences
+and nearest-even rounding to a common grid h after each stage, the sharp
+uniform error over every grid input is
+
+    h [J/3 + (1-(-1/2)^J)/9].
+
+The usual stagewise bound is J h/2. The new bound is strictly smaller
+for J>=2 and approaches two thirds of that coefficient. This is a scoped
+mathematical proof with exact finite corroboration, not a new kappa.
+
+[PROOF.md](PROOF.md) proves the even/odd output recurrence and constructs
+attaining integer inputs for every J. At even stored outputs the maximum
+is h a_J; at odd outputs it is h a_(J-1). The attaining even-output inputs
+use only integers between -J and zero in grid units.
+
+## New source application
+
+CubeJerry's [PR #6119](https://github.com/CrocSwap/integer-mult-bounds/pull/6119)
+reports normalized error at most 3/16 on a finite cube for its particular
+two-phase nearest-even surrogate at h=1/4. Its separate arbitrary-defect
+box has a sharp bound of 1. The present result proves **3/16 is the exact
+global error for every grid input** of that surrogate. Exact raw recovery
+gives the sharp value 3/4. Its rounded echo returns the temporary row to
+zero on every such input. This does not establish a physical erasure cost.
+
+The source is pinned as a literature reference at
+`bdfe5a10d488b5f774e906d8d4588dc8da25e7ba`. Its explicit m=1/2,a=4 echo
+becomes identity on grid inputs; the remaining computation is two rounded
+Walsh axes. One new attaining original-coordinate input is
+`(0,0,-1/4,0,-1/2,0,0,0)`. No predecessor verifier or census is imported,
+executed or offered as this contribution.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and the standard library suffice:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nearest-even-walsh-error/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nearest-even-walsh-error/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nearest-even-walsh-error
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nearest-even-walsh-error --check-source-history
+```
+
+Another CPython 3.12 interpreter may replace that absolute path. The last
+command checks publication bytes after committing. Direct verification
+prints a generated SHA256-bound JSON receipt with status
+`PASS_NEAREST_EVEN_WALSH_ERROR` and writes no files.
+
+The exact finite coverage is:
+
+- 2,049 signed half-integers checked against a separate exact Fraction
+  nearest-even implementation, including the tie-output parity.
+- All 16 one-stage and 4,096 two-stage residue inputs, with every output
+  compared to the literal Walsh coefficient formula. Error periodicity
+  makes these complete integer-input domains at those two depths.
+- Reachable error sets classified by output parity through depth seven,
+  independently of the proposed closed formula.
+- Even- and odd-output attaining witnesses through depth twelve, in both
+  low-bit-first and reversed schedules, with every output checked and
+  negative witnesses checked by actual execution.
+- 256 signed periodicity fixtures through eight stages, 513 echo values
+  and 65 full eight-coordinate source-application fixtures.
+- Four scope controls and five rejected invalid inputs. Off-grid data
+  give error 7/8 at J=2; different tie rules can give error 1. These
+  explicitly reject unwarranted extensions of the 3/4 grid-unit theorem.
+
+The finite checks corroborate the all-J written proof. They do not replace
+its quantifiers or supply independent human or proof-kernel review.
+
+## Scope, provenance and overlap
+
+The original `uniform-transfer-audit` card is explicitly changed to this
+numerical side theorem for the `precision_tape` boundary. It does not
+discharge any selected framework assumption. The authenticated selected
+metadata baseline passed at main
+`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. Its selected
+conditional kappa is 0.003125804. No selected cold replay was needed or run.
+
+This is a new quantizer-specific step beyond PR6119's finite cube, not an
+audit of its arbitrary-defect theorem. Source questions and exact reference
+heads are in [TASK.json](TASK.json). The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241916)
+records the expected scope. Live PRs, recent account work, Discussion
+claims, local reservations, main text and merged-PR searches were checked.
+The overlap cache covered 379 open PRs and 5,777 Discussion records with
+complete remote pagination, but only 70 of 8,348 local note paths. Direct
+Git searches supplemented that sparse coverage. These are bounded overlap
+checks, not proof of global novelty.
+
+The theorem requires grid input, distinct Walsh axes, the specified tie
+rule, exact pre-rounding arithmetic and sufficient range. Arbitrary faults,
+non-grid inputs, other gates, repeated axes and complex Gaussian butterflies
+need separate bounds. A real emitted recursive caller, bit costs, overflow
+guards, tape routing, reversible history and supplier admission remain open.
+The selected frontier and all five assumptions are unchanged. No Lean,
+Docker, full native replay or complete multiplication theorem is claimed.
+
+## Engineering bounds
+
+The verifier has no recursion, subprocesses or external mathematical imports.
+Its transform accepts at most 4,096 entries and signed inputs of magnitude
+at most 2^64. The formula interface permits depths through 64; executed
+full witnesses stop at twelve. Every function is below 60 physical lines.
+The largest explicit exhaustive input domain has 4,096 tuples; the parity
+enumeration stops at seven and stores at most 627 errors in one parity set.
+All checks use explicit exceptions and remain active under optimization.
+
+Python's required dynamic allocation is the bounded managed-runtime
+deviation from Power of Ten static allocation. Lists, integer sizes and
+set domains are bounded by the fixed limits above. Receipt reads are
+limited to twelve package files of at most one MiB each. Warning-strict
+normal and optimized checks provide runtime diagnostics; no shared build
+configuration is changed. This offline verifier is not a machine-cost model.
+
+## Open next questions
+
+1. Bind the sharp bound to an actual emitted recursive H0 boundary with
+   its grid, axis ordering, pre-rounding arithmetic and range guards.
+   First export that complete event list; it is missing here. The smaller
+   logical error coefficient alone supplies no accelerated physical bill.
+2. Can an analogous parity-state analysis sharpen deterministic rounding
+   for the actual complex Gaussian butterflies? Start with their joint
+   real/imaginary parity states. Their mixing and error amplification
+   differ from this real averaging tree, so this formula does not transfer.
+
+## Credit
+
+Credit CubeJerry for PR6119's explicit surrogate and separation between
+defect boxes and quantizer correlations; Vlado Vojdanovski for PR1673's
+normalized H0/deferred-row interface; and JoyboyBrian for related pair-first
+nearest-even Gaussian butterfly arithmetic and parity constraints. Their
+native, analytic, compiler and selected-construction predecessors retain
+their attribution. The new result is the all-J parity recurrence, its
+sharp attaining family and the all-grid two-phase consequence. Independent
+human and formal proof-kernel review are unclaimed.

research/nearest-even-walsh-error/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}