Prove the exact input-dimension price of unequal Fourier reads

research/fourier-input-defect/PROOF.md

@@ -0,0 +1,133 @@
+# The exact input-dimension price of a mismatched Fourier layout
+
+This scoped proof was produced by Nick Petalas. It changes the second-input
+contract of Hanson Sun / bbMisk's PR #1477. Its full-input convolution criterion
+and Ross Richardson's unweighted PR #940 are predecessor results, not claims
+rechecked here. The cycle argument below is classical weighted-permutation
+linear algebra. The contribution is the exact maximal-input contract, its
+sharp codimension and the resulting unequal-layout convolution construction.
+
+## 1. Contract
+
+Let G be a finite abelian group of order N with a nondegenerate symmetric
+character pairing chi. Use the predecessor's normalization
+
+    F^-u(y) = (1/N) sum_x chi(-y,x) u(x),
+    F^+u(x) = (1/N) sum_y chi(x,y) u(y).
+
+Then F^+ F^- = I/N. Let tau be any permutation of G.
+Let alpha and beta be fixed unit complex functions, and put h=alpha beta.
+Use read permutations P_tau g(y)=g(tau(y)). Consider
+
+    B(u,v) = F^+ [ (D_alpha F^-u) . (D_beta P_tau F^-v) ].
+
+Here . is coordinatewise multiplication and convolution * is unnormalized.
+The first input u is unrestricted. The second input v ranges over a complex
+linear subspace V. The question is which V satisfy
+
+    B(u,v) = (u*v)/N^2                 for every u and every v in V.   (1)
+
+Only the second forward read map and the two forward weights change. The
+first forward read map and the final Fourier map stay in their standard
+charts. No free physical implementation of any change is assumed.
+
+## 2. The maximal space and its exact dimension
+
+For a permutation cycle C define H_C=product_(y in C) h(y). Write b(tau,h)
+for the number of cycles with H_C=1, including singleton cycles. Define
+
+    K = {g in C^G : g(y)=h(y)g(tau(y)) for every y},
+    V_max = (F^-)^-1 K.
+
+**Theorem.** Equation (1) holds if and only if V is contained in V_max.
+Moreover,
+
+    dim_C V_max = b(tau,h),
+    codim_C V_max = N - b(tau,h).                                  (2)
+
+Every allowed dimension up to b is attained by a subspace of V_max. Thus
+(2) is the exact number of independent complex input dimensions that must
+be removed for these fixed maps and weights. It is not a paid-call count.
+
+**Proof.** The convolution theorem in the stated normalization gives
+
+    F^+ [(F^-u).(F^-v)] = (u*v)/N^2.
+
+Since F^+ is invertible, (1) is equivalent, at each y, to
+
+    (F^-u)(y) [ h(y)(F^-v)(tau(y)) - (F^-v)(y) ] = 0.               (3)
+
+Choosing u=delta_0 makes every first factor 1/N. Consequently (3) for all
+u is equivalent to F^-v belonging to K. This proves both directions and
+the maximality assertion. An arbitrary subset of inputs also satisfies
+(1) precisely when it is a subset of V_max.
+
+On a cycle C=(y_0,...,y_(ell-1)) with tau(y_j)=y_(j+1), set g(y_0)=c.
+The equations determine
+
+    g(y_j) = c / product_(k=0)^(j-1) h(y_k).
+
+Closing the cycle requires c=H_C c. If H_C differs from one, c=0. If
+H_C=1, c is arbitrary and contributes exactly one complex dimension.
+Cycles have disjoint support, so their dimensions add. Fourier inversion
+preserves dimension. This proves (2). For each balanced cycle, the above
+vector with c=1, zero off C, gives an explicit basis vector g_C of K;
+the vectors N F^+g_C give an attaining basis of V_max. QED.
+
+The formula recovers full-input rigidity in this fixed chart. Dimension N
+is possible exactly when every cycle is a singleton and its phase is one,
+that is, tau=id and h=1 pointwise. Nonconstant alpha remains possible when
+beta=alpha^-1. This does not address the predecessor's separate contract
+in which the same weighted routine also determines the inverse map.
+
+## 3. Translation layouts become character-level sparse inputs
+
+Let tau(y)=y+b and let h(y)=lambda be constant of modulus one. If b has
+order d, every permutation cycle has length d. The theorem gives
+
+    dim V_max = N/d if lambda^d=1, and 0 otherwise.                 (4)
+
+More explicitly,
+
+    V_max = {v : supp(v) is contained in
+                 {x in G : chi(b,x)=lambda}}.                     (5)
+
+Indeed, on the time coordinate delta_x, translation of its negative-sign
+Fourier character multiplies it by chi(-b,x). The kernel equation is
+lambda chi(-b,x)=1, equivalently chi(b,x)=lambda. Those time coordinates
+form a basis, so they prove (5). Nondegeneracy makes x -> chi(b,x) a
+character of order d. Its image is all d-th roots, and each level has
+N/d points, also proving (4) directly.
+
+For a concrete nonzero-output construction, take G=(Z/4)^2 with the usual
+pairing, b=(1,0), and lambda=i. Then
+
+    V_max = {v : v(x_0,x_1)=0 whenever x_0 is not 1},
+    dim V_max = 4, codim V_max = 12.
+
+For every arbitrary sixteen-coordinate u and every such four-coordinate
+v, reading the second negative Fourier spectrum at y+(1,0), multiplying
+that forward product by i, and applying the unchanged positive Fourier
+map computes (u*v)/256 exactly. The bound is sharp for this fixed wrapper:
+no five-dimensional complex linear second-input space works. Alpha and
+beta may split the factor i arbitrarily, as only their product occurs.
+
+This permits unequal read maps on a quantified sparse-input contract. It
+does not permit the same change on arbitrary second inputs, and it does
+not prove that the sparse representation or shifted reads are free.
+
+## 4. Evidence and limits
+
+The proof above is the unbounded finite-dimensional claim. The accompanying
+verifier independently realifies I-D_h P_tau over Q and computes its rank,
+constructs the cycle basis, and compares literal Fourier products with
+direct convolution over Gaussian integers. Its Fourier transforms are
+unnormalized, so it checks F_raw^+(F_raw^-u . F_raw^-v)=N(u*v).
+Its finite domains and rejection controls are specified in README.md.
+
+No selected framework assumption is discharged. Arbitrary changes to the
+final map, restrictions coupling the two operands, approximation, nonlinear
+address maps on actual tapes, native realization, input preparation,
+ownership/restoration, physical movement, precision, stock, complete cost,
+supplier admission and the multiplication theorem are outside this proof.
+Independent human and formal proof-kernel review are unclaimed.

research/fourier-input-defect/README.md

@@ -0,0 +1,130 @@
+# The exact input price of unequal Fourier read maps
+
+For a fixed phase-weighted permutation of the second Fourier spectrum, this
+package proves the largest linear second-input space on which convolution
+still works with every unrestricted first input. If tau is the read
+permutation and h is the product of the two forward phases, then
+
+    maximum complex input dimension
+      = number of cycles C of tau with product_(y in C) h(y) = 1.
+
+The sharp codimension is N minus that count. An explicit cycle basis attains
+the bound. This is a scoped mathematical proof with exact finite
+corroboration. It is not a paid-call saving or a new kappa.
+
+The changed hypothesis is deliberate. Hanson Sun / bbMisk's
+[PR #1477](https://github.com/CrocSwap/integer-mult-bounds/pull/1477) requires
+both operands to be arbitrary and characterizes the allowed full-input
+layouts. This contribution restricts the second operand, fixes the standard
+first and final Fourier charts, and computes the exact price in input
+dimension of a mismatched second read. The predecessor is cited rather than
+audited. [PROOF.md](PROOF.md) gives the complete statement and proof.
+
+## A nonzero sparse-input construction
+
+For translation tau(y)=y+b with b of order d and constant h=lambda, the
+maximal input space is exactly
+
+    {v : supp(v) is contained in {x : chi(b,x)=lambda}}.
+
+Its dimension is N/d if lambda^d=1, and zero otherwise. In G=(Z/4)^2,
+b=(1,0), lambda=i permits every second input supported on x_0=1. This
+four-dimensional space is maximal among all linear second-input spaces,
+including dense ones, for that fixed wrapper. Every sixteen-dimensional
+first input is allowed. The unequal-read wrapper returns (u*v)/256 in the
+predecessor's normalization. A five-dimensional second-input space is
+impossible. This is an algebraic construction; physical routing and
+preparation costs remain unpriced.
+
+## Evidence and reproduction
+
+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/fourier-input-defect/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/fourier-input-defect/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fourier-input-defect
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fourier-input-defect --check-source-history
+```
+
+Substitute another CPython 3.12 executable elsewhere. The direct marker is
+`PASS_FOURIER_INPUT_DEFECT`. Verification writes a generated JSON receipt to
+stdout, binding the six package file hashes and an ordered classification
+digest. No receipt is hand-authored or written into the checkout.
+
+The independent rational-rank oracle realifies I-D_h P_tau. Its rank must
+equal twice the asserted complex codimension. The cycle solver uses a
+different representation and constructs every allowed basis vector.
+Literal Fourier transforms over Gaussian integers are compared with direct
+group-addition convolution, including a nonconstant split of h between the
+two forward phase maps. All acceptance checks remain active under `-O`.
+
+The fixed replay covers:
+
+- All 6,564 permutations with fourth-root phase assignments at dimensions
+  one through four, with 13,556 cycles and 3,389 balanced cycle vectors.
+- All 12,324 layouts on the trivial group, Z/2, Z/4 and (Z/2)^2. These give
+  25,625 accepted convolution basis pairs, 6,413 dense first operands and
+  46,139 forbidden-coordinate witnesses. The dimension-three fixtures
+  receive rank and kernel checks, with no Z/3 Fourier computation claimed.
+- All 104 translation/constant-phase fixtures on Z/2, Z/4, (Z/2)^2 and
+  (Z/4)^2, checking 1,168 time-coordinate columns against character-level
+  support, plus all 64 input basis pairs for the explicit sparse example.
+- Seven malformed-domain rejections and three semantic controls that
+  distinguish unbalanced cycles, nonconstant balanced cycle vectors and
+  the incorrect constant-vector rule.
+
+The card's first command, `scripts/research_selected_baseline.py`, passed
+with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. It was source orientation,
+not a scientific replay. Hosted CI is separate from local verification.
+
+## Scope and implementation
+
+The written proof covers every finite abelian group with its standard
+nondegenerate symmetric pairing, arbitrary permutations and arbitrary unit
+complex phases. The finite replay uses fourth roots and the bounded groups
+listed above. Neither claim extends to arbitrary changes of the final map,
+coupled restrictions on both operands, or approximate equality.
+
+No actual physical caller, sparse-input preparation, ownership/restoration,
+movement, native circuit, precision/storage bound, stock, complete supplier
+invoice, selected framework assumption, supplier admission or multiplication
+theorem is established. Independent human and formal proof-kernel review are
+unclaimed. No predecessor scientific replay, selected cold replay, Lean or
+Docker run is part of this contribution.
+
+The checker has no recursion, subprocesses, dynamic imports or filesystem
+mutations. Exhaustive permutation/phase loops stop at dimension four;
+translation and Fourier helpers stop at sixteen coordinates; rank matrices
+have at most 32 rows and columns. Every function is below sixty lines. Source
+reads are capped at one MiB and the source inventory at eight rows. All
+arithmetic is integer or Fraction arithmetic. Power of Ten rule 3 has a
+managed-runtime deviation: CPython allocates objects during execution.
+The fixed domains bound live mathematical data, and fixtures are streamed.
+Larger domains require a new capacity assessment. Warning-strict normal and
+optimized execution and AST inspection provide the available diagnostics;
+no repository-wide diagnostic configuration is changed.
+
+## Sources and credit
+
+[SOURCES.json](SOURCES.json) pins the unchanged predecessor README at
+canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`. The runtime checks
+its SHA256 without executing its scientific code. [TASK.json](TASK.json)
+records the changed side-result scope under `uniform-transfer-audit`.
+The selected frontier is unchanged.
+
+This contribution was produced by Nick Petalas. Credit Hanson Sun / bbMisk
+#1477 for the weighted Fourier interface, full-input boundary and
+normalization, Ross Richardson #940 for its unweighted predecessor, and
+the retained Fourier/construction lineage. Weighted-permutation cycle
+decomposition, character orthogonality and rank-nullity are classical;
+literature priority for those methods is unclaimed. Apache-2.0.
+
+## Open next questions
+
+Can an actual convolution caller provide a character-level sparse operand
+and absorb the shifted read and phase at a favorable complete cost? Start
+with one literal operand and translation, prove its support contract, then
+charge preparation, movement, restoration, precision and the complete
+wrapper. No such caller or invoice is supplied here. The exact dimension
+formula alone does not make the changed layout a cheaper supplier.

research/fourier-input-defect/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "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"
+    }
+  ]
+}

research/fourier-input-defect/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact maximal complex-linear second-input space admitting a phase-weighted mismatched Fourier read, while the first input is arbitrary and the first/final maps are standard.",
+  "scope_change_reason": "Changed-contract side result from PR1477: restrict the second operand instead of auditing or replaying the full-input criterion. This is not discharge of a selected framework assumption.",
+  "bottleneck_link": "Side result: quantifies exactly which restricted-input producer could legally feed an unequal-layout convolution wrapper. A complete physical caller and invoice remain absent.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after proving the dimension formula and attaining basis, checking the fixed small exact domain, and packaging one PR. No larger search or supplier claim.",
+  "outcome": "completed",
+  "evidence": "Written cycle-kernel proof in PROOF.md; verify.py independently computes rational realification ranks, literal Gaussian-integer Fourier/convolution identities, forbidden-input witnesses and translation support.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual convolution caller supply one of these character-level input spaces and absorb the shifted read and phase at a favorable complete cost?",
+      "why_it_matters": "The exact input restriction can replace full-input layout rigidity only if a real caller satisfies it.",
+      "first_step": "Choose an actual sparse operand and an explicit translated read, then charge preparation, movement, restoration, precision and the whole wrapper.",
+      "blocked_by": "No physical caller or complete invoice is supplied."
+    }
+  ]
+}