From 04a5da5ce867cc965103094b8e52d51368291fac Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:22:25 +0000 Subject: [PATCH] feat(research): prove exact restricted Fourier input dimension --- research/fourier-input-defect/PROOF.md | 133 +++++++++ research/fourier-input-defect/README.md | 130 +++++++++ research/fourier-input-defect/SOURCES.json | 24 ++ research/fourier-input-defect/TASK.json | 83 ++++++ research/fourier-input-defect/VERIFY.json | 36 +++ research/fourier-input-defect/verify.py | 308 +++++++++++++++++++++ 6 files changed, 714 insertions(+) create mode 100644 research/fourier-input-defect/PROOF.md create mode 100644 research/fourier-input-defect/README.md create mode 100644 research/fourier-input-defect/SOURCES.json create mode 100644 research/fourier-input-defect/TASK.json create mode 100644 research/fourier-input-defect/VERIFY.json create mode 100644 research/fourier-input-defect/verify.py diff --git a/research/fourier-input-defect/PROOF.md b/research/fourier-input-defect/PROOF.md new file mode 100644 index 0000000000..c227a1879b --- /dev/null +++ b/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. diff --git a/research/fourier-input-defect/README.md b/research/fourier-input-defect/README.md new file mode 100644 index 0000000000..b5de379be2 --- /dev/null +++ b/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. diff --git a/research/fourier-input-defect/SOURCES.json b/research/fourier-input-defect/SOURCES.json new file mode 100644 index 0000000000..b0149e9d0b --- /dev/null +++ b/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" + } + ] +} diff --git a/research/fourier-input-defect/TASK.json b/research/fourier-input-defect/TASK.json new file mode 100644 index 0000000000..896dd09dad --- /dev/null +++ b/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." + } + ] +} diff --git a/research/fourier-input-defect/VERIFY.json b/research/fourier-input-defect/VERIFY.json new file mode 100644 index 0000000000..7c62f40087 --- /dev/null +++ b/research/fourier-input-defect/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/weighted-fourier-layout/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact weighted-cycle dimensions versus independent rational rank; literal Fourier/convolution identities; forbidden directions, sparse construction, source hashes and boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "The same complete finite domain with optimized Python, retaining every acceptance check." + } + ] +} diff --git a/research/fourier-input-defect/verify.py b/research/fourier-input-defect/verify.py new file mode 100644 index 0000000000..c712b102de --- /dev/null +++ b/research/fourier-input-defect/verify.py @@ -0,0 +1,308 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration of the restricted Fourier-input theorem.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + + +ROOTS = ((1, 0), (0, 1), (-1, 0), (0, -1)) +ZERO = (0, 0) +ONE = (1, 0) +MAX_N = 16 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(left, right): + return (left[0] + right[0], left[1] + right[1]) + + +def multiply(left, right): + a, b = left + c, d = right + return (a * c - b * d, a * d + b * c) + + +def conjugate(value): + return (value[0], -value[1]) + + +def validate(permutation, phases): + n = len(permutation) + require(1 <= n <= MAX_N, "permutation size") + require(all(type(x) is int for x in permutation), "integer addresses") + require(sorted(permutation) == list(range(n)), "bijection") + require(len(phases) == n, "phase count") + require(all(x in ROOTS for x in phases), "fourth-root phase") + + +def cycle_basis(permutation, phases): + """Solve g[y] = h[y] g[tau(y)] with an explicitly bounded walk.""" + validate(permutation, phases) + n = len(permutation) + visited = set() + basis, cycles = [], [] + for start in range(n): + if start in visited: + continue + vector = [ZERO] * n + cycle = [] + index, value = start, ONE + for _ in range(n): + require(index not in visited, "cycle intersects an earlier cycle") + visited.add(index) + cycle.append(index) + vector[index] = value + value = multiply(value, conjugate(phases[index])) + index = permutation[index] + if index == start: + break + require(index == start, "cycle did not close") + cycles.append((tuple(cycle), value == ONE)) + if value == ONE: + basis.append(tuple(vector)) + require(len(visited) == n, "incomplete cycle cover") + return tuple(basis), tuple(cycles) + + +def residual(vector, permutation, phases): + return tuple(add(vector[y], multiply((-1, 0), + multiply(phases[y], vector[permutation[y]]))) + for y in range(len(vector))) + + +def vanishes(vector): + return all(value == ZERO for value in vector) + + +def real_matrix(permutation, phases): + """Independent realification of I - D_h P_tau.""" + n = len(permutation) + rows = [[0] * (2 * n) for _ in range(2 * n)] + for y in range(n): + rows[y][y] += 1 + rows[y + n][y + n] += 1 + a, b = phases[y] + z = permutation[y] + rows[y][z] -= a + rows[y][z + n] += b + rows[y + n][z] -= b + rows[y + n][z + n] -= a + return rows + + +def rational_rank(matrix): + require(1 <= len(matrix) <= 2 * MAX_N, "row bound") + width = len(matrix[0]) + require(1 <= width <= 2 * MAX_N, "column bound") + require(all(len(row) == width for row in matrix), "rectangular matrix") + rows = [[Fraction(x) for x in row] for row in matrix] + rank = 0 + for column in range(width): + pivot = next((r for r in range(rank, len(rows)) if rows[r][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + divisor = rows[rank][column] + rows[rank] = [x / divisor for x in rows[rank]] + for r in range(rank + 1, len(rows)): + scalar = rows[r][column] + rows[r] = [x - scalar * y for x, y in zip(rows[r], rows[rank])] + rank += 1 + if rank == len(rows): + break + return rank + + +def elements(moduli): + require(moduli in ((), (2,), (4,), (2, 2), (4, 4)), "group domain") + return tuple(product(*(range(q) for q in moduli))) + + +def character(left, right, moduli, sign=1): + exponent = sum((4 // q) * x * y for x, y, q in zip(left, right, moduli)) + return ROOTS[(sign * exponent) % 4] + + +def transform(vector, group, moduli, sign): + require(len(vector) == len(group) <= MAX_N, "transform domain") + result = [] + for x in group: + value = ZERO + for y, coefficient in zip(group, vector): + value = add(value, multiply(character(x, y, moduli, sign), coefficient)) + result.append(value) + return tuple(result) + + +def convolution(left, right, group, moduli): + """Direct group addition, without any Fourier or cycle routine.""" + result = [ZERO] * len(group) + positions = {x: i for i, x in enumerate(group)} + for a, x in enumerate(group): + for b, y in enumerate(group): + z = tuple((s + t) % q for s, t, q in zip(x, y, moduli)) + i = positions[z] + result[i] = add(result[i], multiply(left[a], right[b])) + return tuple(result) + + +def convolution_identity(left, right, permutation, phases, group, moduli): + first = transform(left, group, moduli, -1) + second = transform(right, group, moduli, -1) + alpha = tuple(ROOTS[y % 4] for y in range(len(group))) + beta = tuple(multiply(h, conjugate(a)) for h, a in zip(phases, alpha)) + mixed = tuple(multiply(multiply(a, u), multiply(b, second[z])) + for a, b, u, z in zip(alpha, beta, first, permutation)) + actual = transform(mixed, group, moduli, 1) + target = tuple(multiply((len(group), 0), v) + for v in convolution(left, right, group, moduli)) + return actual == target + + +def delta(n, index): + return tuple(ONE if j == index else ZERO for j in range(n)) + + +def check_fourier_fixture(permutation, phases, basis, moduli, counts): + group = elements(moduli) + n = len(group) + for spectral in basis: + right = transform(spectral, group, moduli, 1) + for x in range(n): + require(convolution_identity(delta(n, x), right, permutation, + phases, group, moduli), "attaining convolution basis") + counts["convolution_basis_pairs"] += 1 + dense = tuple((y + 1, 1 - y) for y in range(n)) + require(convolution_identity(dense, right, permutation, phases, + group, moduli), "dense first operand") + counts["dense_first_operands"] += 1 + for x in range(n): + spectral = delta(n, x) + if not vanishes(residual(spectral, permutation, phases)): + right = transform(spectral, group, moduli, 1) + require(not convolution_identity(delta(n, 0), right, permutation, + phases, group, moduli), "forbidden direction must fail") + counts["forbidden_direction_witnesses"] += 1 + + +def exhaustive(counts): + digest = sha256() + groups = {1: ((),), 2: ((2,),), 4: ((4,), (2, 2))} + for n in range(1, 5): + for permutation in permutations(range(n)): + for phases in product(ROOTS, repeat=n): + basis, cycles = cycle_basis(permutation, phases) + rank = rational_rank(real_matrix(permutation, phases)) + require(rank == 2 * (n - len(basis)), "independent rank formula") + for vector in basis: + require(vanishes(residual(vector, permutation, phases)), + "cycle vector fails its equations") + counts["weighted_permutations"] += 1 + counts["balanced_cycle_vectors"] += len(basis) + counts["cycles"] += len(cycles) + digest.update(bytes((n, *permutation, len(basis)))) + digest.update(bytes(ROOTS.index(h) for h in phases)) + for moduli in groups.get(n, ()): + check_fourier_fixture(permutation, phases, basis, moduli, counts) + counts["fourier_layouts"] += 1 + return digest.hexdigest() + + +def translations(counts): + for moduli in ((2,), (4,), (2, 2), (4, 4)): + group = elements(moduli) + positions = {x: j for j, x in enumerate(group)} + for shift in group: + permutation = tuple(positions[tuple((x + b) % q + for x, b, q in zip(y, shift, moduli))] for y in group) + for phase in ROOTS: + phases = (phase,) * len(group) + basis, _ = cycle_basis(permutation, phases) + support = tuple(x for x in group + if character(shift, x, moduli) == phase) + require(len(basis) == len(support), "translation dimension") + for x in group: + time = delta(len(group), positions[x]) + spectral = transform(time, group, moduli, -1) + accepted = vanishes(residual(spectral, permutation, phases)) + require(accepted == (x in support), "character-level support") + counts["translation_time_columns"] += 1 + counts["translation_layouts"] += 1 + moduli = (4, 4) + group = elements(moduli) + permutation = tuple(group.index(((y[0] + 1) % 4, y[1])) for y in group) + for x in group: + if x[0] == 1: + for u in range(len(group)): + require(convolution_identity(delta(16, u), delta(16, group.index(x)), + permutation, ((0, 1),) * 16, group, moduli), "sparse example") + counts["sparse_example_basis_pairs"] += 1 + + +def controls(counts): + malformed = [((0, 0), (ONE, ONE)), ((1,), (ONE,)), + ((True,), (ONE,)), ((), ()), ((0,), ()), + ((0,), ((2, 0),)), (tuple(range(17)), (ONE,) * 17)] + for permutation, phases in malformed: + try: + cycle_basis(permutation, phases) + except ValueError: + counts["rejection_controls"] += 1 + else: + raise ValueError("malformed boundary accepted") + permutation = (1, 2, 0) + basis, _ = cycle_basis(permutation, (ONE, ONE, (-1, 0))) + require(not basis, "unbalanced cycle counted") + basis, _ = cycle_basis(permutation, ((0, 1), (-1, 0), (0, 1))) + require(len(basis) == 1 and len(set(basis[0])) > 1, + "nonconstant balanced weights lost") + require(not vanishes(residual((ONE, ONE, ONE), permutation, + ((0, 1), (-1, 0), (0, 1)))), "constant cycle-vector mutant") + counts["rejection_controls"] += 3 + + +def source_hashes(): + package = Path(__file__).resolve().parent + paths = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result = {} + for name in paths: + path = package / name + require(path.stat().st_size <= 1024 * 1024, "package file bound") + result[name] = sha256(path.read_bytes()).hexdigest() + manifest = json.loads((package / "SOURCES.json").read_text()) + require(len(manifest["files"]) <= 8, "source manifest bound") + for row in manifest["files"]: + if row["usage"] == "input": + path = package.parents[1] / row["path"] + require(path.stat().st_size <= 1024 * 1024, "source file bound") + require(sha256(path.read_bytes()).hexdigest() == row["sha256"], "source drift") + return result + + +def main(): + hashes = source_hashes() + counts = dict.fromkeys(("weighted_permutations", "balanced_cycle_vectors", "cycles", + "fourier_layouts", "convolution_basis_pairs", "dense_first_operands", + "forbidden_direction_witnesses", "translation_layouts", + "translation_time_columns", "sparse_example_basis_pairs", + "rejection_controls"), 0) + digest = exhaustive(counts) + translations(counts) + controls(counts) + require(counts["weighted_permutations"] == sum( + len(tuple(permutations(range(n)))) * 4 ** n for n in range(1, 5)), + "exhaustive domain coverage") + print(json.dumps({"status": "PASS_FOURIER_INPUT_DEFECT", "counts": counts, + "classification_sha256": digest, "package_sha256": hashes, + "claim_type": "scoped proof with finite corroboration"}, sort_keys=True)) + + +if __name__ == "__main__": + main()