From aedf15cadfc10d566d7811936019a21207c99545 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:05:17 +0000 Subject: [PATCH] feat(research): prove exact constant-weight phase COPY error --- .../constant-weight-phase-copy-error/PROOF.md | 149 ++++++++++ .../README.md | 116 ++++++++ .../SOURCES.json | 36 +++ .../TASK.json | 81 +++++ .../VERIFY.json | 34 +++ .../verify.py | 276 ++++++++++++++++++ 6 files changed, 692 insertions(+) create mode 100644 research/constant-weight-phase-copy-error/PROOF.md create mode 100644 research/constant-weight-phase-copy-error/README.md create mode 100644 research/constant-weight-phase-copy-error/SOURCES.json create mode 100644 research/constant-weight-phase-copy-error/TASK.json create mode 100644 research/constant-weight-phase-copy-error/VERIFY.json create mode 100644 research/constant-weight-phase-copy-error/verify.py diff --git a/research/constant-weight-phase-copy-error/PROOF.md b/research/constant-weight-phase-copy-error/PROOF.md new file mode 100644 index 0000000000..3a1b32ccbb --- /dev/null +++ b/research/constant-weight-phase-copy-error/PROOF.md @@ -0,0 +1,149 @@ +# Exact COPY error from constant-weight phase histories + +This scoped proof was produced by Nick Petalas. New work is Apache-2.0. + +## Contract and theorem + +Let n and f be positive integers, and let 1 <= k <= n. Write S = diag(1,i). +For a k-element subset A of {1,...,n}, let U_A be the n-axis diagonal unitary +that applies S on the axes in A and I on the other axes. Let V_A = U_A tensor +... tensor U_A, with f factors. Its dimension is D = 2^(nf). Exterior scalar +coefficients are not raised to the f-th power. + +There are N = binom(n,k) available histories. The admitted accumulator word +is any finite sequence of operations + + (x,y) -> (x, y + c V_A x), c in C, |A|=k. + +Both x and the initial accumulator y are arbitrary independent inputs. The +source x must return unchanged. Repetition and order are unrestricted, but +source mixing, other history operators and other register operations are +outside this contract. Equal histories can be collected, so every such word +has endpoint (x, y + Mx), where M = sum_A c_A V_A. Conversely any coefficient +vector has that endpoint using at most N accumulator operations. + +Use the normalized response norm ||R||_HS^2 = tr(R* R)/D. Define + + q = 2^(-f), + L(n,k,f) = sum_{j=0}^{min(k,n-k)} binom(k,j) binom(n-k,j) q^j, + b = ((1-i)/2)^(kf). + +Then the exact minimum COPY error is + + E(n,k,f) = min_c ||I - sum_A c_A V_A||_HS^2 + = 1 - binom(n,k) q^k / L(n,k,f). + +It satisfies 0 < E(n,k,f) < 1. The unique coefficient vector attaining the +minimum is constant on the layer: + + c_A = b / L(n,k,f) for every A. + +Thus no admitted word realizes exact COPY. The statement allows arbitrary +complex coefficients, including coefficients depending on f. It is stronger +than a claim restricted to Gaussian-dyadic coefficients, but does not assert +that its minimizer is implementable in that smaller alphabet. + +## Phase-sensitive kernel + +Use the inner product = tr(P* Q)/D, conjugate-linear in P. +For two k-subsets A and B, put j = |A minus B| = |B minus A|. +On an axis in A minus B the normalized trace contribution is (1-i)/2; +on an axis in B minus A it is (1+i)/2. All other axes contribute one. +Consequently + + = [((1-i)/2)^j ((1+i)/2)^j]^f = q^j, + = b. + +The cancellation of the two phases depends on equal subset cardinalities. +Taking absolute trace values before deriving b would lose its phase and +produce the wrong attaining coefficient. + +For fixed A, exactly binom(k,j) binom(n-k,j) choices of B remove j axes from +A and add j axes from its complement. Every row of the Gram matrix G +therefore sums to L. This is a constant-weight subset intersection count. + +## Independence and the attained optimum + +The two operators I^(tensor f) and S^(tensor f) are linearly independent. +Their diagonal entries at the all-zero address are both one, while at an +address with exactly one set bit they are one and i. After a fixed permutation +of the tensor axes, the full 2^n family indexed by all subsets A is the tensor +product of n copies of this independent pair. It is therefore independent. +This elementary tensor-basis argument works at every positive f. + +In particular, the k-layer is independent, so G is positive definite. Its +normal equations for approximation of I are Gc = b 1. Since G1 = L1 and +L>0, their unique solution is c = (b/L)1. Its squared projection mass is + + c* G c = N |b|^2 / L = N q^k / L. + +The residual is orthogonal to every V_A. For every other coefficient vector d, + + ||I - sum_A d_A V_A||_HS^2 + = E(n,k,f) + (d-c)* G (d-c). + +This proves global optimality and uniqueness, over all complex coefficients. +The projection is nonzero since b is nonzero, so E<1. Since k>=1, I is the +empty-subset member of the full independent family and is not in the k-layer +span. Hence E>0. No finite enumeration is needed for these universal steps. + +For the one-phase layer, k=1, the formula simplifies to + + E(n,1,f) = (2^f - 1)/(2^f + n - 1). + +For example E(2,1,1)=1/3, E(4,2,1)=7/13, E(8,4,1)=251/321 and +E(8,4,2)=1851/1921. The first coefficient vector is c_A=(1-i)/3. + +## Complete independent columns and the physical boundary + +The complete two-register endpoint and desired COPY are + + B_M = [[I,0],[M,I]], B_COPY = [[I,0],[I,I]]. + +Their only differing block is M-I. Thus all source-return columns and all +columns of the initially arbitrary accumulator already have their required +values. The response norm in the theorem is normalized by D. The squared +Hilbert-Schmidt distance of the complete 2D-dimensional matrices, normalized +by 2D, is E/2 at the optimum. Their operator-norm squared distance is at least +E, since the maximum squared singular value of M-I bounds its average. + +One algebraic realization of a summand phases x by V_A, adds c_A x to y, +and applies V_A inverse to x. This explains source restoration explicitly. +The verifier executes this sandwich on every input basis column in its +finite domain. No state is assumed initially zero. There is no extra helper. + +This algebraic word does not supply native physical queries or their tariffs. +In particular, c_A can have an odd denominator. Coefficient preparation, +phase/inverse delivery, movement, ownership, precision, storage and the full +recursive invoice remain unpriced. A lower bound remains valid if the caller +restricts the coefficients, but attainment in such a restriction is unclaimed. +The theorem excludes only its fixed available-history span, not arbitrary +Clifford programs, networks with feedback or changes to the source contract. + +## Evidence and credit + +The universal claim is the written argument above. The standalone exact +verifier independently constructs literal diagonal tensor matrices for every +1<=n<=6, 1<=k<=n and 1<=f<=min(8,floor(10/n)). It solves the complex normal +equations using rational elimination and positive Schur pivots, checks the +literal squared residual, and executes both register input columns at every +address. It imports no predecessor implementation and uses no floating point. + +The generated stdout receipt reports actual counts and hashes of all package +files. It distinguishes the literal cases from 160 larger evaluations of the +formula, whose matrices are not enumerated. Its nine semantic controls cover +conjugation, exterior-coefficient exponentiation, exchange distance, the +diagonal Gram term, inclusion of the identity history, changing S to Z, +restricting coefficients to real values, erasing dirty y and failing to restore +x. Ten malformed or out-of-range evaluator inputs are rejected. The evaluator +is capped at n<=128 and f<=256; the written theorem has no such cap. + +Ali Romman's [PR #5727](https://github.com/CrocSwap/integer-mult-bounds/pull/5727) +poses the finite paid-history application and supplies its exact projection +contract. Its general contraction engine and theorem are cited, not rechecked. +This contribution supplies a new explicit history family, its closed optimum +and attaining coefficients. Constant-weight intersection counts, tensor-product +independence and Hilbert-space normal equations are classical ingredients. +The broader Clifford/native/controller lineage remains with the contributors +credited in #5727. No new general projection method or literature priority is +claimed. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/constant-weight-phase-copy-error/README.md b/research/constant-weight-phase-copy-error/README.md new file mode 100644 index 0000000000..63bbfa7f32 --- /dev/null +++ b/research/constant-weight-phase-copy-error/README.md @@ -0,0 +1,116 @@ +# Exact COPY error from constant-weight phase histories + +This contribution was produced by Nick Petalas. It proves the exact best COPY +approximation from one explicit family of Gaussian-dyadic Clifford histories. +The claim is a scoped written mathematical proof with exact finite corroboration. +There is no new kappa or selected-frontier change. + +Let S=diag(1,i), and let U_A apply S on exactly the k axes in A among n axes. +Available source-preserving operations add c_A U_A^(tensor f) x to an arbitrary +initial accumulator y and return x unchanged. For every n>=1, 1<=k<=n and +integer f>=1, define + + L = sum_{j=0}^{min(k,n-k)} binom(k,j) binom(n-k,j) 2^(-fj). + +The exact minimum normalized squared response error is + + min_c ||I - sum_{|A|=k} c_A U_A^(tensor f)||_HS^2 + = 1 - binom(n,k) 2^(-fk)/L > 0. + +Its unique attaining coefficients are c_A=((1-i)/2)^(kf)/L. This permits +arbitrary complex, width-dependent exterior coefficients. For k=1 the error +is `(2^f-1)/(2^f+n-1)`. For n=8,k=4 it is `251/321` at f=1 and `1851/1921` +at f=2. No exact COPY can be synthesized within this fixed history contract. + +[PROOF.md](PROOF.md) derives the phase-sensitive kernel, constant Gram row sum +and global optimum, then records every independent source and accumulator +column. The error normalization uses response dimension 2^(nf); for the full +two-register matrix normalized by twice that dimension the minimum is half +the displayed value. The source and dirty accumulator returns are exact. + +## Evidence and reproduction + +The standard-library verifier constructs literal tensor diagonals independently +of the formula, solves the exact normal equations, and executes a phase/ADD/ +inverse-phase word on both registers. Its complete small domain is +`1<=n<=6`, `1<=k<=n`, `1<=f<=min(8,floor(10/n))`. + +- 51 literal interfaces, 49,538 source diagonal entries and 1,653 Gram entries. +- 398 real/imaginary normal equations and 23,484 independent endpoint columns. +- 160 larger formula evaluations, nine semantic controls and ten input controls. + +The larger evaluations reach n=128 and f=256; their matrices are not enumerated. +The universal statement relies on the written proof. Semantic controls change +the trace conjugation, coefficient power, intersection exponent, diagonal term, +history alphabet, coefficient field, dirty-state handling and source restoration. +The verifier generates a stdout receipt bound to SHA256 of all six package files. +No receipt is handwritten and no output is written into the package. + +From the repository root, using CPython 3.12 and no third-party dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/constant-weight-phase-copy-error/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/constant-weight-phase-copy-error/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/constant-weight-phase-copy-error +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/constant-weight-phase-copy-error --check-source-history +``` + +The direct commands emit `PASS_CONSTANT_WEIGHT_PHASE_COPY_ERROR` in JSON. +The direct verifier also runs from a Git-free export using a local Python 3.12. +The committed-byte preflight requires a committed package and full Git history. +Hosted CI is separate from the local evidence. + +## Scope, sources and implementation limits + +This is a new explicit application of the finite-span follow-up in Ali Romman's +[PR #5727](https://github.com/CrocSwap/integer-mult-bounds/pull/5727), head +`8b74ecd0eea26d95b400e56435d35fbd261dc49b`. Its exact projection contract is +cited, not audited or replayed. No predecessor executable is imported or copied. +Normal equations, Hilbert-space projection, tensor-basis independence and subset +intersection counts are classical. The new contribution is the closed optimum +and attaining coefficients for this history family, with its complete endpoint. +Retain the broader Clifford/native/controller credit recorded by #5727. + +[SOURCES.json](SOURCES.json) pins the predecessor proof and question, the +revision-8 catalogue and selected record as historical provenance at canonical +main `de5ec2e7a6074068452f45b1a191b5c72832df4a`. There are no live scientific +inputs outside this package. [TASK.json](TASK.json) preserves the original +helper-inventory card and explicitly changes its scope to an algebraic side +result. The selected source-binding orientation passed; it was not a replay. +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216139) +states this same target. + +The coefficients can have odd denominators. Native realization, coefficient +preparation, physical source restoration, precision, movement, ownership, stock, +storage and the complete recursive invoice are unproved and unpriced. The result +is not a physical supplier or a complete multiplication theorem. Adding other +history weights, source feedback or an identity history changes the theorem's +premise. Independent human and formal proof-kernel review are unclaimed. + +The Python evaluator is bounded to n<=128,f<=256, and the literal enumeration +to n<=6,nf<=10. Loops have explicit finite bounds; the largest literal layer +has 20 histories and its largest diagonal has 1,024 entries. All functions +are below 60 lines, there is no recursion or dynamic code generation, and +checks use explicit exceptions that remain enabled with `-O`. Warning-strict +runs provide the available language diagnostics; no static type checker is +required here. + +Rule 3 deviation applies to `verify.py` for its entire standalone run. +Python/Fraction requires dynamic allocation. Enforced domains bound live +collections and integer sizes; each interface is processed and released before +the next. Literal domain and rejection controls verify the caps. Before widening +them, derive and check the new live collection and integer-size limits. Runtime +and library allocation internals are not independently inspected. + +## Open next questions + +- What changes when two positive history weights are available together? Start + with the phase-sensitive two-layer Gram blocks and their invariant normal + equations. No multi-layer optimum is supplied. This can distinguish a real + caller with a larger history alphabet from the fixed-layer obstruction. +- Can one attaining coefficient vector be implemented with a fully charged + Gaussian-dyadic caller? Start with one explicit n,k,f and price coefficient + approximation and restoration. Native delivery, precision, movement and the + complete recursive bill are blockers; the algebraic optimum alone admits none. + +New proof and verifier are Apache-2.0. Predecessor files and credit are unchanged. diff --git a/research/constant-weight-phase-copy-error/SOURCES.json b/research/constant-weight-phase-copy-error/SOURCES.json new file mode 100644 index 0000000000..aa4cabb41b --- /dev/null +++ b/research/constant-weight-phase-copy-error/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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/clifford-exact-contractions/README.md", + "usage": "provenance", + "git_blob": "b2284cdf98ab493c246a8b0fa8c84e8b3d0a8f09", + "sha256": "3a01996ff6da7402442842db70c45ea6aaceab1ae03c17dad1fcb2e11fee1f89" + }, + { + "path": "research/clifford-exact-contractions/PROOF.md", + "usage": "provenance", + "git_blob": "cb7e1bdf410942d3d681c6b8b48d3ff8c62d8c1a", + "sha256": "b3834a57ba82f4fe316669910693b6c2399f50af8e7a73722d61cddc00ec31aa" + } + ], + "predecessor": { + "pr": 5727, + "author": "Ali Romman", + "head": "8b74ecd0eea26d95b400e56435d35fbd261dc49b", + "use": "Question and finite-span projection contract only; no scientific replay or executable import." + } +} diff --git a/research/constant-weight-phase-copy-error/TASK.json b/research/constant-weight-phase-copy-error/TASK.json new file mode 100644 index 0000000000..c3152edba7 --- /dev/null +++ b/research/constant-weight-phase-copy-error/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the 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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact all-width COPY projection from the constant-weight phase-history layer, with a closed error formula and unique attaining coefficients.", + "scope_change_reason": "The helper-inventory card is narrowed to a new algebraic side result from PR5727, not a selected-supplier construction or audit.", + "bottleneck_link": "A sharp attainable response error prices the information missing from one explicit phase-history interface. It does not discharge physical delivery or the complete supplier bill.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified closed optimum; do not extend the history family or seek a kappa.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal argument; verify.py enumerates literal finite interfaces, solves independent normal equations and checks complete two-register columns.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact optimum when two different positive history weights are admitted together?", + "why_it_matters": "The fixed-layer obstruction does not cover a caller with a larger history alphabet.", + "first_step": "Derive the phase-sensitive two-layer Gram blocks and solve their invariant two-dimensional normal equations.", + "blocked_by": "No multi-layer result or physical coefficient implementation is supplied here." + }, + { + "question": "Can the attaining coefficients be realized with a fully charged Gaussian-dyadic caller?", + "why_it_matters": "An algebraic minimizer may have odd denominators and does not establish an admissible physical approximation.", + "first_step": "Choose one concrete n,k,f and price a legal coefficient approximation and its source restoration.", + "blocked_by": "Coefficient preparation, native delivery, precision, movement, ownership and complete recursive costs are unresolved." + } + ], + "claim_type": "Scoped written mathematical proof with exact finite corroboration." +} diff --git a/research/constant-weight-phase-copy-error/VERIFY.json b/research/constant-weight-phase-copy-error/VERIFY.json new file mode 100644 index 0000000000..cc5925c266 --- /dev/null +++ b/research/constant-weight-phase-copy-error/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Enumerate every literal diagonal in 51 interfaces, solve exact normal equations, execute full independent endpoint columns, check semantic and input controls; emit generated package hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete verifier with assertions disabled; all proof-relevant checks remain active." + } + ] +} diff --git a/research/constant-weight-phase-copy-error/verify.py b/research/constant-weight-phase-copy-error/verify.py new file mode 100644 index 0000000000..c2949e2fff --- /dev/null +++ b/research/constant-weight-phase-copy-error/verify.py @@ -0,0 +1,276 @@ +#!/usr/bin/env python3 +"""Exact constant-weight phase COPY projection. Apache-2.0. + +Produced by Nick Petalas. No predecessor executable is imported. +""" + +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations +import json +from math import comb +from pathlib import Path +import platform + + +ROOTS = ((1, 0), (0, 1), (-1, 0), (0, -1)) +MAX_AXES = 128 +MAX_WIDTH = 256 +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(left, right): + a, b = left + c, d = right + return a * c - b * d, a * d + b * c + + +def target_overlap(exponent): + """Return ((1-i)/2)^exponent without a loop in the exponent.""" + require(type(exponent) is int and 0 <= exponent <= MAX_AXES * MAX_WIDTH, + "unsupported overlap exponent") + half, odd = divmod(exponent, 2) + numerator = ROOTS[(-half) % 4] + if odd: + numerator = multiply(numerator, (1, -1)) + denominator = 1 << (half + odd) + return F(numerator[0], denominator), F(numerator[1], denominator) + + +def layer_solution(n, k, width): + require(all(type(v) is int for v in (n, k, width)), "integer parameters required") + require(1 <= n <= MAX_AXES and 1 <= k <= n, "unsupported layer") + require(1 <= width <= MAX_WIDTH, "unsupported width") + radius = min(k, n - k) + row_sum = sum((F(comb(k, j) * comb(n - k, j), 1 << (width * j)) + for j in range(radius + 1)), F(0)) + overlap = target_overlap(k * width) + coefficient = overlap[0] / row_sum, overlap[1] / row_sum + error = 1 - F(comb(n, k), 1 << (width * k)) / row_sum + require(row_sum > 0 and 0 < error < 1, "projection range invariant") + return coefficient, error, row_sum + + +def literal_diagonals(n, k, width, phase=1): + """Enumerate every entry of each literal tensor diagonal in the small domain.""" + require(1 <= n <= 6 and 0 <= k <= n and 1 <= width <= 8 and n * width <= 10, + "literal enumeration domain exceeded") + require(phase in (1, 2), "unsupported literal phase") + masks = [sum(1 << bit for bit in subset) for subset in combinations(range(n), k)] + diagonals = [] + for mask in masks: + base = [(phase * (mask & address).bit_count()) % 4 for address in range(1 << n)] + diagonal = [0] + for _ in range(width): + diagonal = [(left + right) % 4 for left in diagonal for right in base] + require(len(diagonal) == 1 << (n * width), "tensor dimension invariant") + diagonals.append(diagonal) + return masks, diagonals + + +def literal_average(exponents): + real = sum(ROOTS[value][0] for value in exponents) + imag = sum(ROOTS[value][1] for value in exponents) + return F(real, len(exponents)), F(imag, len(exponents)) + + +def literal_gram(diagonals): + size = len(diagonals) + dimension = len(diagonals[0]) + gram = [[F(0) for _ in range(size)] for _ in range(size)] + rhs = [] + for i, left in enumerate(diagonals): + rhs.append(literal_average([(-value) % 4 for value in left])) + for j, right in enumerate(diagonals): + real, imag = literal_average([(right[a] - left[a]) % 4 + for a in range(dimension)]) + require(imag == 0, "literal fixed-layer Gram must be real") + gram[i][j] = real + return gram, rhs + + +def solve_positive_gram(gram, rhs): + """Independent exact elimination of both real and imaginary normal equations.""" + size = len(gram) + rows = [list(gram[i]) + list(rhs[i]) for i in range(size)] + for column in range(size): + pivot = rows[column][column] + require(pivot > 0, "nonpositive exact Schur pivot") + for i in range(column + 1, size): + factor = rows[i][column] / pivot + for j in range(column, size + 2): + rows[i][j] -= factor * rows[column][j] + solution = [(F(0), F(0)) for _ in range(size)] + for i in range(size - 1, -1, -1): + parts = [] + for part in range(2): + remainder = sum((rows[i][j] * solution[j][part] + for j in range(i + 1, size)), F(0)) + parts.append((rows[i][size + part] - remainder) / rows[i][i]) + solution[i] = tuple(parts) + return solution + + +def literal_error(diagonals, coefficients): + dimension = len(diagonals[0]) + total = F(0) + for address in range(dimension): + real, imag = F(0), F(0) + for diagonal, coefficient in zip(diagonals, coefficients, strict=True): + a, b = multiply(coefficient, ROOTS[diagonal[address]]) + real += a + imag += b + total += (1 - real) ** 2 + imag ** 2 + return total / dimension + + +def verify_literal_cases(): + counts = {"interfaces": 0, "source_diagonal_entries": 0, + "gram_entries": 0, "normal_equations": 0, + "endpoint_basis_columns": 0} + for n in range(1, 7): + for width in range(1, min(8, 10 // n) + 1): + for k in range(1, n + 1): + masks, diagonals = literal_diagonals(n, k, width) + gram, rhs = literal_gram(diagonals) + solution = solve_positive_gram(gram, rhs) + coefficient, error, row_sum = layer_solution(n, k, width) + require(solution == [coefficient] * len(masks), "attaining coefficients differ") + require(literal_error(diagonals, solution) == error, "literal distance differs") + for i, left in enumerate(masks): + require(sum(gram[i], F(0)) == row_sum, "literal row sum differs") + for j, right in enumerate(masks): + swaps = (left ^ right).bit_count() // 2 + require(gram[i][j] == F(1, 1 << (width * swaps)), "intersection kernel differs") + for part in range(2): + value = sum((gram[i][j] * solution[j][part] + for j in range(len(masks))), F(0)) + require(value == rhs[i][part], "literal residual not orthogonal") + dimension = len(diagonals[0]) + counts["interfaces"] += 1 + counts["source_diagonal_entries"] += len(masks) * dimension + counts["gram_entries"] += len(masks) ** 2 + counts["normal_equations"] += 2 * len(masks) + counts["endpoint_basis_columns"] += verify_endpoints(diagonals, solution) + return counts + + +def run_at_address(diagonals, coefficients, address, source, accumulator, + restore=True, erase=False): + """Literal phase, accumulator ADD, inverse-phase execution at one address.""" + if erase: + accumulator = (0, 0) + for diagonal, coefficient in zip(diagonals, coefficients, strict=True): + phase = ROOTS[diagonal[address]] + source = multiply(phase, source) + term = multiply(coefficient, source) + accumulator = accumulator[0] + term[0], accumulator[1] + term[1] + if restore: + source = multiply((phase[0], -phase[1]), source) + return source, accumulator + + +def verify_endpoints(diagonals, coefficients): + """Check both input columns at every address, including the arbitrary dirty y column.""" + dimension = len(diagonals[0]) + for address in range(dimension): + response = (F(0), F(0)) + for diagonal, coefficient in zip(diagonals, coefficients, strict=True): + term = multiply(coefficient, ROOTS[diagonal[address]]) + response = response[0] + term[0], response[1] + term[1] + for source, accumulator in (((1, 0), (0, 0)), ((0, 0), (1, 0))): + returned_source, returned_accumulator = run_at_address( + diagonals, coefficients, address, source, accumulator) + expected = multiply(response, source) + require(returned_source == source, "source return changed") + require(returned_accumulator == (accumulator[0] + expected[0], + accumulator[1] + expected[1]), "dirty endpoint differs") + return 2 * dimension + + +def verify_large_formulas(): + count = 0 + for n in (8, 16, 32, 64, 128): + for k in (1, n // 2, n - 1, n): + for width in (1, 2, 3, 4, 8, 16, 64, 256): + coefficient, error, row_sum = layer_solution(n, k, width) + radius = min(k, n - k) + integer_sum = sum(comb(k, j) * comb(n - k, j) << (width * (radius - j)) + for j in range(radius + 1)) + require(row_sum == F(integer_sum, 1 << (width * radius)), "integer row sum differs") + magnitude = coefficient[0] ** 2 + coefficient[1] ** 2 + require(magnitude * row_sum * comb(n, k) == 1 - error, "projection mass differs") + if k == 1: + require(error == F((1 << width) - 1, (1 << width) + n - 1), + "one-phase closed form differs") + count += 1 + return count + + +def verify_controls(): + _, diagonals = literal_diagonals(2, 1, 2) + coefficient, error, _ = layer_solution(2, 1, 2) + wrong_phase = coefficient[0], -coefficient[1] + require(literal_error(diagonals, [wrong_phase] * 2) > error, "conjugation control") + squared = multiply(coefficient, coefficient) + require(literal_error(diagonals, [squared] * 2) > error, "external coefficient power control") + wrong_row = F(1) + F(1, 16) + b = target_overlap(2) + wrong = b[0] / wrong_row, b[1] / wrong_row + require(literal_error(diagonals, [wrong] * 2) > error, "exchange distance control") + wrong = b[0] / F(1, 4), b[1] / F(1, 4) + require(literal_error(diagonals, [wrong] * 2) > error, "diagonal term control") + _, identity = literal_diagonals(2, 0, 2) + require(literal_error(identity, [(F(1), F(0))]) == 0 < error, "identity-history boundary") + _, paulis = literal_diagonals(2, 1, 2, phase=2) + gram, rhs = literal_gram(paulis) + require(literal_error(paulis, solve_positive_gram(gram, rhs)) == 1, "phase alphabet boundary") + _, one = literal_diagonals(1, 1, 1) + require(literal_error(one, [(F(1, 2), F(0))]) == F(3, 4) + > layer_solution(1, 1, 1)[1], "real coefficient boundary") + clean_coefficient = [layer_solution(1, 1, 1)[0]] + normal = run_at_address(one, clean_coefficient, 1, (0, 0), (1, 0)) + erased = run_at_address(one, clean_coefficient, 1, (0, 0), (1, 0), erase=True) + require(normal != erased, "erasing the dirty accumulator must change its basis column") + unrestored = run_at_address(one, clean_coefficient, 1, (1, 0), (0, 0), restore=False) + require(unrestored[0] != (1, 0), "unreturned phase changes the source basis column") + return 9 + + +def verify_invalid_inputs(): + bad = ((0, 1, 1), (2, 0, 1), (2, 3, 1), (2, 1, 0), (-1, 1, 1), + (True, 1, 1), (2, 1.0, 1), (2, 1, "1"), (129, 1, 1), (2, 1, 257)) + for parameters in bad: + rejected = False + try: + layer_solution(*parameters) + except ValueError: + rejected = True + require(rejected, "invalid parameters were accepted") + return len(bad) + + +def main(): + results = {"literal": verify_literal_cases(), "large_formula_interfaces": verify_large_formulas(), + "semantic_controls": verify_controls(), "invalid_input_controls": verify_invalid_inputs()} + results["fixtures"] = {} + for n, k, width in ((2, 1, 1), (4, 2, 1), (8, 4, 1), (8, 4, 2)): + coefficient, error, row_sum = layer_solution(n, k, width) + results["fixtures"][f"{n},{k},{width}"] = { + "coefficient": [str(part) for part in coefficient], + "squared_error": str(error), "row_sum": str(row_sum)} + directory = Path(__file__).resolve().parent + hashes = {name: sha256((directory / name).read_bytes()).hexdigest() for name in PACKAGE_FILES} + print(json.dumps({"status": "PASS_CONSTANT_WEIGHT_PHASE_COPY_ERROR", "result": results, + "package_sha256": hashes, "python": platform.python_version()}, sort_keys=True)) + + +if __name__ == "__main__": + main()