diff --git a/research/composite-chirp-phase-repair/PROOF.md b/research/composite-chirp-phase-repair/PROOF.md new file mode 100644 index 0000000000..8bbba936cb --- /dev/null +++ b/research/composite-chirp-phase-repair/PROOF.md @@ -0,0 +1,146 @@ +# Rank-optimal folding and the exact phase-repair count + +This is a scoped algebraic construction over the complex numbers. All inputs +are arbitrary vectors. No tape, dirty-scratch, rounded-arithmetic or selected +supplier contract is implicit in the matrix identities. + +## Statement + +Let n be any positive odd integer, let a,b be integers, and write + +``` +zeta = exp(2 pi i/n), g = gcd(a,n), m = n/g, +K_b[j,k] = zeta^(a(j-k)^2 + b(j-k)), 0 <= j,k < n. +``` + +Reducing a and b modulo n does not change the operator. The convention +gcd(0,n)=n includes a=0 and n=1. + +1. K_b factors through exactly m coordinates. Its rank is m, and each of its + m nonzero singular values is sqrt(n g). No linear factorization through + fewer coordinates exists. +2. A sum of q scalar-weighted chirps with this fixed a, and arbitrary linear + phase twists b, has rank at most m times the number of distinct b modulo g + that occur, hence at most qm. An invertible sum requires at least g terms. +3. Exactly g terms suffice. The explicit sum S=sum_(b=0)^(g-1) K_b satisfies + S* S = n g I, so S is invertible, has condition number one, and + S^(-1)=S*/(n g). Here * denotes conjugate transpose. With one representative + of each residue and nonzero scalar weights c_b, the singular values are + sqrt(n g)|c_b|, each repeated m times. + +The minimum repair count is for this specified family of complete chirp +operators. It is not a lower bound for circuits using different quadratic +coefficients, arbitrary additional native operations, or nonlinear encodings. + +## Explicit factorization + +Define the n-by-m phased replication E_b and the m-by-m reduced chirp C by + +``` +E_b[j,r] = zeta^(bj) if j = r mod m, and 0 otherwise, +C[s,r] = zeta^(a(s-r)^2) = exp(2 pi i (a/g)(s-r)^2/m). +``` + +Then + +``` +K_b = E_b C E_b*. +``` + +Indeed, for fixed j,k only s=j mod m and r=k mod m contribute to this +matrix entry. Its exponent is bj+a(s-r)^2-bk. Since j-k=s-r+hm for some +integer h, the difference from a(j-k)^2+b(j-k) is a multiple of n. Both +2 a m h(s-r) and a m^2 h^2 are multiples of n because a m=(a/g)n. +This proves the identity entry by entry, without cancellation or numerical +approximation. Thus the program is a phased fold E_b*, the reduced chirp C, +and a phased replication E_b. It preserves every input contribution. + +The columns of E_b have disjoint supports and squared norm g, hence +E_b*E_b=gI. Put a'=a/g. Since gcd(a',m)=1 and m is odd, 2a' is a unit +modulo m. Character orthogonality gives + +``` +(C C*)[s,t] + = exp(2 pi i a'(s^2-t^2)/m) + sum_(r=0)^(m-1) exp(-2 pi i 2a'(s-t)r/m) + = m if s=t, and 0 otherwise. +``` + +Consequently C is nonsingular and both C C* and C*C equal mI. Because E_b +is injective and E_b* is surjective, rank(K_b)=m. Rank cannot increase +through an intermediate vector space, proving that this intermediate +dimension is optimal among all complex linear factorizations. + +## Orthogonal phase classes and the sharp repair + +For fixed r, the only possible overlap of columns of E_b and E_c is + +``` +(E_b* E_c)[r,r] + = zeta^((c-b)r) sum_(h=0)^(g-1) exp(2 pi i (c-b)h/g). +``` + +It is zero unless b=c modulo g. If b=c modulo g, E_b and E_c have the +same range, because their corresponding columns differ by a nonzero +scalar. Thus there are exactly g mutually orthogonal m-dimensional ranges +V_0,...,V_(g-1), and their direct sum is the whole n-dimensional space. +The orthogonal projector onto V_b is P_b=E_b E_b*/g. + +The factorization shows that the image of K_b is V_b and that K_b +annihilates its orthogonal complement. Direct multiplication gives + +``` +K_b* K_b = E_b C* (gI) C E_b* = n g P_b. +``` + +For different residues, K_b* K_c=0, because E_b*E_c=0. A sum using only +q distinct residues has image inside their direct sum and rank at most qm. +If it omits any residue it cannot be invertible. In particular, fewer +than g individual chirps cannot repair the rank defect, even if their +phases and scalar coefficients are chosen freely. + +Conversely, choose b=0,...,g-1 and nonzero complex c_b. The cross terms in +the Gram matrix vanish, giving + +``` +(sum c_b K_b)* (sum c_b K_b) = n g sum |c_b|^2 P_b. +``` + +Every projector has rank m and the projectors sum to I. This proves the +weighted singular-value statement. Taking every c_b=1 proves the explicit +inverse, exact conditioning and attainment of the lower count g. + +## Consequence and limits for composite axes + +For n=9,a=3 the reduced dimension is three, and exactly three twists repair +invertibility. For n=45,a=15 the reduced dimension is also three, but fifteen +twists are necessary. Using several twists from the same residue class +cannot compensate for a missing class. If a is a unit modulo an odd composite +n, then g=1 and a single chirp is already nonsingular and perfectly conditioned. + +These are algebraic options and obstructions for a possible composite-axis +consumer following David Ganz's PR5564. That package supplies coprime axes and +CRT streams, not this phase-only convolution or its physical implementation. +No claim is made that a particular published Gaussian resampler uses K_b. +A caller must identify its actual kernel and coefficient a before applying +this result. A real Gaussian kernel with nonconstant magnitudes is a different +operator. Physical delivery, phase manufacture, exact/rounded normalization, +movement, owned restoration, storage, recursive prices and complete recovery +remain unpriced. The selected assumptions and kappa are unchanged. + +The proof uses classical finite-character orthogonality, the same elementary +ingredient behind quadratic Gauss sums. The construction and constrained +repair interface are the repository contribution; global novelty of Gauss-sum +rank or magnitude identities is unclaimed. NIST's +[Gauss-sum reference](https://dlmf.nist.gov/20.11.i) provides classical context. +No external Gauss-sum evaluation or phase formula is needed in this proof. + +## Verification scope + +Finite-field evaluations are exact ring images of the phase identities, not +complex numerical approximations. The verifier separately reduces literal +complex Gram polynomials modulo the integer cyclotomic polynomial Phi_n. +It also obtains finite-field ranks by dense row elimination and tests phase +subsets and the attaining inverse. These corroborate the written proof and +the bounded implementation. They do not replace the universal argument or +constitute independent human or formal proof-kernel review. diff --git a/research/composite-chirp-phase-repair/README.md b/research/composite-chirp-phase-repair/README.md new file mode 100644 index 0000000000..eb465fe53e --- /dev/null +++ b/research/composite-chirp-phase-repair/README.md @@ -0,0 +1,148 @@ +# Rank-optimal folding and sharp phase repair for composite cyclic chirps + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +Claim type: scoped algebraic construction and sharp lower bound, with exact +finite corroboration. For every positive odd axis n, let + +``` +K_b[j,k] = exp(2 pi i (a(j-k)^2+b(j-k))/n), +g = gcd(a,n), m = n/g. + +K_b = phased replication[n <- m] + * nonsingular reduced chirp[m <- m] + * phased fold[m <- n]. +``` + +The intermediate dimension m is optimal. A sum of chirps with this same +quadratic coefficient needs at least g phase twists to become invertible. +Exactly g attain the bound, and the explicit sum S of twists b=0,...,g-1 +has S* S=n g I. Its condition number is one and its inverse is S*/(n g). +For n=9,a=3 this reduces a nine-coordinate operator to three coordinates +and requires three twists to repair invertibility. For n=45,a=15 the +reduced dimension is again three, while the minimum repair count is fifteen. + +[PROOF.md](PROOF.md) proves the universal statement and supplies every +matrix in the factorization. The lower bound permits arbitrary scalar +weights and arbitrary linear phase parameters within this fixed quadratic +family. Repeated phase residues cannot compensate for a missing residue. +The result includes the nonsingular unit-coefficient case on composite axes. + +## Connection and credit + +David Ganz / Dugongue's [PR5564](https://github.com/CrocSwap/integer-mult-bounds/pull/5564) +constructs prime-free coprime axes and leaves a complete composite-axis +numerical caller open. This is one algebraic side result for that question. +It supplies a rank-optimal implementation of a possible phase-only cyclic +convolution, together with the exact cost of repairing its rank in its own +term alphabet. It does not identify this operator with an existing real +Gaussian resampler. The actual caller and complete physical bill remain open. +No predecessor scientific verifier is imported or replayed as the deliverable. + +Finite-character orthogonality and quadratic Gauss-sum algebra are classical; +see [NIST DLMF](https://dlmf.nist.gov/20.11.i). Global novelty of those facts is +unclaimed. The new repository contribution is the explicit folding/replication +interface, sharp constrained phase-repair construction and bounded exact +implementation. Credit PR5564's retained ToikY, Jose Manuel, Tekalign, Cinna +Davis, Chafik Boukhalfa, Josie Elliston and Harvey–van der Hoeven lineage. +Its source credit and files are unchanged. + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/composite-chirp-phase-repair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/composite-chirp-phase-repair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/composite-chirp-phase-repair +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/composite-chirp-phase-repair --check-source-history +``` + +Another CPython 3.12 executable can replace the absolute local path. +The direct checker prints `PASS_COMPOSITE_CHIRP_PHASE_REPAIR` in a generated +JSON receipt bound to all eight package files. It writes no files. No receipt +is handwritten. The registered hook runs normal and optimized modes. + +`chirp.py` implements the factorization. `oracle.py` imports no part of that +implementation: it builds literal dense matrices, performs finite-field +elimination and constructs integer cyclotomic polynomials by exact division. +The verifier checks all odd n through 31 and every a,b modulo n for the +factorization, with complete basis inputs through n=9. Literal modular ranks, +complex cyclotomic Gram entries and the complete attaining inverse use the +separately declared smaller domains. Every subset of phase residues is tested +when n<=15 and g<=9. The generated receipt enumerates 5,456 factorization +cases, 3,344,528 phase entries, 1,225 basis vectors, 127 modular ranks, +16,255 cyclotomic Gram entries, 890 phase subsets and 8,128 inverse entries +across 64 repair families. No floating-point rank or complex tolerance is used. + +Controls exercise invalid dimensions, coefficient types and bounds, malformed +ring evaluations, omitted twists, repeated phase residues, a nonprimitive root +that hides rank, and the failure of the odd-axis rank formula at n=4. Acceptance +checks use exceptions and remain enabled with optimization. All seventeen +listed domain/semantic controls pass. + +## Scope and implementation bounds + +This is a linear-algebra theorem and a reference implementation, not a finite +certificate for the selected supplier or a complete multiplication theorem. +No new kappa or selected-assumption discharge is claimed. Phase manufacture, +rounded normalization, input encoding, native calls, movement, owned workspace +restoration, compiler stock, physical time/storage and the whole recovery +contract remain unpriced and unrun. No selected cold replay, Lean or Docker +run is part of this contribution. Matrix conditioning alone supplies no rounded +implementation theorem. An odd composite modulus alone does not cause a defect; +the decisive quantity for this operator is gcd(a,n). + +The theorem has no size cap. The executable accepts odd n<=255, coefficients +of at most 256 bits, modular rings of size at most 1,000,000 and n input +coordinates. It evaluates in the supplied ring and needs only a root whose +order divides n. Complex rank checks additionally use independently certified +prime fields with primitive roots; a nonprimitive evaluation is explicitly +not accepted as evidence of complex rank. Verification axes are at most 31, +the independent field-search axis cap is 63, and every search is bounded. + +Power of Ten review: no recursion, external process, dynamic code generation, +mutable global state or acceptance assertions occur in the new computation. +All functions fit within sixty lines. Domain limits bound every loop; field +search has 1,023 prime candidates and fewer than 64,514 root candidates per +candidate. Every verifier matrix has at most 31 squared entries. The repair +census retains two families of at most fifteen phase matrices plus their sums. +Every reference-API array has at most 255 entries, including the folded and +middle arrays, phase table and input/output vectors. +Python allocation is a rule-3 deviation forced by its managed integer/list +runtime. These enforced finite domains and bounded live arrays are the +compensating controls; a fixed-allocation native implementation remains future +work. No allocation-free runtime or bit-cost theorem is asserted. Warning-strict +normal/optimized execution and AST/compilation inspection supply diagnostics. +No external linter or type checker was available in the supplied environment. + +## Provenance and overlap + +Canonical base `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +[SOURCES.json](SOURCES.json) pins the task catalogue, selected record and the +two PR5564 source notes as historical provenance. Runtime inputs are package +local. [TASK.json](TASK.json) explicitly changes the card from selected-caller +assumption discharge to this algebraic side result. The current selected +source-binding orientation passed; it is not scientific evidence for this result. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227603) +followed live open PRs, recent account publications, handoff/active discussions, +main README searches and merged searches for composite chirps, Gauss sums, +rank and singular kernels. The cached card search covered 377 open PRs and +5,601 Discussion records with complete remote pagination at 21:06 UTC. Its +sparse local coverage was 254 of 8,136 HEAD notes, supplemented by distinctive +all-main README searches. Absence of a +search match is not a novelty certificate and excludes unpublished work and +unread arbitrary diffs. Nearby #5946 concerns the allowed second-input space +of unequal Fourier read layouts, not this quadratic convolution or repair. +Its result and the Gaussian adapter packages are not reverified here. + +## Open next questions + +Can an actual composite-axis consumer use K_b or the g-term repair at a +favorable complete cost? First name one literal kernel and its coefficient a, +prove the actual input/output contract, and charge the folds, phase tables, +recursive calls, normalization and owned restoration. A compatible producer, +native implementation and complete invoice are the blockers. The present +result reserves no continuation and establishes no profitable supplier. diff --git a/research/composite-chirp-phase-repair/SOURCES.json b/research/composite-chirp-phase-repair/SOURCES.json new file mode 100644 index 0000000000..1b772960c6 --- /dev/null +++ b/research/composite-chirp-phase-repair/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/native-coprime-grid/README.md", + "usage": "provenance", + "git_blob": "85a3c8d7a1e3e3b2a45451472707ce8281233c40", + "sha256": "c180783791bf1b43d9682d77f3811a6d564ee216c82b4e8bfc5920c7275da4c0" + }, + { + "path": "research/native-coprime-grid/PROOF.md", + "usage": "provenance", + "git_blob": "7e202209c9844e77fef9835fdf494cc04ad37ae2", + "sha256": "aa02a23e16c575968f381569a33b1126003ce57e144a05262c667d80881e6bee" + } + ], + "literature": [ + { + "url": "https://dlmf.nist.gov/20.11.i", + "use": "Classical Gauss-sum context only; the proof is self-contained." + } + ] +} diff --git a/research/composite-chirp-phase-repair/TASK.json b/research/composite-chirp-phase-repair/TASK.json new file mode 100644 index 0000000000..9b2c60b3cf --- /dev/null +++ b/research/composite-chirp-phase-repair/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Rank-optimal phased folding and the sharp number of linear-phase chirps needed to repair an odd composite cyclic quadratic convolution.", + "scope_change_reason": "A self-contained algebraic side result for the composite-axis numerical-interface question in PR5564. No selected assumption is discharged and no published Gaussian kernel is identified with this phase-only operator.", + "bottleneck_link": "Composite axes remove prime-selection setup, but their numerical caller remains missing. This result distinguishes nonsingular unit-coefficient chirps from rank-deficient nonunit chirps and prices repair by an exact term count, not a native cost.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved factorization and sharp repair count. Bound finite corroboration to the declared small axes; no whole-supplier replay.", + "outcome": "completed", + "evidence": "Written all-odd-n construction and lower bound; exact finite checks enumerate 5,456 factorizations, 3,344,528 phase entries, 1,225 basis vectors, 127 modular ranks, 16,255 cyclotomic Gram entries, 890 phase subsets, 8,128 inverse entries across 64 repair families, and 17 domain/semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual composite-axis consumer use this phase-only operator or its g-term repair with a favorable complete bill?", + "why_it_matters": "An exact algebraic component cannot improve the multiplication recurrence without a compatible producer and paid consumer.", + "first_step": "Name one literal kernel and its integer quadratic coefficient, establish the input/output contract, and charge all folds, phase tables, calls, restoration and normalization.", + "blocked_by": "No actual Gaussian resampling caller or native cost is supplied here." + } + ], + "source_question": { + "pr": 5564, + "author": "Dugongue", + "question": 1, + "scope": "One phase-only cyclic-convolution component, not the complete composite numerical caller." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227603" +} diff --git a/research/composite-chirp-phase-repair/VERIFY.json b/research/composite-chirp-phase-repair/VERIFY.json new file mode 100644 index 0000000000..f2f2759d82 --- /dev/null +++ b/research/composite-chirp-phase-repair/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact factorization, literal modular rank, cyclotomic Gram entries, exhaustive bounded phase subsets, inverse and semantic/domain controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with optimization; acceptance does not depend on assertions." + } + ] +} diff --git a/research/composite-chirp-phase-repair/chirp.py b/research/composite-chirp-phase-repair/chirp.py new file mode 100644 index 0000000000..f67fff14c6 --- /dev/null +++ b/research/composite-chirp-phase-repair/chirp.py @@ -0,0 +1,63 @@ +"""Bounded exact evaluations of the composite cyclic-chirp factorization. + +Produced by Nick Petalas. Apache-2.0. +The arithmetic here evaluates the formula in a supplied modular ring. Complex +rank and optimality are the written theorem, not consequences of this model. +""" + +from math import gcd + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parameters(n, a, b): + require(type(n) is int and 1 <= n <= 255 and n % 2 == 1, + "n must be odd and between 1 and 255") + require(type(a) is int and type(b) is int, + "coefficients must be integers") + require(a.bit_length() <= 256 and b.bit_length() <= 256, + "coefficients exceed the 256-bit reference limit") + a, b = a % n, b % n + g = gcd(a, n) + return a, b, g, n // g + + +def phase_table(n, modulus, root): + require(type(modulus) is int and 2 <= modulus <= 1_000_000, + "invalid modular-ring size") + require(type(root) is int and 0 < root < modulus, + "invalid root representative") + require(pow(root, n, modulus) == 1, "root must have order dividing n") + return tuple(pow(root, j, modulus) for j in range(n)) + + +def factorized(n, a, b, values, modulus, root): + """Return E_b C E_b^* x without modifying x; no scratch ABI is claimed.""" + a, b, g, m = parameters(n, a, b) + phases = phase_table(n, modulus, root) + require(type(values) in (tuple, list) and len(values) == n, + "input must have exactly n coordinates") + require(all(type(x) is int and 0 <= x < modulus for x in values), + "input coordinates must be modular-ring representatives") + folded = [0] * m + for r in range(m): + folded[r] = sum(phases[(-b * (r + h * m)) % n] * values[r + h * m] + for h in range(g)) % modulus + middle = [0] * m + for s in range(m): + middle[s] = sum(phases[(a * (s - r) ** 2) % n] * folded[r] + for r in range(m)) % modulus + return [phases[(b * j) % n] * middle[j % m] % modulus for j in range(n)] + + +def repair(n, a, values, modulus, root): + """Sum one chirp for every phase residue modulo gcd(a,n).""" + _, _, g, _ = parameters(n, a, 0) + result = [0] * n + for b in range(g): + contribution = factorized(n, a, b, values, modulus, root) + result = [(x + y) % modulus for x, y in zip(result, contribution)] + return result diff --git a/research/composite-chirp-phase-repair/oracle.py b/research/composite-chirp-phase-repair/oracle.py new file mode 100644 index 0000000000..d0a670cf3e --- /dev/null +++ b/research/composite-chirp-phase-repair/oracle.py @@ -0,0 +1,99 @@ +"""Literal matrices and integer-polynomial checks, independent of chirp.py. + +Produced by Nick Petalas. Apache-2.0. +""" + +from math import isqrt + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def prime(p): + return p >= 2 and all(p % d for d in range(2, 1 + isqrt(p))) + + +def field(n): + require(type(n) is int and 1 <= n <= 63, "oracle axis limit") + if n == 1: + return 3, 1 + for k in range(2, 1025): + p = k * n + 1 + if not prime(p): + continue + for root in range(2, p): + if pow(root, n, p) == 1 and all( + pow(root, d, p) != 1 for d in range(1, n) if n % d == 0): + return p, root + raise ValueError("bounded field search exhausted") + + +def matrix(n, a, b, p, root): + return [[pow(root, (a * (j - k) ** 2 + b * (j - k)) % n, p) + for k in range(n)] for j in range(n)] + + +def apply(rows, values, p): + return [sum(x * y for x, y in zip(row, values)) % p for row in rows] + + +def rank(rows, p): + a = [list(row) for row in rows] + height, width = len(a), len(a[0]) + pivot = 0 + for column in range(width): + found = next((r for r in range(pivot, height) if a[r][column] % p), None) + if found is None: + continue + a[pivot], a[found] = a[found], a[pivot] + inverse = pow(a[pivot][column], -1, p) + a[pivot] = [x * inverse % p for x in a[pivot]] + for r in range(pivot + 1, height): + multiplier = a[r][column] % p + a[r] = [(x - multiplier * y) % p for x, y in zip(a[r], a[pivot])] + pivot += 1 + if pivot == height: + break + return pivot + + +def polynomial_division(numerator, denominator): + work = list(numerator) + degree = len(denominator) - 1 + quotient = [0] * max(1, len(work) - degree) + for k in range(len(work) - 1, degree - 1, -1): + coefficient = work[k] + quotient[k - degree] = coefficient + for j in range(degree + 1): + work[k - degree + j] -= coefficient * denominator[j] + return quotient, work[:degree] + + +def cyclotomic(n): + """Construct Phi_n by exact division, with no symbolic-algebra dependency.""" + polynomials = {} + for k in range(1, n + 1): + if n % k: + continue + value = [-1] + [0] * (k - 1) + [1] + for d in range(1, k): + if k % d == 0: + value, remainder = polynomial_division(value, polynomials[d]) + require(not any(remainder), "nonexact cyclotomic division") + polynomials[k] = value + return polynomials[n] + + +def reduced(polynomial, phi): + _, remainder = polynomial_division(polynomial, phi) + return tuple(remainder) + + +def gram_entry(n, a, b, j, ell, phi): + polynomial = [0] * n + for k in range(n): + exponent = (a * ((j - k) ** 2 - (ell - k) ** 2) + b * (j - ell)) % n + polynomial[exponent] += 1 + return reduced(polynomial, phi) diff --git a/research/composite-chirp-phase-repair/verify.py b/research/composite-chirp-phase-repair/verify.py new file mode 100644 index 0000000000..bbc8bcaf08 --- /dev/null +++ b/research/composite-chirp-phase-repair/verify.py @@ -0,0 +1,164 @@ +"""Exact finite corroboration; the universal proof is PROOF.md. + +Produced by Nick Petalas. Apache-2.0. Normal execution writes no files. +""" + +from hashlib import sha256 +import json +from math import gcd +from pathlib import Path +import sys + +import chirp +import oracle + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def factorizations(): + cases = entries = vectors = ranks = 0 + for n in range(1, 32, 2): + p, root = oracle.field(n) + values = [(j * j + 3 * j + 7) % p for j in range(n)] + for a in range(n): + m = n // gcd(a, n) + for b in range(n): + rows = oracle.matrix(n, a, b, p, root) + got = chirp.factorized(n, a, b, values, p, root) + require(got == oracle.apply(rows, values, p), "dense factorization") + for j in range(n): + for k in range(n): + direct = a * (j - k) ** 2 + b * (j - k) + folded = b * j + a * (j % m - k % m) ** 2 - b * k + require((direct - folded) % n == 0, "phase factorization") + entries += 1 + if n <= 9: + for k in range(n): + unit = [int(j == k) for j in range(n)] + require(chirp.factorized(n, a, b, unit, p, root) + == [row[k] for row in rows], "basis factorization") + vectors += 1 + if n <= 15 and b in {0, 1}: + require(oracle.rank(rows, p) == m, "literal modular rank") + ranks += 1 + cases += 1 + return dict(cases=cases, phase_entries=entries, basis_vectors=vectors, + modular_ranks=ranks) + + +def gram_polynomials(): + entries = 0 + for n in range(1, 16, 2): + phi = oracle.cyclotomic(n) + for a in range(n): + m = n // gcd(a, n) + for b in sorted({0, 1 % n}): + for j in range(n): + for ell in range(n): + expected = [0] * n + if (j - ell) % m == 0: + expected[(b * (j - ell)) % n] = n + actual = oracle.gram_entry(n, a, b, j, ell, phi) + require(actual == oracle.reduced(expected, phi), + "complex cyclotomic Gram entry") + entries += 1 + return dict(odd_axes_through=15, entries=entries) + + +def summed(rows, mask, p): + n = len(rows[0]) + return [[sum(matrix[j][k] for b, matrix in enumerate(rows) if mask >> b & 1) % p + for k in range(n)] for j in range(n)] + + +def repairs(): + subsets = inverse_entries = families = 0 + for n in range(1, 16, 2): + p, root = oracle.field(n) + for a in range(n): + g, m = gcd(a, n), n // gcd(a, n) + rows = [oracle.matrix(n, a, b, p, root) for b in range(g)] + all_rows = summed(rows, (1 << g) - 1, p) + stars = [oracle.matrix(n, a, b, p, pow(root, -1, p)) for b in range(g)] + star = list(map(list, zip(*summed(stars, (1 << g) - 1, p)))) + for j in range(n): + for k in range(n): + entry = sum(star[j][r] * all_rows[r][k] for r in range(n)) % p + require(entry == (n * g * int(j == k)) % p, "repair inverse") + inverse_entries += 1 + if g <= 9: + for mask in range(1 << g): + require(oracle.rank(summed(rows, mask, p), p) == m * mask.bit_count(), + "phase-subset rank") + subsets += 1 + values = [(5 * j + 2) % p for j in range(n)] + require(chirp.repair(n, a, values, p, root) + == oracle.apply(all_rows, values, p), "repair program") + families += 1 + return dict(families=families, phase_subsets=subsets, inverse_entries=inverse_entries) + + +def controls(): + rejected = [] + arguments = [ + (0, 0, 0), (2, 0, 0), (257, 0, 0), (True, 0, 0), + (3, True, 0), (3, 1, "1"), (3, 1 << 257, 0), + ] + for args in arguments: + try: + chirp.parameters(*args) + except ValueError: + rejected.append("parameters:" + repr(args)) + else: + raise ValueError("invalid parameter accepted") + p, root = oracle.field(9) + for values, modulus, phase in [([], p, root), ([0] * 8 + [True], p, root), + ([0] * 8 + [p], p, root), ([0] * 9, 1, root), + ([0] * 9, p, p), ([0] * 9, p, 2)]: + try: + chirp.factorized(9, 3, 1, values, modulus, phase) + except ValueError: + rejected.append("invalid evaluation") + else: + raise ValueError("invalid evaluation accepted") + unit = [int(j == 1) for j in range(9)] + require(chirp.factorized(9, 3, 1, unit, p, root) + != chirp.factorized(9, 3, 0, unit, p, root), "omitted phase hidden") + rejected.append("omitted twist changes output") + duplicates = [oracle.matrix(9, 3, b, p, root) for b in (0, 3, 6)] + require(oracle.rank(summed(duplicates, 7, p), p) <= 3, "duplicate residue repair") + rejected.append("three duplicate residues do not repair") + require(oracle.rank(oracle.matrix(9, 3, 0, p, 1), p) == 1, "nonprimitive root") + rejected.append("nonprimitive root cannot certify complex rank") + require(oracle.rank(oracle.matrix(4, 1, 0, 5, 2), 5) == 2, "even-axis control") + rejected.append("even-axis full-rank extrapolation fails") + require(chirp.parameters(9, -6, -8) == chirp.parameters(9, 3, 1), "residue inputs") + return rejected + + +def source_hashes(): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "chirp.py", "oracle.py", "verify.py") + folder = Path(__file__).resolve().parent + result = {} + for name in names: + with (folder / name).open("rb") as source: + content = source.read(131073) + require(len(content) <= 131072, "package source size limit") + result[name] = sha256(content).hexdigest() + return result + + +def main(): + require(len(sys.argv) == 1, "no arguments accepted") + receipt = dict(status="PASS_COMPOSITE_CHIRP_PHASE_REPAIR", + factorizations=factorizations(), gram=gram_polynomials(), + repairs=repairs(), controls=controls(), sources=source_hashes()) + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()