From f24bb18c20f7bdb3cbc27a1b6a010babf427d6cc Mon Sep 17 00:00:00 2001 From: Hanson Sun Date: Tue, 13 Oct 2026 21:24:10 -0400 Subject: [PATCH] Audit phase-weighted Fourier convolution layouts Add the exact monomial admission criterion, shared-conjugate phase rigidity, independent cyclotomic evidence and scoped failure controls. No new kappa or selected-source changes. Prepared with substantial OpenAI Codex assistance. --- .../weighted-fourier-layout/EXPECTED.json | 1373 +++++++++++++++++ research/weighted-fourier-layout/README.md | 261 ++++ research/weighted-fourier-layout/SOURCES.json | 43 + research/weighted-fourier-layout/TASK.json | 121 ++ research/weighted-fourier-layout/VERIFY.json | 32 + research/weighted-fourier-layout/oracle.py | 168 ++ .../weighted-fourier-layout/test_verify.py | 158 ++ research/weighted-fourier-layout/verify.py | 353 +++++ 8 files changed, 2509 insertions(+) create mode 100644 research/weighted-fourier-layout/EXPECTED.json create mode 100644 research/weighted-fourier-layout/README.md create mode 100644 research/weighted-fourier-layout/SOURCES.json create mode 100644 research/weighted-fourier-layout/TASK.json create mode 100644 research/weighted-fourier-layout/VERIFY.json create mode 100644 research/weighted-fourier-layout/oracle.py create mode 100644 research/weighted-fourier-layout/test_verify.py create mode 100644 research/weighted-fourier-layout/verify.py diff --git a/research/weighted-fourier-layout/EXPECTED.json b/research/weighted-fourier-layout/EXPECTED.json new file mode 100644 index 0000000000..dbed65d4a1 --- /dev/null +++ b/research/weighted-fourier-layout/EXPECTED.json @@ -0,0 +1,1373 @@ +{ + "additional_fixtures": [ + { + "common_denominator": 512, + "dense_output_numerator": [ + [ + -128, + 0 + ], + [ + -152, + 0 + ], + [ + 96, + 0 + ], + [ + -240, + 0 + ], + [ + -112, + 0 + ], + [ + 176, + 0 + ], + [ + 24, + 0 + ], + [ + -456, + 0 + ] + ], + "layout": { + "alpha": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "beta": [ + 3, + 2, + 3, + 2, + 1, + 0, + 1, + 0 + ], + "omega": [ + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0 + ], + "pi": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ], + "rho": [ + 7, + 4, + 5, + 6, + 1, + 2, + 3, + 0 + ], + "sigma": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ] + }, + "literal_basis_pairs": 64, + "moduli": [ + 2, + 4 + ], + "phase_order": 4 + }, + { + "common_denominator": 216, + "dense_output_numerator": [ + [ + -294, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0 + ], + [ + 138, + 0, + 0, + 0 + ], + [ + 48, + 0, + 0, + 0 + ], + [ + -252, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0 + ] + ], + "layout": { + "alpha": [ + 0, + 6, + 2, + 0, + 0, + 2 + ], + "beta": [ + 11, + 9, + 5, + 5, + 9, + 11 + ], + "omega": [ + 1, + 5, + 9, + 7, + 11, + 3 + ], + "pi": [ + 4, + 3, + 5, + 1, + 0, + 2 + ], + "rho": [ + 5, + 4, + 3, + 2, + 1, + 0 + ], + "sigma": [ + 4, + 3, + 5, + 1, + 0, + 2 + ] + }, + "literal_basis_pairs": 36, + "moduli": [ + 2, + 3 + ], + "phase_order": 12 + }, + { + "common_denominator": 729, + "dense_output_numerator": [ + [ + -252, + 0, + 0, + 0 + ], + [ + -45, + 0, + 0, + 0 + ], + [ + -180, + 0, + 0, + 0 + ], + [ + -108, + 0, + 0, + 0 + ], + [ + -198, + 0, + 0, + 0 + ], + [ + -135, + 0, + 0, + 0 + ], + [ + -189, + 0, + 0, + 0 + ], + [ + -180, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0 + ] + ], + "layout": { + "alpha": [ + 0, + 6, + 2, + 0, + 0, + 2, + 6, + 0, + 8 + ], + "beta": [ + 11, + 1, + 1, + 3, + 11, + 5, + 1, + 3, + 3 + ], + "omega": [ + 1, + 9, + 5, + 5, + 1, + 9, + 9, + 5, + 1 + ], + "pi": [ + 5, + 6, + 1, + 8, + 0, + 4, + 2, + 3, + 7 + ], + "rho": [ + 7, + 8, + 6, + 2, + 0, + 1, + 3, + 4, + 5 + ], + "sigma": [ + 5, + 6, + 1, + 8, + 0, + 4, + 2, + 3, + 7 + ] + }, + "literal_basis_pairs": 81, + "moduli": [ + 3, + 3 + ], + "phase_order": 12 + }, + { + "common_denominator": 4096, + "dense_output_numerator": [ + [ + -144, + 0 + ], + [ + 96, + 0 + ], + [ + -1040, + 0 + ], + [ + -80, + 0 + ], + [ + -640, + 0 + ], + [ + 464, + 0 + ], + [ + -656, + 0 + ], + [ + -704, + 0 + ], + [ + 416, + 0 + ], + [ + -400, + 0 + ], + [ + 48, + 0 + ], + [ + -1104, + 0 + ], + [ + 160, + 0 + ], + [ + 96, + 0 + ], + [ + -384, + 0 + ], + [ + -1504, + 0 + ] + ], + "layout": { + "alpha": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "beta": [ + 3, + 0, + 3, + 0, + 0, + 1, + 0, + 1, + 1, + 2, + 1, + 2, + 2, + 3, + 2, + 3 + ], + "omega": [ + 1, + 0, + 3, + 2, + 2, + 1, + 0, + 3, + 3, + 2, + 1, + 0, + 0, + 3, + 2, + 1 + ], + "pi": [ + 7, + 8, + 13, + 2, + 11, + 12, + 1, + 6, + 15, + 0, + 5, + 10, + 3, + 4, + 9, + 14 + ], + "rho": [ + 13, + 14, + 15, + 12, + 2, + 3, + 0, + 1, + 7, + 4, + 5, + 6, + 8, + 9, + 10, + 11 + ], + "sigma": [ + 7, + 8, + 13, + 2, + 11, + 12, + 1, + 6, + 15, + 0, + 5, + 10, + 3, + 4, + 9, + 14 + ] + }, + "literal_basis_pairs": 256, + "moduli": [ + 4, + 4 + ], + "phase_order": 4 + }, + { + "common_denominator": 125, + "dense_output_numerator": [ + [ + -70, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -5, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -65, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -25, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + -85, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + "layout": { + "alpha": [ + 12, + 18, + 6, + 16, + 8 + ], + "beta": [ + 19, + 13, + 5, + 15, + 3 + ], + "omega": [ + 9, + 9, + 9, + 9, + 9 + ], + "pi": [ + 0, + 2, + 4, + 1, + 3 + ], + "rho": [ + 0, + 2, + 4, + 1, + 3 + ], + "sigma": [ + 0, + 2, + 4, + 1, + 3 + ] + }, + "literal_basis_pairs": 25, + "moduli": [ + 5 + ], + "phase_order": 20 + } + ], + "assignment_seed": 71, + "census": [ + { + "accepted": 16, + "classification_sha256": "aa705d44bc3edba21eed4e23d2938e813669bca60dd4f9c6b039ffe5387f74a4", + "literal_basis_pairs": 64, + "mismatch_sha256": "984cd56bc5d3669627475b9885d90b89f1ec71f7204470bfff6a8ba5fbe55eaf", + "mismatched_forward_pairs": 2, + "moduli": [ + 2 + ], + "phase_order": 4, + "reduced_candidates": 64, + "shared_classification_sha256": "366736b02151f853c1699a4bb2b28909091018190a7ca2177f9ac04b53ad57ec", + "shared_routine_accepted": 1, + "shared_routine_candidates": 32 + }, + { + "accepted": 216, + "classification_sha256": "cd905f35f39cb5491c9c517d2e36fa5efc7f201604a560cca6ca5beb7371d68f", + "literal_basis_pairs": 1944, + "mismatch_sha256": "c820fd26fd44a49152f4dc9cd065bfcd1c7c2890a61becb8fb0f53d53fb2959a", + "mismatched_forward_pairs": 30, + "moduli": [ + 3 + ], + "phase_order": 12, + "reduced_candidates": 62208, + "shared_classification_sha256": "e03d7c0ab1e59d1fe1942334634f8a35b6ef5906f819c203f7fabf3c44fe96cc", + "shared_routine_accepted": 2, + "shared_routine_candidates": 10368 + }, + { + "accepted": 128, + "classification_sha256": "b09c7e5c2d58800c971582068e2bcfe390ef0c01083baf91c70a0acca5e51e5b", + "literal_basis_pairs": 2048, + "mismatch_sha256": "c614aeab9a472d84f7f5f942a13baeaab02a80e1145204c0f2c00f64af0318d1", + "mismatched_forward_pairs": 552, + "moduli": [ + 4 + ], + "phase_order": 4, + "reduced_candidates": 147456, + "shared_classification_sha256": "fea7d2ba03ecb58906366a43197d5135935098a582eab8fa598083fc0d028bfd", + "shared_routine_accepted": 2, + "shared_routine_candidates": 6144 + }, + { + "accepted": 384, + "classification_sha256": "515b128bb4d9d8ba46c4f769a7667fc96bb4bc378e9f55a0f2b3ed72f450c86f", + "literal_basis_pairs": 6144, + "mismatch_sha256": "146598a9f0ff1f665a7b471fe1355732c19fbc888b5a7a9d4120f36543d3b96e", + "mismatched_forward_pairs": 552, + "moduli": [ + 2, + 2 + ], + "phase_order": 4, + "reduced_candidates": 147456, + "shared_classification_sha256": "62c2800f4ecdbe8fa2b1e7473a4e698138cf29546ba5a975b1464cccb79ae586", + "shared_routine_accepted": 4, + "shared_routine_candidates": 6144 + } + ], + "schema_version": 1, + "scope": "Exact algebraic admission only; written universal proof, bounded finite replay, no new kappa.", + "semantic_controls": [ + { + "layout": { + "alpha": [ + 1, + 1, + 1, + 1 + ], + "beta": [ + 1, + 1, + 1, + 1 + ], + "omega": [ + 3, + 3, + 3, + 3 + ], + "pi": [ + 0, + 1, + 2, + 3 + ], + "rho": [ + 0, + 1, + 2, + 3 + ], + "sigma": [ + 0, + 1, + 2, + 3 + ] + }, + "moduli": [ + 4 + ], + "name": "constant_i_shared_routine", + "options": {}, + "witness": { + "actual_numerator": [ + 0, + 4 + ], + "common_denominator": 64, + "cyclotomic_order": 4, + "expected_numerator": [ + 4, + 0 + ], + "input_basis": [ + 0, + 0 + ], + "output_index": 0 + } + }, + { + "layout": { + "alpha": [ + 0, + 1, + 2, + 3 + ], + "beta": [ + 0, + 1, + 2, + 3 + ], + "omega": [ + 0, + 3, + 2, + 1 + ], + "pi": [ + 0, + 1, + 2, + 3 + ], + "rho": [ + 0, + 1, + 2, + 3 + ], + "sigma": [ + 0, + 1, + 2, + 3 + ] + }, + "moduli": [ + 4 + ], + "name": "nonconstant_character_shared_routine", + "options": {}, + "witness": { + "actual_numerator": [ + 0, + 0 + ], + "common_denominator": 64, + "cyclotomic_order": 4, + "expected_numerator": [ + 4, + 0 + ], + "input_basis": [ + 0, + 0 + ], + "output_index": 0 + } + }, + { + "layout": { + "alpha": [ + 0, + 3, + 2, + 1 + ], + "beta": [ + 0, + 3, + 2, + 1 + ], + "omega": [ + 0, + 1, + 2, + 3 + ], + "pi": [ + 1, + 2, + 3, + 0 + ], + "rho": [ + 1, + 2, + 3, + 0 + ], + "sigma": [ + 1, + 2, + 3, + 0 + ] + }, + "moduli": [ + 4 + ], + "name": "phase_compensated_translation_shared_routine", + "options": {}, + "witness": { + "actual_numerator": [ + 0, + 0 + ], + "common_denominator": 64, + "cyclotomic_order": 4, + "expected_numerator": [ + 4, + 0 + ], + "input_basis": [ + 0, + 0 + ], + "output_index": 0 + } + }, + { + "layout": { + "alpha": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "beta": [ + 3, + 2, + 3, + 2, + 1, + 0, + 1, + 0 + ], + "omega": [ + 1, + 0, + 3, + 2, + 1, + 0, + 3, + 2 + ], + "pi": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ], + "rho": [ + 7, + 4, + 5, + 6, + 1, + 2, + 3, + 0 + ], + "sigma": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ] + }, + "moduli": [ + 2, + 4 + ], + "name": "inverse_character_wrong_sign", + "options": {}, + "witness": { + "actual_numerator": [ + -8, + 0 + ], + "common_denominator": 512, + "cyclotomic_order": 4, + "expected_numerator": [ + 8, + 0 + ], + "input_basis": [ + 0, + 1 + ], + "output_index": 1 + } + }, + { + "layout": { + "alpha": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "beta": [ + 3, + 2, + 3, + 2, + 1, + 0, + 1, + 0 + ], + "omega": [ + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0 + ], + "pi": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ], + "rho": [ + 7, + 0, + 5, + 2, + 3, + 4, + 1, + 6 + ], + "sigma": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ] + }, + "moduli": [ + 2, + 4 + ], + "name": "reuse_forward_linear_map_as_adjoint", + "options": {}, + "witness": { + "actual_numerator": [ + 0, + 0 + ], + "common_denominator": 512, + "cyclotomic_order": 4, + "expected_numerator": [ + 8, + 0 + ], + "input_basis": [ + 0, + 1 + ], + "output_index": 1 + } + }, + { + "layout": { + "alpha": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "beta": [ + 3, + 3, + 3, + 2, + 1, + 0, + 1, + 0 + ], + "omega": [ + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0 + ], + "pi": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ], + "rho": [ + 7, + 4, + 5, + 6, + 1, + 2, + 3, + 0 + ], + "sigma": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ] + }, + "moduli": [ + 2, + 4 + ], + "name": "uncompensated_one_operand_phase", + "options": {}, + "witness": { + "actual_numerator": [ + 7, + 1 + ], + "common_denominator": 512, + "cyclotomic_order": 4, + "expected_numerator": [ + 8, + 0 + ], + "input_basis": [ + 0, + 0 + ], + "output_index": 0 + } + }, + { + "layout": { + "alpha": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "beta": [ + 3, + 2, + 3, + 2, + 1, + 0, + 1, + 0 + ], + "omega": [ + 1, + 2, + 3, + 0, + 1, + 2, + 3, + 0 + ], + "pi": [ + 1, + 6, + 3, + 4, + 5, + 2, + 7, + 0 + ], + "rho": [ + 7, + 4, + 5, + 6, + 1, + 2, + 3, + 0 + ], + "sigma": [ + 0, + 7, + 2, + 5, + 4, + 3, + 6, + 1 + ] + }, + "moduli": [ + 2, + 4 + ], + "name": "different_forward_addresses", + "options": {}, + "witness": { + "actual_numerator": [ + 0, + 0 + ], + "common_denominator": 512, + "cyclotomic_order": 4, + "expected_numerator": [ + 8, + 0 + ], + "input_basis": [ + 0, + 1 + ], + "output_index": 1 + } + }, + { + "layout": { + "alpha": [ + 0, + 0, + 0, + 0 + ], + "beta": [ + 0, + 0, + 0, + 0 + ], + "omega": [ + 0, + 0, + 0, + 0 + ], + "pi": [ + 0, + 1, + 2, + 3 + ], + "rho": [ + 0, + 1, + 2, + 3 + ], + "sigma": [ + 0, + 1, + 2, + 3 + ] + }, + "moduli": [ + 4 + ], + "name": "wrong_inverse_fourier_sign", + "options": { + "inverse_sign": -1 + }, + "witness": { + "actual_numerator": [ + 0, + 0 + ], + "common_denominator": 64, + "cyclotomic_order": 4, + "expected_numerator": [ + 4, + 0 + ], + "input_basis": [ + 0, + 1 + ], + "output_index": 1 + } + }, + { + "layout": { + "alpha": [ + 0, + 0, + 0, + 0 + ], + "beta": [ + 0, + 0, + 0, + 0 + ], + "omega": [ + 0, + 0, + 0, + 0 + ], + "pi": [ + 0, + 1, + 2, + 3 + ], + "rho": [ + 0, + 1, + 2, + 3 + ], + "sigma": [ + 0, + 1, + 2, + 3 + ] + }, + "moduli": [ + 4 + ], + "name": "missing_one_normalization", + "options": { + "expected_scale": 16 + }, + "witness": { + "actual_numerator": [ + 4, + 0 + ], + "common_denominator": 64, + "cyclotomic_order": 4, + "expected_numerator": [ + 16, + 0 + ], + "input_basis": [ + 0, + 0 + ], + "output_index": 0 + } + } + ], + "sources": { + "upstream/build/sections/07-resampling.tex": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c", + "upstream/manifest.json": "16ab13971694cabab09440c47ebf2fc0496a9d35fc3af33950fda3498f8e2392" + }, + "status": "PASS_WEIGHTED_FOURIER_LAYOUT", + "totals": { + "accepted": 744, + "dense_pairs": 5, + "literal_basis_pairs": 10662, + "mismatched_forward_pairs": 1136, + "reduced_candidates": 357184, + "semantic_controls": 9, + "shared_routine_accepted": 9, + "shared_routine_candidates": 22688 + } +} diff --git a/research/weighted-fourier-layout/README.md b/research/weighted-fourier-layout/README.md new file mode 100644 index 0000000000..7cd23891f1 --- /dev/null +++ b/research/weighted-fourier-layout/README.md @@ -0,0 +1,261 @@ +# Exact convolution boundary for phase-weighted Fourier layouts + +**Mathematical audit / scoped interface theorem; no new kappa.** A shared +phase-weighted Fourier routine cannot preserve the retained convolution +identity merely by conjugating that routine for the final pass, unless +**every phase is 1** and its read permutation is a self-adjoint group +automorphism. Phases cannot repair a translated or non-self-adjoint shared +layout under this contract. + +With separately chosen forward and inverse weights, affine layouts do work. +The theorem below gives all of them, including the exact character factors +and the necessary agreement of the two forward address maps. It extends +[Ross Richardson's PR #940](https://github.com/CrocSwap/integer-mult-bounds/pull/940) +from unweighted permutations to three monomial maps. The unweighted result +and Fourier duality are predecessor work, not new claims here. + +The source's stated coordinate multipliers satisfy the criterion. There is +no counterexample to its actual lemma and no change to the selected result. +This supplies an admission boundary for proposed phase/address changes; +it does not price or implement physical routing. + +## Exact statement + +Let `G = product_i Z/q_i`, `q_i >= 2`, `N = |G|`, with pairing + +\[ +\chi(x,y)=\exp\left(2\pi i\sum_i x_i y_i/q_i\right). +\] + +Both Fourier signs are normalized by `1/N`: + +\[ +(F^\pm u)(x)=\frac1N\sum_y\chi(x,y)^{\pm1}u(y). +\] + +Use **read** permutations `(P_pi f)(y)=f(pi(y))`, and diagonal maps +`(D_alpha f)(y)=alpha(y)f(y)`. The weights `alpha`, `beta`, `omega` +are arbitrary complex functions of modulus one, not necessarily roots of +unity or characters. Let `pi`, `sigma`, `rho` be permutations of `G`. +Convolution `*` is unnormalized. We ask when, for every `u,v in C^G`, + +\[ +D_\omega P_\rho F^+ + \left[(D_\alpha P_\pi F^-u)\cdot(D_\beta P_\sigma F^-v)\right] + =\frac{u*v}{N^2}. \tag{1} +\] + +**Theorem.** (1) holds if and only if there are a group automorphism `L`, +offsets `a,b in G`, and a unit complex scalar `gamma` such that + +\[ +\begin{aligned} +\sigma(y)=\pi(y)&=L(y)+b, &\rho(x)&=L^\dagger(x)+a,\\ +\alpha(y)\beta(y)&=\gamma\chi(-a,y), + &\omega(x)&=\gamma^{-1}\chi(x,b). \tag{2} +\end{aligned} +\] + +Here the adjoint uses the actual product-group pairing: +`chi(L^dagger(x),y)=chi(x,L(y))`. On unequal cyclic factors it is generally +not an ordinary matrix transpose. The forward weights can split their +specified product arbitrarily: every unit function `h` gives the same +result after `alpha -> h alpha`, `beta -> h^-1 beta`. + +### Proof + +Write `f=F^-u`, `g=F^-v`. They range independently over all complex +functions because `F^-` is invertible. The normalized convolution rule is +`F^+(f ยท g)=(u*v)/N^2`, with a pointwise product inside the transform. +The coefficient of `f(pi(y))g(sigma(y))` in output coordinate `x` on the +left of (1) is + +\[ +N^{-1}\omega(x)\alpha(y)\beta(y)\chi(\rho(x),y), \tag{3} +\] + +which is nonzero. If `pi(y) != sigma(y)`, the right side has zero coefficient +for this off-diagonal monomial. No other `y` can cancel it because `pi` +is injective. Consequently `sigma=pi` is necessary. + +Put `q(y)=alpha(y)beta(y)`. Comparing the remaining diagonal coefficients +after writing their common address as `pi(y)` gives precisely + +\[ +\omega(x)q(y)\chi(\rho(x),y)=\chi(x,\pi(y)) +\quad\hbox{for every }x,y. \tag{4} +\] + +Let `b=pi(0)`, `a=rho(0)`, `gamma=q(0)`. First set `y=0` in (4), then +`x=0`. These force + +\[ +\omega(x)=\gamma^{-1}\chi(x,b),\qquad +q(y)=\gamma\chi(-a,y). +\] + +After cancellation, (4) becomes + +\[ +\chi(\rho(x)-a,y)=\chi(x,\pi(y)-b). \tag{5} +\] + +Define `L(y)=pi(y)-b`. Multiplicativity of the left side in `y` implies +`chi(x,L(y+z)-L(y)-L(z))=1` for all `x`. Nondegeneracy forces additivity. +Since `pi` is bijective, `L` is an automorphism. Equation (5) then forces +`rho(x)-a=L^dagger(x)`. The adjoint exists uniquely because every character +of the product group is `chi(w,.)` for a unique `w`; composition with an +automorphism permutes these characters. This also makes the adjoint an +automorphism. This proves necessity. Substituting (2) into (4), then +reversing the coefficient calculation, proves sufficiency. + +### Shared routine and conjugate inverse + +Suppose both forward passes use `A=D_w P_pi F^-`, and the final routine +is obtained by conjugating input and output: `bar(A)=D_conj(w) P_pi F^+`. +In (4), set `alpha=beta=w`, `omega=conj(w)`, `rho=pi`, and then `y=x`. +Symmetry of the pairing cancels the character factors and leaves +`conj(w(x))*w(x)^2=1`. Since `|w(x)|=1`, **`w(x)=1` at every address**. +The theorem now gives `a=b=0` and `L=L^dagger`, exactly PR940's unweighted +criterion. Conversely those conditions suffice. + +A minimal failure is `G=Z/4`, `pi=id`, `w=i`, `u=v=delta_0`: the output +is `i delta_0/16`, whereas (1) requires `delta_0/16`. Even a global phase +does not cancel across these three passes. The receipt records numerators +`4i` and `4` over their common denominator `64`. + +The asymmetric contract has a simple positive contrast. On `Z/4`, set +`pi(y)=sigma(y)=y+1`, `rho(x)=x+1`, `alpha(y)=1`, `beta(y)=i^-y`, +`omega(x)=i^x`. Equation (4) holds exactly. All sixteen input basis pairs +are checked in the tests. Thus the negative corollary does not prohibit +affine layouts with the correct separate phases. + +## Source and scope + +- Base: `410026dc5513b87db92ae98571d1d5984c69a983`. +- Audited source: [07-resampling.tex](../../upstream/build/sections/07-resampling.tex), + `lem:chirp-permutation`, specifically `eq:source-permutation-cancel`; + original `openai/math@adc7f1241b42e322a6451854ab7e4b4c146bf78a`. +- Predecessor: Ross Richardson's PR940 at + `fccac36fa9bcc063c4fda733299a22349ce10e56`. Its proof was inspected; + no pending code is imported or needed for replay. +- The selected record at the base is PR1094's conditional + `836330098538459/500000000000000000`, with complex supplier binding. + The selected review, source manifest, actual T16 package and assembly + were followed. `research_baseline.py` passed source bindings only. +- [SOURCES.json](SOURCES.json) pins live source bytes and historical + selection/task provenance separately. [TASK.json](TASK.json) records + OS seed **71**, three candidates, scope, stopping rule, credit and the + [coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1463). + +The theorem is exact complex algebra. It supplies no rounded Gaussian +implementation, tape schedule, saved operation, paid recurrence, supplier +adoption, improved kappa, or full multiplication proof. Arbitrary phase +weights preserve coordinate magnitudes, but their calculation and application +are not free. Both read permutations and both required character factors +must be included in any proposed implementation's cost and error budget. +The all-size/compiler, hosting, precision/tape and analytic obligations of +the selected construction remain inherited. + +## Reproduce and inspect the evidence + +From the repository root, using Python 3.12 and only the standard library: + +```sh +python3.12 scripts/research_package.py --package research/weighted-fourier-layout +``` + +Expected: `PASS_WEIGHTED_FOURIER_LAYOUT`, eleven passing test groups, and +`PASS_REGISTERED_RESEARCH_PACKAGE research/weighted-fourier-layout outcome=completed`. +The direct checker also works in an offline source export with this package +and its two pinned upstream inputs: + +```sh +python3 -I -O -B research/weighted-fourier-layout/verify.py +python3 -I -O -B research/weighted-fourier-layout/test_verify.py +``` + +The registered metadata check additionally requires Git history to resolve +historical provenance. The direct checker compares the complete regenerated +receipt to [EXPECTED.json](EXPECTED.json). `--write /path/to/new.json` +instead creates a fresh receipt and refuses overwrite. It performs the +mathematical checks but does not compare to the committed expected receipt. + +For the finite census let `M=lcm(4,q_1,...,q_d)` and restrict weights to +`M`th roots of unity. For every pair `pi,rho` and every product phase vector +`q`, the `y=0` coefficient of (4) forces a unique `omega`. This is the +explicit reduction used for the following complete finite domain; arbitrary +complex weights are covered by the written proof, not a finite search. + +| Group | M | Reduced candidates | Accepted | Shared-routine candidates | Accepted | +|---|---:|---:|---:|---:|---:| +| Z/2 | 4 | 64 | 16 | 32 | 1 | +| Z/3 | 12 | 62,208 | 216 | 10,368 | 2 | +| Z/4 | 4 | 147,456 | 128 | 6,144 | 2 | +| (Z/2)^2 | 4 | 147,456 | 384 | 6,144 | 4 | +| Total | | **357,184** | **744** | **22,688** | **9** | + +Two classifications agree everywhere: literal scaled-integer character +coefficients, and affine reconstruction from generator images with rational +turns and a weighted adjoint. Digests bind the ordered classification streams. +An independent [oracle.py](oracle.py) evaluates both forward transforms, +the product, the final transform, and direct convolution in exact cyclotomic +rings. It does not call either admission classifier. It checks: + +- All input basis pairs for the 744 accepted reduced cases, choosing a + deterministic split of each product phase, plus five larger/unequal-factor + fixtures: **10,662 basis pairs**, and five dense integer pairs in total. +- All **1,136 unequal forward-permutation pairs** in the census domain, + using explicit character inputs with zero desired convolution and nonzero + computed output. The written nonzero-coefficient argument handles arbitrary + phases and inverse maps; these finite witnesses use fixed deterministic ones. +- **Nine semantic counterexamples**: constant/shared character phases, + phase-compensated shared translation, wrong inverse character sign, + forward linear map in place of its adjoint, an uncompensated operand phase, different forward + addresses, the wrong inverse Fourier sign, and a missing normalization. + +[test_verify.py](test_verify.py) additionally checks all **32,768 unreduced +two-point cases** (all three permutations and all three independent phase +vectors) against literal convolution; exactly **256** pass. It checks all +256 reciprocal phase vectors on Z/4, the translated positive example, +exact root fields and normalization, wrong classifiers in both directions, +nonbijective inputs, source relocation/drift/missing files and overwrite +rejection. This validates the finite reduction with an unreduced domain. +Assertions are not used for acceptance, so checks remain active under `-O`. + +The fixed domain is exhausted; this is not a heuristic search. The written +universal argument and its finite checks are separate. Neither has been +verified by a proof assistant or an independent human reviewer. No numerical +FFT, full supplier cold replay or benchmark is claimed. + +Local validation passed on macOS arm64: the registered Python 3.12.13 replay +and all eleven tests, optimized isolated Python 3.14.2 execution, and an +offline export without Git in a path containing spaces. Deliberately changed +source bytes and a false expected certificate were both rejected. The selected +record check passed. On refreshed main +`e6f9716621f4e01fc190617934cdfaf072bd976f`, both live source inputs and the +selected kappa were unchanged. The final overlap snapshot covered 829 open +PRs and all paginated discussion records, with no retrieval warnings; its +coverage limits and the credited PR940 overlap are retained in TASK.json. +Hosted CI is separate from these local results. + +## Open next questions + +Can an existing physical Fourier schedule absorb a permitted affine shift +and its two character factors without additional paid work? This could make +the algebraic admission result useful to a recursive boundary change. A +bounded next step is to choose one actual source schedule and one nonzero +offset, realize both read maps and both character factors, and price the +complete forward/product/inverse wrapper. No such candidate schedule or +interface is constructed here; that is the present blocker. The structured +question is also in [TASK.json](TASK.json). + +## Credit + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex +assistance** in mathematics, implementation, verification and prose. +Credit **Ross Richardson** for PR940's unweighted criterion and proof, +**OpenAI** for the original manuscript, and **Douglas Colkitt / CrocSwap** +for the retained construction and normalization audit. No literature-priority +claim is made for elementary character or monomial-map algebra. +New material is Apache-2.0. Original source files and licenses are unchanged. diff --git a/research/weighted-fourier-layout/SOURCES.json b/research/weighted-fourier-layout/SOURCES.json new file mode 100644 index 0000000000..dd749bf54a --- /dev/null +++ b/research/weighted-fourier-layout/SOURCES.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "upstream/build/sections/07-resampling.tex", + "usage": "input", + "git_blob": "256243bf9416baefb82bf9203f80215b9ebe28f2", + "sha256": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c" + }, + { + "path": "upstream/manifest.json", + "usage": "input", + "git_blob": "01c309e34d36cf3669c43d89c5dfb25cdc31b8af", + "sha256": "16ab13971694cabab09440c47ebf2fc0496a9d35fc3af33950fda3498f8e2392" + } + ], + "related_work": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 940, + "head": "fccac36fa9bcc063c4fda733299a22349ce10e56", + "author": "Ross Richardson (@RossRichardson)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/940", + "inspected_path": "research/source-permutation-audit/README.md", + "inspected_readme_sha256": "157a31ee176ceb86243f025cf7fd896bac438a3834a2d49d0be6fb223d78bd0e", + "usage": "Predecessor attribution and scope comparison only; no pending code imported or required for replay.", + "inspected_readme_git_blob": "33e7cbafd02bd70d3d83e489f4b67a37adcf68d5" + } + ] +} diff --git a/research/weighted-fourier-layout/TASK.json b/research/weighted-fourier-layout/TASK.json new file mode 100644 index 0000000000..aedf0b4997 --- /dev/null +++ b/research/weighted-fourier-layout/TASK.json @@ -0,0 +1,121 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 2, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact convolution admission for two phase-weighted Fourier read layouts and an independently weighted positive-sign inverse; shared conjugate routine as a restricted corollary.", + "scope_change_reason": "Refines the all-size transfer card to the source-permutation cancellation obligation, extending PR940 from permutations to monomial layouts and affine shifts.", + "bottleneck_link": "Side-result admission boundary: prevents unpriced phase/address changes from being treated as a valid retained Fourier interface. Does not change the binding complex supplier or its budget.", + "budget_minutes": 60, + "stop_rule": "Prove or falsify the stated criterion, then exhaust the declared small-group census; no optimization or enlarged search. Reserve final 15 minutes of a 60 minute session for verification and handoff.", + "outcome": "completed", + "evidence": "README.md gives the all-group monomial normal form and shared-conjugate rigidity proof. EXPECTED.json binds 357184 reduced candidates, 22688 shared-routine candidates, 10662 direct basis pairs, 1136 mismatched-address witnesses and nine semantic controls. test_verify.py adds an unreduced 32768-case two-point domain and source/failure controls.", + "author": "Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, verification and prose. No independent human review or proof-assistant check.", + "open_questions": [ + { + "question": "Can an existing physical Fourier schedule absorb the affine shifts and the two required character factors without additional paid work?", + "why_it_matters": "The algebra permits asymmetric affine layouts, but only a complete implementation cost could turn this admission criterion into a useful boundary change.", + "first_step": "Choose one source schedule and one explicit nonzero a or b, realize both read permutations and q/omega factors, and price the complete forward/product/inverse wrapper.", + "blocked_by": "No candidate tape schedule or changed supplier interface is constructed in this package." + } + ], + "assignment_seed": 71, + "assignment_source": "One secrets.randbelow(100) OS randomness draw", + "candidate_tasks": [ + "Phase-weighted extension of PR940 exact convolution cancellation (chosen)", + "Tensor resampling invalid-line masks under nonlinear approximants (existing source proof already explicit)", + "Gaussian inverse rounding contract (overlaps PR1430 and PR371/684/902)" + ], + "predecessors": [ + { + "pr": 940, + "head": "fccac36fa9bcc063c4fda733299a22349ce10e56", + "author": "Ross Richardson (@RossRichardson)", + "scope": "Unweighted read-permutation criterion; no code imported" + } + ], + "started_utc": "2026-10-14T00:57:26.033011+00:00", + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1463", + "pinned_issue": null + }, + "overlap_review": { + "searched_at": "2026-10-14T01:18:09.840052+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T01:17:54.614537+00:00", + "complete_pagination": true, + "records": 829 + }, + "discussions": { + "fetched_at": "2026-10-14T01:18:09.794978+00:00", + "complete_pagination": true, + "records": 164 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "relevant_predecessor_pr": 940, + "distinct_delta": "PR940 admits unweighted permutations. This package proves the full three-map phase-weighted criterion and shows phase rigidity for the shared conjugate routine; the finite weighted domain is new.", + "immediate_presubmit": { + "updated_open_prs_checked": 20, + "recent_discussions_checked": 10, + "newest_pr_inspected": 1475, + "no_additional_related_scope_found": true, + "predecessor_head_reconfirmed": "fccac36fa9bcc063c4fda733299a22349ce10e56" + } + }, + "verification_summary": { + "registered_python": "3.12.13", + "optimized_python": "3.14.2", + "focused_test_groups": 11, + "unreduced_two_point_cases": 32768, + "minimal_export_without_git": "passed in path containing spaces", + "source_corruption": "rejected", + "certificate_corruption": "rejected", + "selected_record_check": "passed", + "refreshed_main": "e6f9716621f4e01fc190617934cdfaf072bd976f", + "audited_source_unchanged_on_refreshed_main": true, + "full_supplier_cold_replay": "not run; no supplier changed", + "proof_assistant": "not run", + "independent_human_review": "not claimed" + } +} diff --git a/research/weighted-fourier-layout/VERIFY.json b/research/weighted-fourier-layout/VERIFY.json new file mode 100644 index 0000000000..bd5c6300d8 --- /dev/null +++ b/research/weighted-fourier-layout/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "upstream/build/sections/07-resampling.tex", + "upstream/manifest.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact monomial-layout census, separate literal cyclotomic convolution, source bindings and nine mathematical failure witnesses." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Unreduced two-point exhaustive domain, exact root fields, reciprocal phases, affine controls, classifier mutations, source drift and overwrite rejection." + } + ] +} diff --git a/research/weighted-fourier-layout/oracle.py b/research/weighted-fourier-layout/oracle.py new file mode 100644 index 0000000000..dd7b4445ef --- /dev/null +++ b/research/weighted-fourier-layout/oracle.py @@ -0,0 +1,168 @@ +"""Literal exact Fourier/convolution oracle, independent of admission formulas. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor code is imported. Values lie in Z[z]/Phi_m; denominator N**3. +""" + +from fractions import Fraction +from itertools import product +from math import lcm, prod + + +def exact_quotient(a, b): + a = list(a) + out = [0] * (len(a) - len(b) + 1) + for k in range(len(out) - 1, -1, -1): + out[k] = a[k + len(b) - 1] + for j, coefficient in enumerate(b): + a[k + j] -= out[k] * coefficient + if any(a): + raise ValueError("nonexact polynomial quotient") + return tuple(out) + + +def cyclotomic(m): + polynomials = {} + for n in range(1, m + 1): + if m % n: + continue + p = (-1,) + (0,) * (n - 1) + (1,) + for d in range(1, n): + if n % d == 0: + p = exact_quotient(p, polynomials[d]) + polynomials[n] = p + return polynomials[m] + + +class Ring: + def __init__(self, m): + self.m = m + self.polynomial = cyclotomic(m) + self.degree = len(self.polynomial) - 1 + self.zero = (0,) * self.degree + self.one = (1,) + (0,) * (self.degree - 1) + powers = [] + value = self.one + for _ in range(m): + powers.append(value) + a = [0] + list(value) + leading = a.pop() + value = tuple(a[i] - leading * self.polynomial[i] + for i in range(self.degree)) + if value != self.one or len(set(powers)) != m: + raise ValueError("root of unity is not primitive") + self.powers = tuple(powers) + + def integer(self, n): + return (n,) + (0,) * (self.degree - 1) + + def add(self, a, b): + return tuple(x + y for x, y in zip(a, b)) + + def scale(self, a, n): + return tuple(n * x for x in a) + + def root_mul(self, a, e): + out = [0] * self.degree + for j, coefficient in enumerate(a): + if coefficient: + for i, entry in enumerate(self.powers[(e + j) % self.m]): + out[i] += coefficient * entry + return tuple(out) + + def mul(self, a, b): + out = [0] * self.degree + for j, aj in enumerate(a): + if not aj: + continue + for k, bk in enumerate(b): + if bk: + for i, entry in enumerate(self.powers[(j + k) % self.m]): + out[i] += aj * bk * entry + return tuple(out) + + +class FourierOracle: + def __init__(self, moduli): + self.moduli = tuple(moduli) + self.points = tuple(product(*(range(q) for q in moduli))) + self.n = prod(moduli) + self.m = lcm(4, *moduli) + self.ring = Ring(self.m) + self.indices = {x: i for i, x in enumerate(self.points)} + self.kernel = [] + for x in self.points: + row = [] + for y in self.points: + turn = sum((Fraction(a * b, q) + for a, b, q in zip(x, y, moduli)), Fraction()) + exponent = self.m * turn + if exponent.denominator != 1: + raise ValueError("character is outside phase field") + row.append(int(exponent) % self.m) + self.kernel.append(tuple(row)) + self.sums = tuple(tuple(self.indices[tuple((a + b) % q + for a, b, q in zip(x, y, moduli))] + for y in self.points) for x in self.points) + + def basis(self, i): + return tuple(self.ring.one if j == i else self.ring.zero + for j in range(self.n)) + + def character(self, i): + return tuple(self.ring.powers[self.kernel[j][i]] + for j in range(self.n)) + + def dense(self, seed, salt): + return tuple(self.ring.integer(((seed + salt) * (j + 1) ** 2 + + 3 * j + salt) % 11 - 5) + for j in range(self.n)) + + def transform(self, values, sign): + if sign not in (-1, 1): + raise ValueError("Fourier sign must be -1 or 1") + result = [] + for row in self.kernel: + total = self.ring.zero + for value, exponent in zip(values, row): + total = self.ring.add(total, self.ring.root_mul(value, sign * exponent)) + result.append(total) + return tuple(result) + + def layout(self, values, permutation, phases): + return tuple(self.ring.root_mul(values[j], phase) + for j, phase in zip(permutation, phases)) + + def convolution(self, u, v): + result = [self.ring.zero] * self.n + for i, a in enumerate(u): + if not any(a): + continue + for j, b in enumerate(v): + if any(b): + k = self.sums[i][j] + result[k] = self.ring.add(result[k], self.ring.mul(a, b)) + return tuple(result) + + def evaluate(self, u, v, pi, sigma, rho, alpha, beta, omega, + inverse_sign=1, expected_scale=None): + """Compare literal unnormalized numerator to N times direct convolution.""" + left = self.layout(self.transform(u, -1), pi, alpha) + right = self.layout(self.transform(v, -1), sigma, beta) + pointwise = tuple(self.ring.mul(a, b) for a, b in zip(left, right)) + actual = self.layout(self.transform(pointwise, inverse_sign), rho, omega) + factor = self.n if expected_scale is None else expected_scale + expected = tuple(self.ring.scale(x, factor) for x in self.convolution(u, v)) + return actual, expected + + def first_basis_failure(self, **layout): + for i in range(self.n): + for j in range(self.n): + actual, expected = self.evaluate(self.basis(i), self.basis(j), **layout) + for k, (a, b) in enumerate(zip(actual, expected)): + if a != b: + return {"input_basis": [i, j], "output_index": k, + "actual_numerator": list(a), "expected_numerator": list(b), + "common_denominator": self.n ** 3, + "cyclotomic_order": self.m} + return None diff --git a/research/weighted-fourier-layout/test_verify.py b/research/weighted-fourier-layout/test_verify.py new file mode 100644 index 0000000000..fde8424e56 --- /dev/null +++ b/research/weighted-fourier-layout/test_verify.py @@ -0,0 +1,158 @@ +"""Scoped mathematical and failure-detection tests. Apache-2.0. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. +""" +import importlib.util +from itertools import permutations, product +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("weighted_fourier_verify", HERE / "verify.py") +V = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(V) + + +class Tests(unittest.TestCase): + def test_exact_root_fields_and_fourier_normalization(self): + for m, expected in [(4, (1, 0, 1)), (12, (1, 0, -1, 0, 1)), + (20, (1, 0, -1, 0, 1, 0, -1, 0, 1))]: + self.assertEqual(V.ORACLE.cyclotomic(m), expected) + ring = V.ORACLE.Ring(m) + for i in range(m): + for j in range(m): + self.assertEqual(ring.mul(ring.powers[i], ring.powers[j]), + ring.powers[(i + j) % m]) + for moduli in V.DOMAIN + ((2, 3), (2, 4), (3, 3), (5,)): + oracle = V.ORACLE.FourierOracle(moduli) + for i in range(oracle.n): + reconstructed = oracle.transform(oracle.transform(oracle.basis(i), -1), 1) + self.assertEqual(reconstructed, tuple(oracle.ring.scale(x, oracle.n) + for x in oracle.basis(i))) + + def test_unreduced_two_point_domain(self): + # No forced-weight or matched-address reduction: all 8 * 4**6 tuples. + g = V.Group((2,)) + oracle = V.ORACLE.FourierOracle((2,)) + ps = tuple(permutations(range(2))) + ws = tuple(product(range(4), repeat=2)) + total = accepted = 0 + for pi, sigma, rho in product(ps, repeat=3): + for alpha, beta, omega in product(ws, repeat=3): + layout = dict(pi=pi, sigma=sigma, rho=rho, alpha=alpha, beta=beta, omega=omega) + literal = oracle.first_basis_failure(**layout) is None + self.assertEqual(V.admit(g, **layout), literal) + self.assertEqual(V.normal_form_condition(g, **layout), literal) + total += 1 + accepted += int(literal) + self.assertEqual((total, accepted), (32768, 256)) + + def test_arbitrary_reciprocal_forward_gauges(self): + g = V.Group((4,)) + oracle = V.ORACLE.FourierOracle((4,)) + identity = tuple(range(4)) + u, v = oracle.dense(71, 2), oracle.dense(71, 7) + for alpha in product(range(4), repeat=4): + layout = dict(pi=identity, sigma=identity, rho=identity, alpha=alpha, + beta=tuple(-a % 4 for a in alpha), omega=(0,) * 4) + self.assertTrue(V.admit(g, **layout)) + actual, expected = oracle.evaluate(u, v, **layout) + self.assertEqual(actual, expected) + + def test_unequal_factor_adjoint_and_affine_phases(self): + g, layout = V.make_affine_layout((2, 4), lambda x: ((x[0] + x[1]) % 2, x[1]), + (1, 3), (0, 1)) + self.assertTrue(V.admit(g, **layout)) + self.assertTrue(V.normal_form_condition(g, **layout)) + expected = tuple(g.index[((x + 1) % 2, (2 * x + y + 3) % 4)] + for x, y in g.points) + self.assertEqual(layout["rho"], expected) + self.assertNotEqual(layout["pi"], expected) + inverse_pi = tuple(layout["pi"].index(i) for i in range(g.n)) + self.assertFalse(V.admit(g, **dict(layout, rho=inverse_pi))) + + def test_constant_phase_counterexample_is_literal(self): + oracle = V.ORACLE.FourierOracle((4,)) + identity = tuple(range(4)) + actual, expected = oracle.evaluate(oracle.basis(0), oracle.basis(0), + pi=identity, sigma=identity, rho=identity, + alpha=(1,) * 4, beta=(1,) * 4, omega=(3,) * 4) + self.assertEqual(actual, ((0, 4), (0, 0), (0, 0), (0, 0))) + self.assertEqual(expected, ((4, 0), (0, 0), (0, 0), (0, 0))) + + def test_translated_layout_with_asymmetric_forward_phases(self): + g = V.Group((4,)) + layout = dict(pi=(1, 2, 3, 0), sigma=(1, 2, 3, 0), rho=(1, 2, 3, 0), + alpha=(0, 0, 0, 0), beta=(0, 3, 2, 1), omega=(0, 1, 2, 3)) + self.assertTrue(V.admit(g, **layout)) + self.assertTrue(V.normal_form_condition(g, **layout)) + self.assertEqual(V.checked_basis_pairs(V.ORACLE.FourierOracle((4,)), layout), 16) + + def test_source_multiplier_need_not_be_involutive(self): + g = V.Group((5,)) + pi = (0, 2, 4, 1, 3) + zeros = (0,) * 5 + layout = dict(pi=pi, sigma=pi, rho=pi, alpha=zeros, beta=zeros, omega=zeros) + self.assertTrue(V.admit(g, **layout)) + self.assertTrue(V.normal_form_condition(g, **layout)) + self.assertNotEqual(tuple(pi[pi[j]] for j in range(5)), tuple(range(5))) + self.assertEqual(V.checked_basis_pairs(V.ORACLE.FourierOracle((5,)), layout), 25) + + def test_classification_false_positive_and_false_negative_controls(self): + with patch.object(V, "coefficient_condition", return_value=True): + with self.assertRaisesRegex(ValueError, "classification discrepancy"): + V.census_group((2,)) + with patch.object(V, "coefficient_condition", return_value=False): + with self.assertRaisesRegex(ValueError, "classification discrepancy"): + V.census_group((2,)) + + def test_nonbijective_and_malformed_admission(self): + g = V.Group((2,)) + valid = dict(pi=(0, 1), sigma=(0, 1), rho=(0, 1), + alpha=(0, 0), beta=(0, 0), omega=(0, 0)) + for field, bad in [("pi", (0, 0)), ("sigma", (True, 0)), + ("rho", (1,)), ("alpha", (0, 4)), ("beta", (0, -1))]: + with self.assertRaises(ValueError): + V.admit(g, **dict(valid, **{field: bad})) + + def test_source_relocation_and_corruption(self): + root = HERE.parents[1] + with tempfile.TemporaryDirectory(prefix="weighted Fourier source ") as tmp: + target = Path(tmp) + pins = json.loads((HERE / "SOURCES.json").read_text()) + paths = [] + for row in pins["files"]: + if row["usage"] == "input": + path = target / row["path"] + path.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(root / row["path"], path) + paths.append(path) + self.assertEqual(V.check_sources(target), V.check_sources()) + source = paths[0] + original = source.read_bytes() + source.write_bytes(original + b"\ncorruption\n") + with self.assertRaisesRegex(ValueError, "source drift"): + V.check_sources(target) + source.unlink() + with self.assertRaises(FileNotFoundError): + V.check_sources(target) + + def test_write_preserves_existing_file(self): + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / "existing.json" + path.write_text("do not overwrite\n") + run = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py"), + "--write", str(path)], capture_output=True, text=True) + self.assertNotEqual(run.returncode, 0) + self.assertIn("refusing to overwrite", run.stderr) + self.assertEqual(path.read_text(), "do not overwrite\n") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/weighted-fourier-layout/verify.py b/research/weighted-fourier-layout/verify.py new file mode 100644 index 0000000000..ea7c77a905 --- /dev/null +++ b/research/weighted-fourier-layout/verify.py @@ -0,0 +1,353 @@ +#!/usr/bin/env python3 +"""Exact bounded audit of phase-weighted retained Fourier layouts. + +Hanson Sun (@bbMisk), substantial OpenAI Codex assistance. Apache-2.0. +Explicit exceptions preserve all checks under Python -O. +""" + +import argparse +from fractions import Fraction +import hashlib +import importlib.util +from itertools import permutations, product +import json +from math import lcm, prod +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("weighted_fourier_oracle", HERE / "oracle.py") +ORACLE = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(ORACLE) +SEED = 71 +DOMAIN = ((2,), (3,), (4,), (2, 2)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Group: + def __init__(self, moduli): + require(bool(moduli) and all(type(q) is int and q >= 2 for q in moduli), + "cyclic moduli must be integers at least two") + self.moduli = tuple(moduli) + self.points = tuple(product(*(range(q) for q in moduli))) + self.index = {x: i for i, x in enumerate(self.points)} + self.n = prod(moduli) + self.m = lcm(4, *moduli) + self.pair = tuple(tuple(sum(a * b * (self.m // q) + for a, b, q in zip(x, y, moduli)) % self.m + for y in self.points) for x in self.points) + self.generators = tuple(self.index[tuple(int(i == j) for i in range(len(moduli)))] + for j in range(len(moduli))) + + def subtract(self, x, y): + return self.index[tuple((a - b) % q + for a, b, q in zip(self.points[x], self.points[y], self.moduli))] + + def fractional_character(self, x, y): + # Rational turns, independent of the scaled character table. + turn = sum((Fraction(a * b, q) + for a, b, q in zip(self.points[x], self.points[y], self.moduli)), Fraction()) + scaled = self.m * turn + require(scaled.denominator == 1, "character denominator mismatch") + return int(scaled) % self.m + + +def validate_layout(g, pi, sigma, rho, alpha, beta, omega): + for p in (pi, sigma, rho): + require(len(p) == g.n and all(type(x) is int for x in p) + and sorted(p) == list(range(g.n)), "layout must be a permutation") + for phases in (alpha, beta, omega): + require(len(phases) == g.n and all(type(x) is int and 0 <= x < g.m for x in phases), + "phase exponents must be canonical integers") + + +def coefficient_condition(g, pi, rho, q, omega): + """Literal all-entry condition after the forward permutations agree.""" + for x in range(g.n): + for y in range(g.n): + if (omega[x] + q[y] + g.pair[rho[x]][y] - g.pair[x][pi[y]]) % g.m: + return False + return True + + +def admit(g, pi, sigma, rho, alpha, beta, omega): + validate_layout(g, pi, sigma, rho, alpha, beta, omega) + if tuple(pi) != tuple(sigma): + return False + return coefficient_condition(g, pi, rho, + tuple((a + b) % g.m for a, b in zip(alpha, beta)), omega) + + +def affine_dual(g, pi, rho): + """Generator reconstruction; return inverse/forward offsets or None.""" + b, a = pi[0], rho[0] + columns = tuple(g.points[g.subtract(pi[e], b)] for e in g.generators) + if any((g.moduli[j] * columns[j][i]) % g.moduli[i] + for j in range(len(columns)) for i in range(len(columns))): + return None + for y, point in enumerate(g.points): + image = tuple((g.points[b][i] + sum(point[j] * columns[j][i] + for j in range(len(columns)))) % g.moduli[i] + for i in range(len(columns))) + if image != g.points[pi[y]]: + return None + for x, point in enumerate(g.points): + adjoint = [] + for j, order in enumerate(g.moduli): + coordinate = order * sum((Fraction(point[i] * columns[j][i], g.moduli[i]) + for i in range(len(columns))), Fraction()) + if coordinate.denominator != 1: + return None + adjoint.append((int(coordinate) + g.points[a][j]) % order) + if tuple(adjoint) != g.points[rho[x]]: + return None + return a, b + + +def normal_form_condition(g, pi, sigma, rho, alpha, beta, omega): + validate_layout(g, pi, sigma, rho, alpha, beta, omega) + if tuple(pi) != tuple(sigma): + return False + offsets = affine_dual(g, pi, rho) + if offsets is None: + return False + a, b = offsets + q = tuple((x + y) % g.m for x, y in zip(alpha, beta)) + gamma = q[0] + return (q == tuple((gamma - g.fractional_character(a, y)) % g.m for y in range(g.n)) + and omega == tuple((-gamma + g.fractional_character(x, b)) % g.m + for x in range(g.n))) + + +def split_product(g, q, salt=0): + # Only the product of the two forward phases is constrained. + alpha = tuple((SEED + salt + (j + 1) ** 2 + 3 * j) % g.m for j in range(g.n)) + beta = tuple((q[j] - alpha[j]) % g.m for j in range(g.n)) + return alpha, beta + + +def checked_basis_pairs(oracle, layout): + for i in range(oracle.n): + for j in range(oracle.n): + actual, expected = oracle.evaluate(oracle.basis(i), oracle.basis(j), **layout) + require(actual == expected, f"literal convolution failed on bases {i},{j}") + return oracle.n ** 2 + + +def census_group(moduli): + g = Group(moduli) + oracle = ORACLE.FourierOracle(moduli) + ps = tuple(permutations(range(g.n))) + weights = tuple(product(range(g.m), repeat=g.n)) + digest = hashlib.sha256() + reduced = accepted = basis_pairs = 0 + for pi in ps: + for rho in ps: + offsets = affine_dual(g, pi, rho) + structural_q = None + if offsets is not None: + a, b = offsets + structural_q = tuple(-g.fractional_character(a, y) % g.m for y in range(g.n)) + structural_c = tuple(g.fractional_character(x, b) for x in range(g.n)) + for q in weights: + # y=0 forces the inverse weight, without any affine assumption. + omega = tuple((g.pair[x][pi[0]] - q[0]) % g.m for x in range(g.n)) + literal = coefficient_condition(g, pi, rho, q, omega) + normal = (structural_q is not None + and q == tuple((q[0] + z) % g.m for z in structural_q) + and omega == tuple((z - q[0]) % g.m for z in structural_c)) + require(literal == normal, "matrix / generator classification discrepancy") + reduced += 1 + digest.update(bytes(pi + rho + q + omega + (int(literal),))) + if literal: + accepted += 1 + alpha, beta = split_product(g, q, accepted) + layout = dict(pi=pi, sigma=pi, rho=rho, alpha=alpha, beta=beta, omega=omega) + require(normal_form_condition(g, **layout), "split-product classification failed") + basis_pairs += checked_basis_pairs(oracle, layout) + shared = shared_accepted = 0 + shared_digest = hashlib.sha256() + for pi in ps: + structural = affine_dual(g, pi, pi) + for w in weights: + q = tuple(2 * t % g.m for t in w) + omega = tuple(-t % g.m for t in w) + literal = coefficient_condition(g, pi, pi, q, omega) + predicted = (all(t == 0 for t in w) and structural == (0, 0)) + require(literal == predicted, "shared-routine rigidity discrepancy") + shared += 1 + shared_accepted += int(literal) + shared_digest.update(bytes(pi + w + (int(literal),))) + mismatched = 0 + mismatch_digest = hashlib.sha256() + for pi in ps: + for sigma in ps: + if pi == sigma: + continue + y = next(i for i in range(g.n) if pi[i] != sigma[i]) + q = tuple((SEED + i) % g.m for i in range(g.n)) + alpha, beta = split_product(g, q) + layout = dict(pi=pi, sigma=sigma, rho=tuple(range(g.n)), + alpha=alpha, beta=beta, omega=q) + require(not admit(g, **layout), "mismatched forward layouts admitted") + actual, expected = oracle.evaluate(oracle.character(pi[y]), oracle.character(sigma[y]), **layout) + require(all(not any(z) for z in expected), "off-diagonal convolution should vanish") + require(all(any(z) for z in actual), "mismatched spectral witness should be nonzero") + mismatched += 1 + mismatch_digest.update(json.dumps([pi, sigma, actual], separators=(",", ":")).encode()) + return {"moduli": list(moduli), "phase_order": g.m, + "reduced_candidates": reduced, "accepted": accepted, + "classification_sha256": digest.hexdigest(), "literal_basis_pairs": basis_pairs, + "shared_routine_candidates": shared, "shared_routine_accepted": shared_accepted, + "shared_classification_sha256": shared_digest.hexdigest(), + "mismatched_forward_pairs": mismatched, "mismatch_sha256": mismatch_digest.hexdigest()} + + +def make_affine_layout(moduli, linear, a, b, gamma=SEED): + g = Group(moduli) + pi = tuple(g.index[tuple((u + v) % q for u, v, q in zip(linear(x), b, moduli))] + for x in g.points) + columns = [linear(g.points[e]) for e in g.generators] + rho = [] + for x in g.points: + point = [] + for j, order in enumerate(moduli): + entry = order * sum((Fraction(x[i] * columns[j][i], moduli[i]) + for i in range(len(moduli))), Fraction()) + require(entry.denominator == 1, "invalid dual map") + point.append((int(entry) + a[j]) % order) + rho.append(g.index[tuple(point)]) + ai, bi = g.index[tuple(a)], g.index[tuple(b)] + q = tuple((gamma - g.pair[ai][y]) % g.m for y in range(g.n)) + omega = tuple((-gamma + g.pair[x][bi]) % g.m for x in range(g.n)) + alpha, beta = split_product(g, q) + return g, dict(pi=pi, sigma=pi, rho=tuple(rho), alpha=alpha, beta=beta, omega=omega) + + +def additional_fixtures(): + specs = [ + ((2, 4), lambda x: ((x[0] + x[1]) % 2, x[1]), (1, 3), (0, 1)), + ((2, 3), lambda x: (x[0], 2 * x[1] % 3), (1, 2), (1, 1)), + ((3, 3), lambda x: ((x[0] + x[1]) % 3, x[1]), (2, 1), (1, 2)), + ((4, 4), lambda x: ((x[0] + x[1]) % 4, x[1]), (3, 1), (1, 3)), + ((5,), lambda x: (2 * x[0] % 5,), (0,), (0,)), + ] + receipts = [] + fixtures = [] + for moduli, linear, a, b in specs: + g, layout = make_affine_layout(moduli, linear, a, b) + require(admit(g, **layout) and normal_form_condition(g, **layout), "affine fixture rejected") + oracle = ORACLE.FourierOracle(moduli) + count = checked_basis_pairs(oracle, layout) + actual, expected = oracle.evaluate(oracle.dense(SEED, 1), oracle.dense(SEED, 9), **layout) + require(actual == expected, "dense affine fixture failed") + receipts.append({"moduli": list(moduli), "phase_order": g.m, + "layout": layout, "literal_basis_pairs": count, + "dense_output_numerator": actual, "common_denominator": g.n ** 3}) + fixtures.append((g, layout)) + return receipts, fixtures + + +def semantic_controls(fixtures): + g = Group((4,)) + identity = tuple(range(4)) + zeros = (0,) * 4 + controls = [] + + def reject(name, group, layout, **options): + if not options: + require(not admit(group, **layout), f"admission accepted {name}") + witness = ORACLE.FourierOracle(group.moduli).first_basis_failure(**layout, **options) + require(witness is not None, f"no exact convolution witness for {name}") + controls.append({"name": name, "moduli": list(group.moduli), + "layout": layout, "options": options, "witness": witness}) + + for name, pi, w in [ + ("constant_i_shared_routine", identity, (1,) * 4), + ("nonconstant_character_shared_routine", identity, (0, 1, 2, 3)), + ("phase_compensated_translation_shared_routine", (1, 2, 3, 0), (0, 3, 2, 1))]: + reject(name, g, dict(pi=pi, sigma=pi, rho=pi, alpha=w, beta=w, + omega=tuple(-x % 4 for x in w))) + ag, valid = fixtures[0] + # Reverse the character, keeping gamma^-1 fixed at the zero coordinate. + wrong = dict(valid, omega=tuple((-2 * SEED - x) % ag.m for x in valid["omega"])) + reject("inverse_character_wrong_sign", ag, wrong) + # Keep the correct inverse offset (1,3); change only L^dagger to L. + wrong_rho = tuple(ag.index[((x + y + 1) % 2, (y + 3) % 4)] for x, y in ag.points) + wrong = dict(valid, rho=wrong_rho) + reject("reuse_forward_linear_map_as_adjoint", ag, wrong) + wrong = dict(valid, beta=tuple((x + (i == 1)) % ag.m for i, x in enumerate(valid["beta"]))) + reject("uncompensated_one_operand_phase", ag, wrong) + wrong = dict(valid, sigma=tuple(reversed(valid["sigma"]))) + reject("different_forward_addresses", ag, wrong) + plain = dict(pi=identity, sigma=identity, rho=identity, alpha=zeros, beta=zeros, omega=zeros) + reject("wrong_inverse_fourier_sign", g, plain, inverse_sign=-1) + reject("missing_one_normalization", g, plain, expected_scale=g.n ** 2) + return controls + + +def check_sources(root=None): + root = HERE.parents[1] if root is None else Path(root) + pins = json.loads((HERE / "SOURCES.json").read_text()) + checked = {} + for item in pins["files"]: + if item["usage"] != "input": + continue + digest = hashlib.sha256((root / item["path"]).read_bytes()).hexdigest() + require(digest == item["sha256"], f"source drift: {item['path']}") + checked[item["path"]] = digest + manifest = json.loads((root / "upstream/manifest.json").read_text()) + require(manifest["commit"] == "adc7f1241b42e322a6451854ab7e4b4c146bf78a", "upstream commit changed") + require(manifest["files"]["build/sections/07-resampling.tex"]["sha256"] + == checked["upstream/build/sections/07-resampling.tex"], "manifest/source mismatch") + return checked + + +def build_receipt(): + sources = check_sources() + groups = [census_group(moduli) for moduli in DOMAIN] + extras, fixtures = additional_fixtures() + controls = semantic_controls(fixtures) + return {"schema_version": 1, "status": "PASS_WEIGHTED_FOURIER_LAYOUT", + "assignment_seed": SEED, "sources": sources, + "scope": "Exact algebraic admission only; written universal proof, bounded finite replay, no new kappa.", + "census": groups, "additional_fixtures": extras, "semantic_controls": controls, + "totals": {"reduced_candidates": sum(x["reduced_candidates"] for x in groups), + "accepted": sum(x["accepted"] for x in groups), + "shared_routine_candidates": sum(x["shared_routine_candidates"] for x in groups), + "shared_routine_accepted": sum(x["shared_routine_accepted"] for x in groups), + "mismatched_forward_pairs": sum(x["mismatched_forward_pairs"] for x in groups), + "literal_basis_pairs": sum(x["literal_basis_pairs"] for x in groups + extras), + "dense_pairs": len(extras), "semantic_controls": len(controls)}} + + +def canonical(receipt): + return json.dumps(receipt, indent=2, sort_keys=True) + "\n" + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a new receipt; refuses overwrite") + args = parser.parse_args() + if args.write: + require(not args.write.exists(), "refusing to overwrite receipt") + receipt = build_receipt() + text = canonical(receipt) + if args.write: + with args.write.open("x") as handle: + handle.write(text) + else: + require((HERE / "EXPECTED.json").read_text() == text, "expected receipt differs") + print(receipt["status"] + " " + json.dumps(receipt["totals"], sort_keys=True)) + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError) as exc: + print(f"FAIL_WEIGHTED_FOURIER_LAYOUT: {exc}", file=sys.stderr) + sys.exit(1)