Prove the sharp shared Fourier translation error floor (no κ)

research/shared-fourier-translation-floor/PROOF.md

@@ -0,0 +1,169 @@
+# Sharp error for a shared translated Fourier routine
+
+This proof and its application were produced by Nick Petalas. Apache-2.0.
+
+## Contract and result
+
+Let G be any finite product of cyclic groups, N=|G|, with its standard
+symmetric nondegenerate character pairing chi. Write
+
+    (F± u)(x) = (1/N) sum_y chi(x,y)^±1 u(y).
+
+Both signs have the factor 1/N. Convolution has no normalization. Let
+b be a nonzero element of order two, let P_b f(x)=f(x+b), and let w(x)
+be an arbitrary complex function with |w(x)|=1. Use exactly the same
+routine A=D_w P_b F− for the two forward passes, and conjugate its
+coefficients for the final pass. Thus
+
+    B_w(u,v) = D_conj(w) P_b F+ [(D_w P_b F−u)(D_w P_b F−v)],
+    B(u,v)   = (u*v)/N².
+
+For a bilinear map L, define its coefficient Frobenius norm by
+
+    ||L||_F² = sum_(s,t in G) ||L(e_s,e_t)||_2².
+
+The normalization gives ||B||_F=1/N. Define
+
+    E(w) = N ||B_w-B||_F,
+    R(w) = N² max_(s,t in G) ||B_w(e_s,e_t)-B(e_s,e_t)||_2.
+
+These are respectively a relative coefficient norm and the largest
+relative output error among the basis-input pairs. No relative error
+claim for arbitrary inputs with possibly zero convolution is intended.
+
+**Theorem.** For every such G and b,
+
+    min_(|w|=1) E(w) = min_(|w|=1) R(w)
+                    = sqrt(2 - 8/(3 sqrt(3))).                 (1)
+
+The same explicit weights attain both minima:
+
+    c(x) = chi(b,x),
+    w(x) = 1/sqrt(3) - i sqrt(2/3) c(x).                       (2)
+
+Moreover, every basis-input pair has the same normalized error in (1)
+for these weights. The constant is independent of N and of chi(b,b).
+
+The new claim is this quantitative optimum for the shared translated
+contract. Hanson Sun / bbMisk's PR1477 supplies the predecessor exact
+weighted-layout classification and normalization, extending Ross
+Richardson's PR940. It already excludes exact convolution here. No part
+of that classification or its census is claimed as new.
+
+## Reduction to two scalar moments
+
+The character c takes values +1 and −1. It is nontrivial by
+nondegeneracy and b!=0. Consequently the two signs each occupy N/2
+points. Set f=F−u, g=F−v and compare the coefficient of
+f(y+b)g(y+b) in output x before substituting f,g. The implemented and
+desired coefficients are respectively
+
+    (1/N) conj(w(x)) w(y)² chi(x+b,y),
+    (1/N) chi(x,y+b).
+
+Their ratio is
+
+    rho(x,y) = conj(w(x)) w(y)² c(x)c(y).                      (3)
+
+There are no off-diagonal input products because the two forward read
+maps agree. Each of the N² desired coefficients has modulus 1/N.
+The matrices sqrt(N) F− are unitary. Substitution of F− in each of
+the two input indices therefore multiplies the squared coefficient
+norm by 1/N². It follows that
+
+    E(w)² = (1/N²) sum_(x,y) |rho(x,y)-1|².
+
+Define a(x)=c(x)w(x), with |a|=1, and use uniform expectations on G:
+
+    m = E a,              n = E c a².
+
+The average of rho is conj(m)n. Thus
+
+    E(w)² = 2 - 2 Re(conj(m)n).                               (4)
+
+This identity is exact. In particular, the normalization does not hide
+an error that decays with N relative to the desired basis output.
+
+## The scalar inequality
+
+We prove |m n| <= 4/(3 sqrt(3)) for every unit-valued a on a
+balanced two-class probability space. Write
+
+    u = E[a | c=+1],       v = E[a | c=−1],
+    p = E[a² | c=+1],      q = E[a² | c=−1],
+    d = (u-v)/2,           r=|m|,      s=|d|.
+
+Since m=(u+v)/2, n=(p-q)/2, and |u|,|v|<=1, we have
+r²+s²=(|u|²+|v|²)/2<=1. The conditional variance identity gives
+
+    |p-u²| = |E[(a-u)² | c=+1]| <= 1-|u|²,
+    |q-v²| <= 1-|v|².
+
+Taking the triangle inequality and using u²-v²=4md yields
+
+    |n| <= 2rs + 1-r²-s² = 1-(r-s)².                         (5)
+
+If r<=1/sqrt(2), the elementary |n|<=1 gives
+|mn|<=1/sqrt(2)<4/(3 sqrt(3)). If r>=1/sqrt(2), then
+s<=sqrt(1-r²)<=r. The right side of (5) increases with s throughout
+this interval. Hence
+
+    |mn| <= 2r² sqrt(1-r²).
+
+For x=r², the following polynomial identity proves the required
+maximum on [1/2,1], without a numerical optimization:
+
+    16/27 - 4x²(1-x) = (4/27)(3x-2)²(3x+1) >= 0.             (6)
+
+Equations (4) and (6) imply E(w)²>=2-8/(3 sqrt(3)). Also
+
+    R(w)² = N⁴ max_(s,t) ||(B_w-B)(e_s,e_t)||²
+          >= N² sum_(s,t) ||(B_w-B)(e_s,e_t)||² = E(w)².
+
+This proves both lower bounds in (1).
+
+## Equality on every basis pair
+
+Set h=1/sqrt(3), r=sqrt(2/3), and choose w=h-i r c. These weights
+have modulus one. Then a=h c-i r, so
+
+    m = -i r,             n = -2i h r,
+    conj(m)n = 2h r² = 4/(3 sqrt(3)).
+
+This proves equality for E. To establish equality for R as well,
+calculate the actual three-pass output on e_s,e_t. Let k=s+t and note
+
+    w(y)² = -1/3 - (2i sqrt(2)/3)c(y).
+
+Character orthogonality leaves only two output coordinates, k and k+b.
+They are distinct since b!=0. Their values, multiplied by N², are
+
+    at k:     4/(3 sqrt(3)) - (2i sqrt(2)/(3 sqrt(3))) c(k),
+    at k+b:   -(1/3)c(k) conj(w(k+b)).                         (7)
+
+The second has modulus 1/3 regardless of chi(b,b). The desired
+normalized output is one at k and zero elsewhere. Its squared error is
+
+    (4/(3 sqrt(3))-1)² + 8/27 + 1/9
+      = 2 - 8/(3 sqrt(3)).
+
+It is the same for every s,t. This proves (1) and (2).
+
+## Scope
+
+The argument covers every unit complex phase function, every product of
+cyclic groups, and every nonzero order-two translation under the stated
+shared-routine contract. The finite checker covers only its listed tiny
+groups and phases. The universal assertion comes from this written proof.
+
+Separate forward/final phases escape the theorem. For example, the same
+translation with forward weights alpha=1, beta=c and final weight omega=c
+gives exact convolution, as in the predecessor affine criterion. This is
+an explicit control of the hypothesis, not a new construction claim.
+
+The optimum uses algebraic phases, and their preparation or application is
+not priced. Other-order translations, arbitrary affine maps, general
+unit-norm-input operator error and rounded implementations are not settled.
+No physical caller, recursive saving, supplier admission, selected-frontier
+change or complete multiplication theorem follows. Independent human and
+formal proof-kernel review are unclaimed.

research/shared-fourier-translation-floor/README.md

@@ -0,0 +1,142 @@
+# A sharp error floor for shared translated Fourier routines
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped written proof with exact finite corroboration. For any finite product
+of cyclic groups and any nonzero order-two translation, the best shared
+phase-weighted two-input Fourier convolution routine has error
+
+    min relative coefficient error = min worst basis-pair relative output error
+                                   = sqrt(2 - 8/(3 sqrt(3))).
+
+Both forward passes use the same routine and the final pass conjugates that
+routine's coefficients. Both Fourier signs use 1/N normalization, so the
+desired output is (u*v)/N². The output error uses the Euclidean norm.
+The optimum is independent of the group size. The explicit unit weights
+
+    w(x) = 1/sqrt(3) - i sqrt(2/3) chi(b,x)
+
+attain it on every basis-input pair. [PROOF.md](PROOF.md) defines both error
+norms and proves the universal statement. This is a quantitative obstruction
+to replacing an exact convolution boundary with this approximate shared
+translated routine. It supplies no new kappa or physical construction.
+
+## What is new and what is inherited
+
+Hanson Sun / bbMisk's [PR1477](https://github.com/CrocSwap/integer-mult-bounds/pull/1477)
+classifies the exact weighted Fourier interface, extending Ross Richardson's
+[PR940](https://github.com/CrocSwap/integer-mult-bounds/pull/940). It already
+rules out exact shared translated convolution. The new result quantifies the
+smallest achievable error and supplies its attaining weights. The two-moment
+inequality, coefficient-norm invariance and character orthogonality are
+elementary tools; no literature-priority claim for those tools is made.
+
+The original approximation question is not the open physical-routing question
+in PR1477. The exact classification and its census were cited, not re-audited.
+Nick Petalas's older PR4874 treats exact cancellation at arbitrary arity.
+PR5946 restricts the second input with unequal forward reads and fixed
+first/final charts. The present contract has two unrestricted inputs, shared
+reads and phases, and measures approximation error. Its proof does not rely
+on either of those packages. The separate concurrent PR1477 replay-arithmetic
+work retains the predecessor's original decisions and is distinct from this
+mathematical question.
+
+This is a changed `joint-query-controller` side result. It addresses the
+precision/analytic boundary of a proposed Fourier contract, rather than an
+active-mode injection, helper-split search or selected paid-word change. The
+selected source orientation passed at main
+`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8, selected
+conditional kappa .003125804. No selected assumption is discharged.
+
+## Reproduction and evidence
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/shared-fourier-translation-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/shared-fourier-translation-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-fourier-translation-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-fourier-translation-floor --check-source-history
+```
+
+Use another CPython 3.12 path on other machines. The direct marker is
+`PASS_SHARED_FOURIER_TRANSLATION_FLOOR`. The verifier prints a generated JSON
+receipt with all seven package hashes, both live source hashes and an ordered
+scientific digest. It writes no receipt into the checkout. There are no
+numerical tolerances or floating-point acceptance checks; the field is
+Q(sqrt(2),sqrt(3),i).
+
+The fixed finite evidence includes the algebraic field relations, all 512
+basis associativity triples, the exact polynomial identity proving the
+scalar maximum, 560 rational scalar grid points, and literal three-pass Fourier
+circuits. Sixteen group/offset fixtures check all 772 basis-input pairs.
+The minimizers cover every nonzero order-two offset in Z/2, Z/4, (Z/2)²,
+Z/8, Z/2 x Z/4 and (Z/2)³.
+A separate coefficient interpreter and the scalar-moment formula agree.
+The finite phase catalogue checks all 1,332 assignments from
+{1,-1,i,-i,(3+4i)/5,(3-4i)/5} on Z/2 and Z/4; twelve selected assignments also
+receive 120 literal basis-pair checks of the Parseval normalization.
+
+Controls reject malformed groups, zero and wrong-order translations,
+nonunit weights and invalid field values. They distinguish the attaining
+global phase, final conjugation and inverse Fourier sign. Separate forward
+and final weights give an exact zero-error escape, verifying that the shared
+contract matters. The unweighted translated routine has squared error two.
+Acceptance checks remain enabled under `-O`.
+
+The universal theorem rests on the written proof, not the finite catalogue.
+Independent human and formal proof-kernel review are unclaimed. No selected
+cold replay, Lean, Docker, native implementation or complete multiplier was run.
+
+## Bounds on the checker
+
+The checker has no recursion and no unbounded search. Functions are below
+60 physical lines. Its exact field has eight rational coefficients, groups
+have at most eight elements and three axes, and the largest phase product has
+6^4 assignments. The root-power loop has at most seven iterations. Local
+source inputs are limited to 1 MB each. Correctness checks raise explicit
+exceptions and survive optimized execution.
+
+Power-of-Ten rule 3 requires a managed-runtime deviation. Python, dataclasses,
+Fraction arithmetic, hashing and JSON allocate while checking. This is confined
+to the fixed finite replay above, which has no user-sized mathematical inputs
+or retained process cache. The command ends after one bounded replay and writes
+only to stdout. The compensating controls are the explicit domain limits,
+normal and optimized complete execution and capacity-rejection control.
+A fixed-storage port would be needed before using this checker in a setting
+that forbids runtime allocation. Rule 9 also has a narrow test-only deviation:
+the rejection helper calls one of eight closed local lambdas, never external
+callbacks. Warning-strict direct execution and registered replay are the
+available Python diagnostics; no repository-wide analyzer is added.
+
+## Open next questions
+
+1. What is the sharp shared-routine error for translations of order greater
+   than two? The balanced sign reduction no longer applies. Start with Z/3
+   and derive the corresponding constrained character-moment problem before
+   any numerical search. This would distinguish a general translation barrier
+   from the order-two theorem. The unresolved moment optimization is the blocker.
+2. What is the sharp error on arbitrary unit-norm input pairs? The coefficient
+   and worst basis-pair norms here do not determine that bilinear operator
+   norm. Start by using the two-output formula for the exhibited minimizer,
+   then establish a matching lower bound over all phases. An optimizer for
+   that different norm and physical implementation costs remain open.
+
+The structured questions are in [TASK.json](TASK.json). No further scope is
+reserved, and the first proved improvement is the result packaged here.
+
+## Credit and limits
+
+Credit Hanson Sun / bbMisk for PR1477's interface and exact theorem, Ross
+Richardson for PR940, and the retained manuscript, Fourier and analytic
+contributors for the normalization and construction context. Predecessor
+files and credit lines are unchanged. [SOURCES.json](SOURCES.json) pins the
+predecessor contract and original resampling section. No executable source
+or scientific receipt is borrowed from a predecessor.
+
+The attaining algebraic phases are not a priced Gaussian-dyadic program.
+Separate weights, other read maps, input restrictions or nonunit weights
+change the hypotheses. There is no uniform relative-error claim for inputs
+whose exact convolution vanishes. Native maps, restoration, movement,
+precision/storage costs, the complete paid invoice, supplier admission and
+all five selected framework assumptions retain their prior status.

research/shared-fourier-translation-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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"
+    },
+    {
+      "path": "research/weighted-fourier-layout/README.md",
+      "usage": "input",
+      "git_blob": "7cd23891f12ea1f054ed778289bc45a7e8fb622e",
+      "sha256": "676e107f9e312a36793ec87ca9eec3df3c8764c71268153055c2d6064a40e79e"
+    },
+    {
+      "path": "upstream/build/sections/07-resampling.tex",
+      "usage": "input",
+      "git_blob": "256243bf9416baefb82bf9203f80215b9ebe28f2",
+      "sha256": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c"
+    }
+  ]
+}