diff --git a/research/multiinput-shared-fourier/ORACLE.json b/research/multiinput-shared-fourier/ORACLE.json new file mode 100644 index 0000000000..bf9b61fbf9 --- /dev/null +++ b/research/multiinput-shared-fourier/ORACLE.json @@ -0,0 +1,135 @@ +{ + "controls": [ + { + "arity": 2, + "failures": 4, + "group": [ + 2 + ], + "permutation": [ + 1, + 0 + ], + "phases": [ + 0, + 2 + ] + }, + { + "arity": 3, + "failures": 0, + "group": [ + 2 + ], + "permutation": [ + 1, + 0 + ], + "phases": [ + 0, + 2 + ] + }, + { + "arity": 3, + "failures": 8, + "group": [ + 2 + ], + "permutation": [ + 0, + 1 + ], + "phases": [ + 1, + 1 + ] + }, + { + "arity": 5, + "failures": 0, + "group": [ + 2 + ], + "permutation": [ + 0, + 1 + ], + "phases": [ + 1, + 1 + ] + }, + { + "arity": 3, + "failures": 27, + "group": [ + 3 + ], + "permutation": [ + 1, + 2, + 0 + ], + "phases": [ + 0, + 8, + 4 + ] + }, + { + "arity": 5, + "failures": 1024, + "group": [ + 4 + ], + "permutation": [ + 1, + 2, + 3, + 0 + ], + "phases": [ + 0, + 1, + 2, + 3 + ] + }, + { + "arity": 3, + "failures": 48, + "group": [ + 2, + 2 + ], + "permutation": [ + 0, + 1, + 3, + 2 + ], + "phases": [ + 0, + 0, + 0, + 0 + ] + } + ], + "replay": { + "basis_tuples": 106332, + "dense_tuples": 194, + "maps": 194, + "output_sha256": "914ac3bcc69b65d40bcea58e0ae74b6e784d38f198be243ea4856c930f9c5606" + }, + "schema": "multiinput-shared-fourier-oracle/v1", + "source_sha256": { + "README.md": "e77ac3e9f42f3de483a05bec4236cdfc2fff8e97e597eeba0028a4048068b22a", + "SOURCES.json": "1bada3ff94050e6906053be2bfbe6c4401709bea14d06fa3f8d0004a7cfac9f0", + "TASK.json": "cf03c98c0763c8e55f077d53f45e4b6c421a7151ca8d786cf01a8036cb3002cc", + "VERIFY.json": "ffdea9aa7a7030112933a0aaf3b48485950c4d611d1b2abfcc8d7fd2e6ffddb9", + "oracle.py": "bf70937e13f94d546f3b6bce4ed070734f9489e2f510160ea937fec33966fba3", + "verify.py": "02c3bf3d05c134a34bd4a376a525f71581322430b2df9a7de169733e8c362d8f" + } +} diff --git a/research/multiinput-shared-fourier/PRIMARY.json b/research/multiinput-shared-fourier/PRIMARY.json new file mode 100644 index 0000000000..6e5dbcbd6d --- /dev/null +++ b/research/multiinput-shared-fourier/PRIMARY.json @@ -0,0 +1,202 @@ +{ + "census": { + "accepted": 194, + "candidates": 90752, + "classification_sha256": "da20e80881d08fee6ea037e87e3a8b1e425f129e344ad46784dec9b0314c9e82", + "rows": [ + { + "accepted": 1, + "arity": 2, + "candidates": 32, + "group": [ + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 1, + "torsion": 1 + }, + { + "accepted": 4, + "arity": 3, + "candidates": 32, + "group": [ + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 1, + "torsion": 2 + }, + { + "accepted": 1, + "arity": 4, + "candidates": 32, + "group": [ + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 1, + "torsion": 1 + }, + { + "accepted": 8, + "arity": 5, + "candidates": 32, + "group": [ + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 1, + "torsion": 2 + }, + { + "accepted": 2, + "arity": 2, + "candidates": 10368, + "group": [ + 3 + ], + "period": 12, + "self_adjoint_automorphisms": 2, + "torsion": 1 + }, + { + "accepted": 4, + "arity": 3, + "candidates": 10368, + "group": [ + 3 + ], + "period": 12, + "self_adjoint_automorphisms": 2, + "torsion": 1 + }, + { + "accepted": 18, + "arity": 4, + "candidates": 10368, + "group": [ + 3 + ], + "period": 12, + "self_adjoint_automorphisms": 2, + "torsion": 3 + }, + { + "accepted": 8, + "arity": 5, + "candidates": 10368, + "group": [ + 3 + ], + "period": 12, + "self_adjoint_automorphisms": 2, + "torsion": 1 + }, + { + "accepted": 2, + "arity": 2, + "candidates": 6144, + "group": [ + 4 + ], + "period": 4, + "self_adjoint_automorphisms": 2, + "torsion": 1 + }, + { + "accepted": 8, + "arity": 3, + "candidates": 6144, + "group": [ + 4 + ], + "period": 4, + "self_adjoint_automorphisms": 2, + "torsion": 2 + }, + { + "accepted": 2, + "arity": 4, + "candidates": 6144, + "group": [ + 4 + ], + "period": 4, + "self_adjoint_automorphisms": 2, + "torsion": 1 + }, + { + "accepted": 32, + "arity": 5, + "candidates": 6144, + "group": [ + 4 + ], + "period": 4, + "self_adjoint_automorphisms": 2, + "torsion": 4 + }, + { + "accepted": 4, + "arity": 2, + "candidates": 6144, + "group": [ + 2, + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 4, + "torsion": 1 + }, + { + "accepted": 32, + "arity": 3, + "candidates": 6144, + "group": [ + 2, + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 4, + "torsion": 4 + }, + { + "accepted": 4, + "arity": 4, + "candidates": 6144, + "group": [ + 2, + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 4, + "torsion": 1 + }, + { + "accepted": 64, + "arity": 5, + "candidates": 6144, + "group": [ + 2, + 2 + ], + "period": 4, + "self_adjoint_automorphisms": 4, + "torsion": 4 + } + ] + }, + "controls": { + "invalid_inputs": 12, + "semantic": 4 + }, + "schema": "multiinput-shared-fourier-primary/v1", + "source_sha256": { + "README.md": "e77ac3e9f42f3de483a05bec4236cdfc2fff8e97e597eeba0028a4048068b22a", + "SOURCES.json": "1bada3ff94050e6906053be2bfbe6c4401709bea14d06fa3f8d0004a7cfac9f0", + "TASK.json": "cf03c98c0763c8e55f077d53f45e4b6c421a7151ca8d786cf01a8036cb3002cc", + "VERIFY.json": "ffdea9aa7a7030112933a0aaf3b48485950c4d611d1b2abfcc8d7fd2e6ffddb9", + "oracle.py": "bf70937e13f94d546f3b6bce4ed070734f9489e2f510160ea937fec33966fba3", + "verify.py": "02c3bf3d05c134a34bd4a376a525f71581322430b2df9a7de169733e8c362d8f" + } +} diff --git a/research/multiinput-shared-fourier/README.md b/research/multiinput-shared-fourier/README.md new file mode 100644 index 0000000000..2395092d71 --- /dev/null +++ b/research/multiinput-shared-fourier/README.md @@ -0,0 +1,212 @@ +# Exact shared Fourier cancellation at arbitrary arity + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped algebraic proof with finite corroboration; no new kappa.** For a +product of k independent inputs, a shared phase-weighted Fourier routine can +have a translated read layout and nontrivial phases. This happens precisely +under the torsion and root-of-unity conditions below. At two inputs the result +reduces to Hanson Sun's [PR1477](https://github.com/CrocSwap/integer-mult-bounds/pull/1477) +phase-free criterion, which builds on Ross Richardson's +[PR940](https://github.com/CrocSwap/integer-mult-bounds/pull/940). + +The new repository contribution is the exact higher-arity classification and +its count, including a three-input translated example. The coefficient method, +Fourier duality and the two-input result are predecessor work. No literature +priority for elementary character algebra is claimed. No predecessor verifier +is replayed or incorporated as the deliverable. + +## Statement + +Let G be a finite product of cyclic groups Z/q_i, each q_i>=2, let N=|G|, +and use the symmetric nondegenerate pairing + + chi(x,y) = exp(2*pi*i*sum_i x_i*y_i/q_i). + +Both Fourier signs have normalization 1/N. A read permutation means +`(P_pi f)(x)=f(pi(x))`, and `D_w` multiplies coordinate x by w(x), where +|w(x)|=1. Set + + A = D_w P_pi F^-, bar(A) = D_conj(w) P_pi F^+. + +For any integer k>=2, the identity + + bar(A)[ product_(j=1)^k A(u_j) ] = (u_1 * ... * u_k)/N^k (1) + +holds for every independent tuple u_j in C^G if and only if + + pi(x) = L(x)+b, + L is a self-adjoint group automorphism, + (k-1)b = 0 in G, + w(x) = c*chi(-x,b), |c|=1, c^(k-1)=1. (2) + +Self-adjoint means `chi(Lx,y)=chi(x,Ly)` for the actual product-group +pairing. Unequal cyclic factors do not in general use ordinary matrix transpose. +Convolution in (1) is unnormalized. The product inside the transform is pointwise. +The bar on A means coefficientwise conjugation, not its adjoint or inverse. + +For example on Z/2 at k=3, take `pi(x)=x+1` and `w=(1,-1)`. +It satisfies (1) for all three inputs. The same routine fails at k=2. +Thus the two-input phase prohibition does not extend to all arities. +On Z/2 the constant phase i fails at k=3 and succeeds at k=5. + +## Proof + +Write f_j=F^-u_j. These range independently over all functions on G. +The ordinary normalized convolution identity gives +`F^+(product_j f_j)=(u_1*...*u_k)/N^k`. +For each output x, compare the coefficient of +`product_j f_j(pi(y))`. Since pi is bijective, exactly one coordinate y +contributes to that monomial. Consequently (1) is equivalent to + + conj(w(x))*w(y)^k*chi(pi(x),y) = chi(x,pi(y)) for all x,y. (3) + +Set y=x. Symmetry cancels the character factors and |w(x)|=1 gives +`w(x)^(k-1)=1` for every x. Hence `w(x)^k=w(x)`. +Set b=pi(0) and c=w(0). Taking y=0 in (3) gives +`conj(w(x))*c=chi(x,b)`, so `w(x)=c*chi(-x,b)`. +At x=0 the pointwise root condition gives `c^(k-1)=1`. +For all x it then gives `chi(x,(k-1)b)=1`. Nondegeneracy forces +`(k-1)b=0`. + +Substitute these weights into (3) and put `L(x)=pi(x)-b`. All offset +characters cancel. What remains is + + chi(L(x),y) = chi(x,L(y)) for all x,y. (4) + +For any x,z,y, the right side of (4) is multiplicative in x, so +`chi(L(x+z)-L(x)-L(z),y)=1`. Nondegeneracy forces additivity of L. +Subtracting b preserves bijectivity, so L is an automorphism, and (4) +is exactly self-adjointness. This proves necessity. + +Conversely, (2) gives `w(y)^k=w(y)`. Self-adjointness and symmetry imply + + conj(w(x))*w(y)*chi(Lx+b,y) + = chi(x,b)*chi(-y,b)*chi(Lx,y)*chi(b,y) + = chi(x,Ly+b). + +This is (3), proving sufficiency and (1) for all complex inputs. +The argument is a written all-group proof, not a proof-kernel certificate. + +## Exact finite count + +Restrict w to the Mth roots of unity, where M is a multiple of the exponent +of G. Write S(G) for the number of self-adjoint automorphisms and G[t] for +the subgroup killed by t. The exact number of shared routines at arity k is + + S(G) * |G[k-1]| * gcd(M,k-1). (5) + +Indeed L, b and c in (2) are uniquely recoverable from pi,w. There are S(G) +choices for L, |G[k-1]| choices for b and gcd(M,k-1) choices for c. +All resulting character weights are Mth roots. For a cyclic-factor +presentation, `|G[k-1]|=product_i gcd(q_i,k-1)`. + +The declared exhaustive census uses M=lcm(4,q_i) and k=2,3,4,5. +It compares the literal coefficient equation (3) with reconstruction of +(2), including an explicit additivity check, for every permutation and phase +vector. It also checks (5). + +| G | M | Candidates per arity | k=2 accepted | k=3 | k=4 | k=5 | +|---|---:|---:|---:|---:|---:|---:| +| Z/2 | 4 | 32 | 1 | 4 | 1 | 8 | +| Z/3 | 12 | 10,368 | 2 | 4 | 18 | 8 | +| Z/4 | 4 | 6,144 | 2 | 8 | 2 | 32 | +| (Z/2)^2 | 4 | 6,144 | 4 | 32 | 4 | 64 | + +The two-input column is inherited mathematics and a boundary control. +The higher-arity columns corroborate the new classification. PRIMARY.json +is generated by verify.py and binds its ordered classification stream and +source hashes. It is not a handwritten receipt. + +oracle.py imports no primary or predecessor code. It performs the actual +unnormalized negative Fourier passes, pointwise products, conjugate positive +pass and direct cyclic convolution over the exact rings Z[i] and +Z[z]/(z^4-z^2+1), where z is a primitive twelfth root. +Scaling both sides by N^(k+1) makes the expected output N times the integer +convolution. It checks every basis input tuple for every admitted map, plus +one dense integer tuple per map. ORACLE.json is its generated source-bound +receipt. Seven separate semantic controls exhaust their basis domains, +including wrong arity, a forbidden torsion shift, a wrong character sign and +a non-self-adjoint linear map. No rejected-case root cause is inferred from a +mere count. The complete census checks necessity through (3); the separate +transform replay corroborates the admitted cases and named controls. + +## Reproduce + +From the repository root, with the standard library and CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/multiinput-shared-fourier +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/multiinput-shared-fourier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/multiinput-shared-fourier/oracle.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/multiinput-shared-fourier --check-source-history +``` + +On another host, substitute its CPython 3.12 path. The registered manifest runs +both verifiers normally and optimized, with warnings as errors. Each default +run reads and compares its full receipt and writes nothing. Explicit +`--write NEW_PATH` generates a fresh receipt and refuses an occupied path. +The two predecessor READMEs are hash-bound live inputs, so a standalone source +export must retain them at their declared repository-relative paths. + +## Limits and engineering choices + +This is exact algebra for k independent functions and unit-modulus weights. +It supplies no physical Fourier schedule, free phase application, rounded +implementation, tape route, supplier recurrence, complete multiplication theorem +or selected-frontier change. All existing ownership, restoration, native, +compiler, precision and analytic transfer obligations remain separate. +Independent human and formal proof-kernel review are unclaimed. + +The fixed census has at most four points, twelve phase choices per coordinate +and four arities. The reference classifier rejects groups above 64 points, +more than three factors, factors outside 2..8 and arities outside 2..64. +These executable limits do not narrow the written theorem. +Loops have finite collection bounds; there is no recursion or dynamic code. +Functions fit within 60 physical lines. Python requires dynamic allocation +and arbitrary-precision integers. This is a Power of Ten rule 3 deviation for +the two finite verifiers: the fixed enumeration domain bounds all live vectors, +ring degrees and integer sizes, and no whole census stream is retained. +The classifier has at most 64 points and its fixed census has at most four. +The oracle uses at most five inputs, four points and ring degree four. +The compensating checks are the exhaustive replay and capacity rejection +controls. Reassess the bounds before expanding the executable domain. +Diagnostics use warnings as errors and optimized replay; no new shared +repository build configuration is changed. + +## Open next questions + +Can one actual three-input convolution caller absorb the permitted two-torsion +shift and its character weights at lower complete cost? Start with one literal +three-input schedule and the Z/2 translated fixture, then price every read map, +phase, intermediate product, restoration and output conversion. No such physical +schedule or favorable invoice is supplied here, so algebraic permission alone +cannot justify a construction expansion. + +Can separately weighted, separately addressed forward routines be classified +for k inputs with a shared final contract? Start by comparing multilinear +coefficients before assuming the forward addresses agree. PR1477 settles the +two-input independent-map case. Physical relevance and a cost advantage remain +unestablished; this follow-on was not pursued after the first verified result. + +## Sources and credit + +Canonical base is 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7. +The selected record remains kappa=0.00302015. Source-bound orientation passed; +the full selected supplier was not replayed. + +Hanson Sun's PR1477 at f24bb18c20f7bdb3cbc27a1b6a010babf427d6cc supplies +the phase-weighted coefficient method and two-input classification. +Ross Richardson's PR940 at fccac36fa9bcc063c4fda733299a22349ce10e56 supplies +the unweighted adjoint criterion. Their READMEs and inherited source notices +remain unchanged. The retained Fourier manuscript and CrocSwap construction +supply the normalization and application context. SOURCES.json binds the exact +retained predecessor bytes at the canonical base; replay requires no pending +branch or imported predecessor executable. + +The [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133995) +reserves this higher-arity question. Overlap checks covered live open PRs, +recent handoffs and active Discussions, this account's recent work, targeted +merged searches and main's READMEs. They are bounded novelty checks, not a +literature-priority guarantee. TASK.json records the scope change from the +current audit card to this original interface extension. diff --git a/research/multiinput-shared-fourier/SOURCES.json b/research/multiinput-shared-fourier/SOURCES.json new file mode 100644 index 0000000000..b12391baf8 --- /dev/null +++ b/research/multiinput-shared-fourier/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/source-permutation-audit/README.md", + "usage": "input", + "git_blob": "33e7cbafd02bd70d3d83e489f4b67a37adcf68d5", + "sha256": "157a31ee176ceb86243f025cf7fd896bac438a3834a2d49d0be6fb223d78bd0e" + }, + { + "path": "research/weighted-fourier-layout/README.md", + "usage": "input", + "git_blob": "7cd23891f12ea1f054ed778289bc45a7e8fb622e", + "sha256": "676e107f9e312a36793ec87ca9eec3df3c8764c71268153055c2d6064a40e79e" + } + ] +} diff --git a/research/multiinput-shared-fourier/TASK.json b/research/multiinput-shared-fourier/TASK.json new file mode 100644 index 0000000000..edd3a21c8d --- /dev/null +++ b/research/multiinput-shared-fourier/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.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 PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "changed", + "actual_scope": "Exact shared-conjugate Fourier cancellation and routine count for products of k>=2 independent inputs on all finite products of cyclic groups.", + "scope_change_reason": "The user requested original research, not a predecessor audit. Change the current caller-audit card to an original higher-arity extension of Hanson Sun PR1477 and Ross Richardson PR940.", + "bottleneck_link": "Side-result interface theorem: it permits specific affine/phase layouts in higher-arity convolution. Complete physical cost is unknown, so no supplier gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved classification and its bounded exact corroboration; do not synthesize a physical schedule or extend the census.", + "outcome": "completed", + "evidence": "README proof of (2) and (5), exhaustive coefficient/normal-form census, separate exact transform/convolution replay and generated source-bound PRIMARY.json and ORACLE.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a literal three-input convolution caller absorb the permitted two-torsion shift and character weights at lower complete cost?", + "why_it_matters": "Algebraic permission only helps if the whole physical bill improves.", + "first_step": "Choose one literal three-input schedule and price the Z/2 translated fixture, including reads, phases, products, restoration and output conversion.", + "blocked_by": "No physical caller or favorable complete invoice is constructed." + }, + { + "question": "What is the exact k-input criterion with separately weighted and addressed forward routines?", + "why_it_matters": "It would describe the asymmetric higher-arity interface beyond this shared-routine contract.", + "first_step": "Compare independent multilinear coefficients, using PR1477 only for its two-input case.", + "blocked_by": "Not pursued after the first verified result; no physical benefit is known." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133995" + }, + "overlap": { + "checked_utc": "2026-10-22T22:37:09Z", + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "coverage": "100 live open PRs with bodies; 60 recent account PRs; latest 30 handoff comments and 12 active Discussions; main README terms; targeted merged searches. Search is bounded and unpublished work is not covered.", + "distinct_delta": "k>=3 shared-routine affine/phase classification and exact routine count; no predecessor numerical replay as deliverable." + } +} diff --git a/research/multiinput-shared-fourier/VERIFY.json b/research/multiinput-shared-fourier/VERIFY.json new file mode 100644 index 0000000000..fd71fe96aa --- /dev/null +++ b/research/multiinput-shared-fourier/VERIFY.json @@ -0,0 +1,58 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/source-permutation-audit/README.md", + "research/weighted-fourier-layout/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exhaustive exact coefficient versus affine normal-form classification, count formula, semantic and capacity controls; compare generated source-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exhaustive exact coefficient versus affine normal-form classification, count formula, semantic and capacity controls; compare generated source-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 240, + "checks": "Literal exact Fourier/product/convolution replay of every admitted basis tuple and dense inputs; named counterexamples; compare generated source-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 240, + "checks": "Literal exact Fourier/product/convolution replay of every admitted basis tuple and dense inputs; named counterexamples; compare generated source-bound receipt." + } + ] +} diff --git a/research/multiinput-shared-fourier/oracle.py b/research/multiinput-shared-fourier/oracle.py new file mode 100644 index 0000000000..e28a10d5b2 --- /dev/null +++ b/research/multiinput-shared-fourier/oracle.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Literal exact Fourier passes and cyclic convolution; no primary import.""" +import argparse +import hashlib +import json +from itertools import permutations, product +from math import lcm +from pathlib import Path + +ROOT = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def roots(period): + need(period in (4, 12), 'unsupported exact root ring') + degree = 2 if period == 4 else 4 + result = [] + for exponent in range(period): + poly = [0] * (period + 1) + poly[exponent] = 1 + for power in range(period, degree - 1, -1): + coefficient = poly[power] + poly[power] = 0 + poly[power - degree] -= coefficient + if period == 12: + poly[power - 2] += coefficient + result.append(tuple(poly[:degree])) + return tuple(result) + + +def add(left, right): + return tuple(a + b for a, b in zip(left, right)) + + +def multiply(left, right): + degree = len(left) + poly = [0] * (2 * degree - 1) + for i, a in enumerate(left): + for j, b in enumerate(right): + poly[i + j] += a * b + for power in range(2 * degree - 2, degree - 1, -1): + coefficient = poly[power] + poly[power] = 0 + poly[power - degree] -= coefficient + if degree == 4: + poly[power - 2] += coefficient + return tuple(poly[:degree]) + + +def pairing(left, right, moduli, period): + return sum(a * b * (period // q) + for a, b, q in zip(left, right, moduli)) % period + + +def transform(vector, moduli, points, permutation, phases, sign, table): + period = len(table) + zero = (0,) * len(table[0]) + output = [] + for x, address in enumerate(permutation): + total = zero + for y, value in enumerate(vector): + exponent = sign * pairing(points[address], points[y], moduli, period) + total = add(total, multiply(table[exponent % period], value)) + output.append(multiply(table[phases[x] % period], total)) + return tuple(output) + + +def literal(inputs, moduli, points, permutation, phases, table): + values = [table[0]] * len(points) + for vector in inputs: + forward = transform(vector, moduli, points, permutation, phases, -1, table) + values = [multiply(a, b) for a, b in zip(values, forward)] + return transform(values, moduli, points, permutation, + tuple(-w for w in phases), 1, table) + + +def convolution(inputs, moduli, points): + lookup = {point: i for i, point in enumerate(points)} + values = list(inputs[0]) + for vector in inputs[1:]: + output = [0] * len(points) + for x, a in enumerate(values): + for y, b in enumerate(vector): + address = tuple((i + j) % q for i, j, q + in zip(points[x], points[y], moduli)) + output[lookup[address]] += a * b + values = output + return tuple(values) + + +def descriptions(moduli, arity, points, period): + lookup = {point: i for i, point in enumerate(points)} + for permutation in permutations(range(len(points))): + offset = points[permutation[0]] + linear = tuple(tuple((a - b) % q for a, b, q + in zip(points[p], offset, moduli)) for p in permutation) + symmetric = all(pairing(linear[x], points[y], moduli, period) + == pairing(points[x], linear[y], moduli, period) + for x in range(len(points)) for y in range(len(points))) + additive = all(linear[lookup[tuple((a + b) % q for a, b, q + in zip(x, y, moduli))]] + == tuple((a + b) % q for a, b, q + in zip(linear[i], linear[j], moduli)) + for i, x in enumerate(points) for j, y in enumerate(points)) + if not symmetric or not additive: + continue + if any((arity - 1) * b % q for b, q in zip(offset, moduli)): + continue + for constant in range(period): + if (arity - 1) * constant % period == 0: + phases = tuple((constant - pairing(x, offset, moduli, period)) % period + for x in points) + yield permutation, phases + + +def basis_replay(): + maps = tuples = dense = 0 + digest = hashlib.sha256() + for moduli in ((2,), (3,), (4,), (2, 2)): + points = tuple(product(*(range(q) for q in moduli))) + size, period = len(points), lcm(4, *moduli) + table = roots(period) + zero = (0,) * len(table[0]) + basis = tuple(tuple(table[0] if x == y else zero for x in range(size)) + for y in range(size)) + for arity in range(2, 6): + for permutation, phases in descriptions(moduli, arity, points, period): + maps += 1 + forward = tuple(transform(v, moduli, points, permutation, + phases, -1, table) for v in basis) + for addresses in product(range(size), repeat=arity): + values = [table[0]] * size + for address in addresses: + values = [multiply(a, b) for a, b in zip(values, forward[address])] + actual = transform(values, moduli, points, permutation, + tuple(-w for w in phases), 1, table) + total = tuple(sum(points[a][i] for a in addresses) % q + for i, q in enumerate(moduli)) + expected = tuple(tuple(size * c for c in table[0]) + if point == total else zero for point in points) + need(actual == expected, 'literal basis mismatch') + digest.update(json.dumps(actual, separators=(',', ':')).encode()) + tuples += 1 + inputs = tuple(tuple((j + 1) * (x + 1) - 2 for x in range(size)) + for j in range(arity)) + embedded = tuple(tuple(tuple(a * c for c in table[0]) for a in v) + for v in inputs) + actual = literal(embedded, moduli, points, permutation, phases, table) + expected = tuple(tuple(size * a * c for c in table[0]) + for a in convolution(inputs, moduli, points)) + need(actual == expected, 'dense convolution mismatch') + dense += 1 + return dict(maps=maps, basis_tuples=tuples, dense_tuples=dense, + output_sha256=digest.hexdigest()) + + +def semantic_controls(): + cases = ( + ((2,), 2, (1, 0), (0, 2), False), + ((2,), 3, (1, 0), (0, 2), True), + ((2,), 3, (0, 1), (1, 1), False), + ((2,), 5, (0, 1), (1, 1), True), + ((3,), 3, (1, 2, 0), (0, 8, 4), False), + ((4,), 5, (1, 2, 3, 0), (0, 1, 2, 3), False), + ((2, 2), 3, (0, 1, 3, 2), (0, 0, 0, 0), False), + ) + observations = [] + for moduli, arity, permutation, phases, expected in cases: + points = tuple(product(*(range(q) for q in moduli))) + period, size = lcm(4, *moduli), len(points) + table = roots(period) + zero = (0,) * len(table[0]) + failures = 0 + for addresses in product(range(size), repeat=arity): + inputs = tuple(tuple(table[0] if i == a else zero for i in range(size)) + for a in addresses) + actual = literal(inputs, moduli, points, permutation, phases, table) + total = tuple(sum(points[a][i] for a in addresses) % q + for i, q in enumerate(moduli)) + wanted = tuple(tuple(size * c for c in table[0]) + if point == total else zero for point in points) + failures += actual != wanted + need((failures == 0) == expected, 'semantic control failed') + observations.append(dict(group=moduli, arity=arity, failures=failures, + permutation=permutation, phases=phases)) + return observations + + +def binding(): + sources = json.loads((ROOT / 'SOURCES.json').read_text()) + for row in sources['files']: + if row['usage'] == 'input': + data = (ROOT.parent.parent / row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], 'source drift') + return {name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + for name in ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', + 'verify.py', 'oracle.py')} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path) + args = parser.parse_args() + result = dict(schema='multiinput-shared-fourier-oracle/v1', source_sha256=binding(), + replay=basis_replay(), controls=semantic_controls()) + result = json.loads(json.dumps(result)) + if args.write is None: + need(result == json.loads((ROOT / 'ORACLE.json').read_text()), 'oracle receipt mismatch') + else: + with args.write.open('x') as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + '\n') + print('PASS_MULTIINPUT_FOURIER_ORACLE', json.dumps(result['replay'], sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/multiinput-shared-fourier/verify.py b/research/multiinput-shared-fourier/verify.py new file mode 100644 index 0000000000..b00186bef7 --- /dev/null +++ b/research/multiinput-shared-fourier/verify.py @@ -0,0 +1,168 @@ +#!/usr/bin/env python3 +"""Exhaust the declared monomial coefficient census using integer turns.""" +import argparse +import hashlib +import json +from itertools import permutations, product +from math import gcd, lcm, prod +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +GROUPS = ((2,), (3,), (4,), (2, 2)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def geometry(moduli): + need(isinstance(moduli, tuple) and 1 <= len(moduli) <= 3, "invalid factors") + need(all(type(q) is int and 2 <= q <= 8 for q in moduli), "invalid modulus") + need(prod(moduli) <= 64, "group too large") + points = tuple(product(*(range(q) for q in moduli))) + period = lcm(4, *moduli) + pairing = tuple(tuple(sum(a * b * (period // q) + for a, b, q in zip(x, y, moduli)) % period + for y in points) for x in points) + return points, period, pairing + + +def validate(arity, permutation, weights, size, period): + need(type(arity) is int and 2 <= arity <= 64, "invalid arity") + need(len(permutation) == size and all(type(x) is int for x in permutation), + "invalid permutation shape") + need(sorted(permutation) == list(range(size)), "not a permutation") + need(len(weights) == size and all(type(x) is int and 0 <= x < period + for x in weights), "invalid phases") + + +def coefficient_rule(arity, permutation, weights, pairing, period): + size = len(pairing) + validate(arity, permutation, weights, size, period) + return all((arity * weights[y] - weights[x] + pairing[permutation[x]][y] + - pairing[x][permutation[y]]) % period == 0 + for x in range(size) for y in range(size)) + + +def normal_form(moduli, arity, permutation, weights, points, period, pairing): + size = len(points) + validate(arity, permutation, weights, size, period) + offset = points[permutation[0]] + lookup = {point: i for i, point in enumerate(points)} + linear = tuple(lookup[tuple((a - b) % q for a, b, q + in zip(points[p], offset, moduli))] + for p in permutation) + if any((arity - 1) * b % q for b, q in zip(offset, moduli)): + return False + if (arity - 1) * weights[0] % period: + return False + if any(weights[x] != (weights[0] - pairing[x][permutation[0]]) % period + for x in range(size)): + return False + for x in range(size): + for y in range(size): + total = lookup[tuple((a + b) % q for a, b, q + in zip(points[x], points[y], moduli))] + image = tuple((a + b) % q for a, b, q + in zip(points[linear[x]], points[linear[y]], moduli)) + if points[linear[total]] != image: + return False + if pairing[linear[x]][y] != pairing[x][linear[y]]: + return False + return True + + +def census(): + rows = [] + digest = hashlib.sha256() + for moduli in GROUPS: + points, period, pairing = geometry(moduli) + size = len(points) + for arity in range(2, 6): + candidates = accepted = symmetric = 0 + for permutation in permutations(range(size)): + if permutation[0] == 0 and all(pairing[permutation[x]][y] + == pairing[x][permutation[y]] + for x in range(size) for y in range(size)): + symmetric += 1 + for weights in product(range(period), repeat=size): + actual = coefficient_rule(arity, permutation, weights, pairing, period) + predicted = normal_form(moduli, arity, permutation, weights, + points, period, pairing) + need(actual == predicted, "normal-form disagreement") + candidates += 1 + accepted += actual + digest.update(bytes((int(actual),))) + torsion = prod(gcd(arity - 1, q) for q in moduli) + expected = symmetric * torsion * gcd(arity - 1, period) + need(accepted == expected, "closed count disagreement") + rows.append(dict(group=moduli, arity=arity, period=period, + candidates=candidates, accepted=accepted, + self_adjoint_automorphisms=symmetric, + torsion=torsion)) + return dict(rows=rows, candidates=sum(r['candidates'] for r in rows), + accepted=sum(r['accepted'] for r in rows), + classification_sha256=digest.hexdigest()) + + +def controls(): + points, period, pairing = geometry((2,)) + good = (3, (1, 0), (0, 2)) + need(coefficient_rule(*good, pairing, period), "ternary translated fixture") + need(not coefficient_rule(2, good[1], good[2], pairing, period), + "bilinear translation must fail") + need(not coefficient_rule(3, (0, 1), (1, 1), pairing, period), + "constant i must fail at arity three") + need(coefficient_rule(5, (0, 1), (1, 1), pairing, period), + "constant i must pass at arity five") + cases = ((1, (0, 1), (0, 0)), (65, (0, 1), (0, 0)), + (True, (0, 1), (0, 0)), (3, (0, 0), (0, 0)), + (3, (0,), (0, 0)), (3, (0, 1), (4, 0)), + (3, (0, 1), (0,)), (3, (False, 1), (0, 0))) + for args in cases: + try: + coefficient_rule(*args, pairing, period) + except ValueError: + continue + raise ValueError("invalid-input control accepted") + for factors in ((), (1,), (2, 2, 2, 2), (8, 8, 8)): + try: + geometry(factors) + except ValueError: + continue + raise ValueError("invalid-group control accepted") + return dict(semantic=4, invalid_inputs=len(cases) + 4) + + +def source_binding(): + manifest = json.loads((ROOT / 'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage'] == 'input': + data = (ROOT.parent.parent / row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], "source drift") + names = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', + 'verify.py', 'oracle.py') + return {name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + for name in names} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path) + args = parser.parse_args() + result = dict(schema='multiinput-shared-fourier-primary/v1', + source_sha256=source_binding(), census=census(), controls=controls()) + result = json.loads(json.dumps(result)) + if args.write is None: + expected = json.loads((ROOT / 'PRIMARY.json').read_text()) + need(result == expected, "primary receipt mismatch") + else: + with args.write.open('x') as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + '\n') + print('PASS_MULTIINPUT_SHARED_FOURIER', result['census']['candidates'], + 'candidates;', result['census']['accepted'], 'accepted') + + +if __name__ == '__main__': + main()