Classify common CRT Fourier permutations, including nonlinear maps (no κ)

research/crt-fourier-common-permutation/PROOF.md

@@ -0,0 +1,145 @@
+# One permutation on both Fourier indices
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let `D >= 1`, and let `s_1,...,s_D >= 2` be pairwise-coprime integers.
+Put `N = product_i s_i`, `M_i = N/s_i`, and
+`G = product_i Z/(s_i)`. Representatives are canonical integers.
+Use the standard positive-exponent, unnormalized Fourier kernels
+
+```text
+K_N(a,b) = exp(2 pi i a b / N),
+K_G(x,y) = exp(2 pi i sum_i x_i y_i / s_i).
+```
+
+The same statements hold with both exponent signs reversed, or with the
+usual unitary normalization on both sides. Normalizing just one side does
+not give the displayed identity.
+
+A bijection `f: G -> Z/(N)` satisfies
+
+```text
+K_N(f(x), f(y)) = K_G(x,y)                  for every x,y in G       (1)
+```
+
+if and only if it has the form
+
+```text
+f(x) = sum_i M_i v_i x_i mod N,
+M_i v_i^2 = 1 mod s_i                     for every i.             (2)
+```
+
+Consequently, such an `f` exists exactly when every `M_i` is a square
+unit modulo `s_i`. The number of such bijections is the product of the
+numbers of solutions to the local congruences in (2). These are all the
+solutions, even when the initial search allows arbitrary nonlinear
+permutations.
+
+This is an exact interface classification. Local roots are fixed to the
+standard roots in the displayed kernels. There are no extra diagonal
+phases, changes of local primitive root, different permutations on the two
+indices, or arbitrary linear input/output transforms.
+
+## Necessity, including arbitrary bijections
+
+Equality of the two roots of unity in (1) is equivalent to
+
+```text
+f(x) f(y) = sum_i M_i x_i y_i mod N.                                (3)
+```
+
+Since `f` is onto, there is a `y_*` with `f(y_*) = 1`. Taking `x=0` in
+(3) gives `f(0)=0`. For any `x,x',y`, subtract the three instances of (3)
+at `(x+x',y)`, `(x,y)` and `(x',y)`. The right sides cancel modulo `N`,
+including any coordinate wrap, because `M_i s_i=N`. Thus
+
+```text
+(f(x+x') - f(x) - f(x')) f(y) = 0 mod N.
+```
+
+Take `y=y_*`. It follows that `f` is a group homomorphism. Nonlinear
+bijections cannot evade this conclusion.
+
+Let `e_i` be the unit vector in factor `i`. Since `s_i e_i=0`, additivity
+gives `s_i f(e_i)=0 mod N`. Hence `M_i` divides the canonical integer
+`f(e_i)`, and `f(e_i)=M_i v_i` for a unique `0<=v_i<s_i`. Every group
+homomorphism is determined by these images, so `f` has the stated form.
+Taking `x=y=e_i` in (3) gives
+
+```text
+M_i^2 v_i^2 = M_i mod N.
+```
+
+Divide the integer divisibility statement by `M_i` to obtain
+`M_i v_i^2=1 mod s_i`. In particular `v_i` and `M_i` are units modulo
+`s_i`. Then `M_i=(v_i^-1)^2 mod s_i`, proving the square-unit condition.
+
+## Sufficiency and exact count
+
+Suppose (2) holds. Modulo `s_i`, all terms of `f` except its `i`th term
+vanish. The surviving coefficient `M_i v_i` is a unit. Thus the reductions
+of `f` are independent invertible rescalings on the factors. The Chinese
+remainder theorem proves that `f` is a bijection.
+
+For distinct indices `i,j`, `N` divides `M_i M_j`. Expanding `f(x)f(y)`
+therefore removes every cross term modulo `N`. Each remaining diagonal
+term is `M_i^2 v_i^2 x_i y_i = M_i x_i y_i mod N`, by (2). This proves
+(3), and hence (1).
+
+If `M_i=w_i^2 mod s_i` for a unit `w_i`, take `v_i=w_i^-1`. This proves
+existence from the square-unit condition. Finally, independent choices of
+the `v_i` give distinct images of the generators `e_i`, so their product
+counts all maps without duplication. QED.
+
+## Explicit positive and negative instances
+
+For axes `(13,17)`, all four coefficient tuples `f(e_1),f(e_2)` are
+
+```text
+(102,26), (102,195), (119,26), (119,195).
+```
+
+For example `102^2=17 mod 221`, `26^2=13 mod 221`, and `102*26=0 mod 221`.
+The map `f(x,y)=102x+26y mod 221` is a bijection and identifies every one
+of the `221^2` Fourier phases. The verifier checks each of the four maps.
+
+For `(3,5)`, the complementary product `5=2 mod 3` is a nonsquare, so no
+common permutation exists. For `(3,7)`, the first local test passes but
+`3 mod 7` is a nonsquare, so the second test excludes every permutation.
+This illustrates why testing just one axis is insufficient.
+
+These exclusions do not forbid ordinary Good–Thomas tensorization. With
+`u_i=M_i^-1 mod s_i`, its two address maps are
+
+```text
+a(x)=sum_i M_i u_i x_i mod N,
+b(y)=sum_i M_i y_i mod N.
+```
+
+They satisfy the two-map Fourier identity for every pairwise-coprime grid,
+including the two excluded shapes. This is the predecessor interface of
+David Ganz / Dugongue's PR5564, not a new result here. The new question is
+whether its two indices can share a single permutation while preserving
+standard local roots. No criticism of its distinct-map convention is implied.
+
+## Proof and execution boundaries
+
+The universal theorem is the written argument above. The exact Python
+reference enumerates local roots and independently enumerates cyclic
+homomorphisms through their generator images, then compares the resulting
+maps using integer phase congruences. Complete tiny permutation domains
+also include every nonlinear bijection and every translation. These finite
+checks corroborate the theorem; they do not establish its quantifiers by
+extrapolation. Neither floating-point Fourier matrices nor approximate
+phase equality are used.
+
+The constructor is an offline bounded reference, not an efficient modular
+square-root algorithm or a native physical program. Root testing can take
+linear time in an axis value, and emitting a permutation takes `N` entries.
+No reduced head movement, storage, coefficient-generation cost, rounded
+resampling, complete paid recurrence, supplier admission or new kappa is
+inferred. Standard-root phase conventions must be matched before applying
+the theorem to a particular physical caller. The five selected framework
+assumptions are unchanged.

research/crt-fourier-common-permutation/README.md

@@ -0,0 +1,122 @@
+# Exact common-permutation criterion for CRT Fourier tensorization
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration.
+For pairwise-coprime cyclic axes `s_i`, put `N=product_i s_i` and `M_i=N/s_i`.
+A single address permutation identifies both indices of the length-N standard
+Fourier kernel with the tensor of the standard axis kernels exactly when
+**every `M_i` is a square unit modulo `s_i`**. This remains necessary when
+arbitrary nonlinear permutations are allowed. Every valid map is
+
+```text
+f(x) = sum_i M_i v_i x_i mod N,     M_i v_i^2 = 1 mod s_i.
+```
+
+[PROOF.md](PROOF.md) proves the classification and its exact product count.
+Axes `(13,17)` have four common maps, including `102x+26y mod 221`.
+Axes `(3,5)` and `(3,7)` admit none. Ordinary two-map Good–Thomas
+factorization still works on all three grids. No new kappa is claimed.
+
+## Connection to the current problem
+
+David Ganz / Dugongue's [PR5564](https://github.com/CrocSwap/integer-mult-bounds/pull/5564)
+supplies prime-free native coprime grids and distinguishes their two CRT
+address conventions. This originally posed question changes that interface
+by demanding exactly the same permutation on both Fourier indices, while
+retaining standard local roots. It settles which grids permit that demand.
+It does not audit the predecessor or assert that its distinct-map contract
+needs replacement. The result is a side interface theorem relevant to
+transform-layout design, not a change to the binding recursive invoice.
+
+Nonlinear reindexing cannot fix a failed square test. Different input/output
+permutations or changed local roots remain available. Their physical costs
+must be charged separately. No permutation-cost saving is claimed here.
+
+## Reproduce
+
+CPython 3.12 and the standard library suffice. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/crt-fourier-common-permutation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/crt-fourier-common-permutation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/crt-fourier-common-permutation
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/crt-fourier-common-permutation --check-source-history --check-modes
+```
+
+Other machines may substitute their CPython 3.12 path. The direct marker is
+`PASS_CRT_FOURIER_COMMON_PERMUTATION`. Stdout is a generated JSON receipt
+bound to all six package files and both exact source inputs. No receipt is
+handwritten. Direct replay needs no Git, network, predecessor executable or
+output directory, and writes no files. Materialize `research/native-coprime-grid`
+in a sparse checkout before replay. The official package export includes
+both inputs and supports the same direct commands without Git.
+
+Local normal and optimized runs agree on 105 coprime shapes, 7,313 cyclic
+candidates, 147 constructed common maps and 887,566 literal phase entries
+for those maps. There are sixty excluded shapes. The tiny domains enumerate
+all 1,592 permutations, accepting nine, all additive. The four `(13,17)`
+maps receive another 195,364 phase checks. Three distinct-map scope controls
+cover 1,066 phase entries, and fourteen invalid-input or semantic controls
+reject. Full phase tests use exact congruences modulo N. Only the written
+proof makes the all-axis-size and arbitrary-bijection claims.
+
+Both registered commands ran locally in about one second each on CPython
+3.12.15, macOS arm64, far below their 120-second bounds. These are local
+check timings, not a performance-improvement or portable-runtime claim.
+
+## Scope and credit
+
+Base canonical main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority
+revision 8, selected conditional kappa `.003125804`. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294771)
+records the original interface question. TASK.json changes the
+`uniform-transfer-audit` card to this side result. No selected assumption is
+discharged. Live open PRs, handoffs, active Discussions, recent account work,
+main README formulas and several merged/all-state object searches were
+checked. Sparse/cache coverage and unpublished work remain limits; empty
+searches are not a novelty proof.
+
+Credit David Ganz / Dugongue for PR5564's native interface, two address
+conventions and context; ToikY for the guard-safe band, Jose Manuel for the
+tensor caller, Tekalign for the earlier CRT streams, and Cinna Davis,
+Chafik Boukhalfa, unpaidmoon and the retained native/tensor/CRT lineage.
+The cited setup and source statements are authenticated inputs, not scientific
+claims re-verified as this contribution. CRT, finite cyclic characters,
+congruence-preserving bilinear forms and Good–Thomas tensorization are
+classical. The contribution is the complete common-permutation criterion at
+this interface, including nonlinear permutations, its constructor and exact
+corroboration. No broad literature-priority claim is made. Predecessor files
+and credit lines are unchanged.
+
+The physical permutation, local roots, numerical resampling, coefficient
+preparation, restoration, precision/tape, stock and complete caller costs
+remain open. No native instruction trace, new supplier, full multiplication
+theorem, selected cold replay, Lean or Docker is supplied. Independent human
+and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. Can one actual caller exploit a successful common-permutation grid after
+   its standard local roots and full movement costs are fixed? Begin with
+   one complete transform and its input/output ABI. A grid alone supplies
+   no physical saving.
+2. When a grid fails the criterion, can an explicitly priced local root
+   change make a common permutation cheaper than retaining the two maps?
+   Begin with `(3,5)` and charge phase generation and the complete transform.
+   Neither route is excluded by this theorem.
+
+Structured questions and blockers are in [TASK.json](TASK.json).
+
+## Verifier constraints
+
+Power-of-ten inspection covers the new verifier. It has no recursion,
+subprocesses, imports of predecessor engines, network operations or file
+writes. Functions are below 60 lines. Input reads are capped at one MiB,
+source rows at sixteen, axis count at four, each axis at 257 and total size
+at 65,536. The actual exhaustive shapes have N at most 255; arbitrary
+permutations have N at most six. All checks use explicit exceptions that
+remain active under optimization. The normal and optimized warning-strict
+replays are the available diagnostics. Rule 3 has a managed-runtime deviation:
+CPython allocates integers and containers. These fixed finite bounds constrain
+live collections; no fixed-allocation native implementation is claimed.

research/crt-fourier-common-permutation/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/native-coprime-grid/PROOF.md",
+      "usage": "input",
+      "git_blob": "7e202209c9844e77fef9835fdf494cc04ad37ae2",
+      "sha256": "aa02a23e16c575968f381569a33b1126003ce57e144a05262c667d80881e6bee"
+    },
+    {
+      "path": "research/native-coprime-grid/README.md",
+      "usage": "input",
+      "git_blob": "85a3c8d7a1e3e3b2a45451472707ce8281233c40",
+      "sha256": "c180783791bf1b43d9682d77f3811a6d564ee216c82b4e8bfc5920c7275da4c0"
+    }
+  ]
+}

research/crt-fourier-common-permutation/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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": "Classify all common input/output address permutations for standard cyclic Fourier tensorization on pairwise-coprime axes, without assuming the permutation additive.",
+  "scope_change_reason": "Originally posed Fourier/CRT layout interface question following PR5564, rather than an audit or discharge of a selected all-size assumption.",
+  "bottleneck_link": "Side result: an exact obstruction and constructor for a changed transform-layout contract. No change to the binding signed moment or claimed physical saving.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved classification with exact finite phase and arbitrary-permutation corroboration. Do not expand to a new native caller.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and the generated hash-bound stdout of verify.py; universal claims rest on the written proof.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a real caller use a successful common-permutation grid profitably?",
+      "why_it_matters": "It could change a transform layout, but a grid is not a physical saving.",
+      "first_step": "Fix standard local roots and a complete input/output ABI, then price the full permutation and transform.",
+      "blocked_by": "No emitted native caller or full physical movement bill is supplied."
+    },
+    {
+      "question": "At a failed grid, can paid local root changes beat two distinct CRT maps?",
+      "why_it_matters": "The square obstruction only covers fixed standard roots.",
+      "first_step": "Compare both complete routes at axes (3,5), including phase generation.",
+      "blocked_by": "Local phase preparation, numerical compatibility and full cost comparison remain absent."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294771"
+}