From 6341bc34e9ca9b24e962ac12064fe56979984dd6 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 12:16:43 +0000 Subject: [PATCH] feat(research): prove sharp dyadic two-wire approximation floors --- .../dyadic-two-wire-approximation/PROOF.md | 141 ++++++++++++ .../dyadic-two-wire-approximation/README.md | 135 +++++++++++ .../SOURCES.json | 41 ++++ .../dyadic-two-wire-approximation/TASK.json | 98 ++++++++ .../dyadic-two-wire-approximation/VERIFY.json | 34 +++ .../dyadic-two-wire-approximation/verify.py | 212 ++++++++++++++++++ 6 files changed, 661 insertions(+) create mode 100644 research/dyadic-two-wire-approximation/PROOF.md create mode 100644 research/dyadic-two-wire-approximation/README.md create mode 100644 research/dyadic-two-wire-approximation/SOURCES.json create mode 100644 research/dyadic-two-wire-approximation/TASK.json create mode 100644 research/dyadic-two-wire-approximation/VERIFY.json create mode 100644 research/dyadic-two-wire-approximation/verify.py diff --git a/research/dyadic-two-wire-approximation/PROOF.md b/research/dyadic-two-wire-approximation/PROOF.md new file mode 100644 index 0000000000..cfb8b65626 --- /dev/null +++ b/research/dyadic-two-wire-approximation/PROOF.md @@ -0,0 +1,141 @@ +# Sharp approximation by exact Gaussian-dyadic two-wire gates + +This scoped proof and its application were produced by Nick Petalas. +New material is Apache-2.0. + +Put D = Z[i,1/2]. Norms below are Euclidean operator norms on complex +coordinate vectors. The target U is any real 2 by 2 orthogonal matrix; +in particular it can be a real rotation or a normalized real butterfly. +Write m = max over i,j of |U_ij|. + +## The approximation theorem + +For every such U, + + min { ||V-U||_op^2 : V* V = I_2, V in D^(2 by 2) } = 2(1-m). (1) + +A real signed permutation attains the minimum. Complex coefficients and +arbitrarily large dyadic denominators cannot improve it. Consequently the +worst minimum over real O(2) is 2-sqrt(2), attained by balanced butterflies. + +### Classical dyadic unit-vector lemma + +A unit vector in D^2, regarded as a real four-coordinate vector, is either +a signed coordinate vector or has all four coordinates equal to +/-1/2. + +Choose its least common denominator 2^k. Its integer numerators satisfy + + x_1^2 + x_2^2 + x_3^2 + x_4^2 = 4^k. + +If k>=1, the number of odd numerators is divisible by four, by reduction +modulo four. Minimality excludes zero odd numerators, so all four are odd. +For k>=2 their squares sum to 4 modulo eight, whereas 4^k is 0 modulo +eight, a contradiction. For k=1 the four odd squares sum to four, forcing +each numerator to be +/-1. For k=0 only a signed coordinate vector is +possible. This is the classical small-dimensional dyadic-unitary argument, +not a new group-classification claim. + +### Lower bound + +Let u=(a,c) be the first column of U, and v the first column of V. +Real two-dimensional orthogonality gives + + a^2+c^2=1, max(|a|,|c|)=m. + +If v is a signed coordinate vector in its four real components, then +Re(u* v) <= m. If its four real components are all +/-1/2, then + + Re(u* v) <= (|a|+|c|)/2 <= m. + +Both vectors have norm one. Thus + + ||V-U||_op^2 >= ||v-u||_2^2 = 2-2 Re(u* v) >= 2(1-m). + +This lower bound concerns the full complex operator norm, even though the +target is real. It does not discard imaginary leakage into either output. + +### Attainment + +Let delta=det U, which is +/-1. Choose p to be the signed coordinate +vector with u dot p = m. Set + + J = [[0,-1],[1,0]], P = [p, delta Jp]. + +Then P is a real signed permutation and has the same determinant as U. +The matrix P^T U is a real rotation with both diagonal entries equal to m. +Therefore + + (P-U)* (P-U) = 2I - P^T U - U^T P = 2(1-m) I. + +This proves (1), including the endpoints m=1 and m=1/sqrt(2). The latter +endpoint gives the worst-case statement because m>=1/sqrt(2). + +## Arbitrarily many exactly restored dirty helpers do not help + +Allow any finite h and any finite circuit of exactly unitary linear gates +over D on two active coordinates and h additional complex coordinates. +Every helper input is arbitrary and independent. Require the completed +linear map W to return every helper exactly to its initial value for every +input. There is no measurement, postselection, data-dependent control or +unobserved output outside this declared space. + +Closure under multiplication gives W in U_(2+h)(D). Exact helper return +gives the block form + + W = [[A,B],[0,I_h]]. + +The bottom-right block of W*W is B*B+I_h, so unitarity forces B*B=0 +and hence B=0. The top-left block gives A*A=I_2. Thus W=A direct-sum I_h +with A in U_2(D), and (1) applies without change. Its attaining P can simply +leave all helpers untouched. This is an all-size block-matrix argument; +the finite one-helper checks only corroborate it. + +## Consequence for the rational-unitary FFT interface + +Jose Manuel's PR4205 uses exactly unitary rational coefficient gates with +stored adjoint inverses. PROOF.md sections 2 and 3 specify rational phases +and butterflies [[a,bw],[b,-aw]], with a^2+b^2=|w|^2=1. Its dyadic data +rounding is a separate operation. Taking w=1 yields the real family covered +by (1). This is a self-posed denominator-elimination question about that +boundary, not a defect in the predecessor's rational construction. + +For the explicit rational member of this algebraic family + + U = [[3/5,4/5],[4/5,-3/5]], + +the optimum squared operator error is exactly 2/5. For any unit-scale real +butterfly with m<=4/5, the same model cannot meet error below sqrt(2/5), +regardless of the precision parameter, circuit length or count of exactly +restored helpers. At input radius R the corresponding worst-case absolute +error is R sqrt(2(1-m)). The operator-norm extremizer proves that statement; +it is not an assertion about every input. + +Rational butterflies approaching a balanced Hadamard gate have optimum +squared error approaching 2-sqrt(2), rather than zero. Hence exact +Gaussian-dyadic unitarity at this restored two-coordinate boundary cannot +replace the rational coefficient approximation as its requested error +tends to zero. + +Removing exact unitarity changes the question. For example the dyadic real +rotation-shaped matrix (5I+6J)/8 has norm square 61/64, while its squared +operator distance to (3I+4J)/5 is only 1/320. Nonunitary dyadic lifting or +rounded gates need their own stability and restoration budget. Joint gates +with additional non-restored active coordinates, global cancellation among +changed gates, Gaussian natives on large address spaces and other endpoint +contracts are outside this obstruction. No physical cost, recursive saving, +supplier admission or selected framework assumption is proved here. + +## Classical credit and proof status + +Alexis De Vos, Raphael Van Laer and Steven Vandenbrande, +[The Group of Dyadic Unitary Matrices, 2012, section 5](https://backoffice.biblio.ugent.be/download/2069554/2069555), +already describe the finite group U_2(D) of order 96. This package supplies +an elementary proof of the unit-vector fact needed for the approximation +formula. The new contribution claimed here is (1), its sharp gate-interface +consequence and the exact-restored-helper extension, in this repository's +arithmetic setting. No worldwide literature priority is claimed. + +The all-real and arbitrary-helper quantifiers rest on this written proof. +The exact finite checker is corroboration and checks of the formula's +implementation. Independent human and formal proof-kernel review are +unclaimed. diff --git a/research/dyadic-two-wire-approximation/README.md b/research/dyadic-two-wire-approximation/README.md new file mode 100644 index 0000000000..70921dc84e --- /dev/null +++ b/research/dyadic-two-wire-approximation/README.md @@ -0,0 +1,135 @@ +# Sharp exact-dyadic approximation floor for two-wire butterflies + +This contribution was produced by Nick Petalas. New material is Apache-2.0. +Claim type: scoped written mathematical proof with exact finite corroboration. +No new kappa or supplier admission is claimed. + +For every real 2 by 2 orthogonal matrix U, let m=max |U_ij|. The exact best +Gaussian-dyadic unitary approximation satisfies + + min_{V in U_2(Z[i,1/2])} ||V-U||_op^2 = 2(1-m). + +A real signed permutation attains it. Any finite number of arbitrary dirty +helpers, returned exactly for every input, leaves this minimum unchanged. +The worst floor over real orthogonal targets is 2-sqrt(2), at a balanced +butterfly. The rational butterfly [[3/5,4/5],[4/5,-3/5]] already has sharp +squared error 2/5, regardless of requested precision or circuit length. +[PROOF.md](PROOF.md) supplies the all-real and arbitrary-helper arguments. + +## The changed arithmetic interface + +Jose Manuel's [PR4205](https://github.com/CrocSwap/integer-mult-bounds/pull/4205), +retained head `78c72e563173f3822fcb4efed9ceeccf05630258`, supplies exactly +unitary rational FFT coefficient gates and stored adjoint inverses. Its +real-phase butterfly family is the motivation for a self-posed question: +can exact Gaussian-dyadic unitaries remove those rational denominators at +the same restored two-coordinate boundary? The formula excludes an +arbitrarily accurate replacement of a nontrivial real butterfly in that +model. The predecessor's rational construction is a cited premise, not an +audit target, and is unchanged. + +This is an arithmetic-interface side result under a changed +`joint-query-controller` card. It does not give a complete supplier invoice +or resolve the selected compiler/precision obligations. Nonunitary lifting, +rounded arithmetic and larger active joint boundaries remain possible. +The nonunitary dyadic matrix (5I+6J)/8, J=[[0,-1],[1,0]], is at squared +distance only 1/320 from (3I+4J)/5, but has norm square 61/64. Thus exact +unitarity is a substantive premise. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dyadic-two-wire-approximation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/dyadic-two-wire-approximation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-two-wire-approximation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-two-wire-approximation --check-source-history +``` + +Any CPython 3.12 path can replace the absolute interpreter path. Direct +replay prints `PASS_DYADIC_TWO_WIRE_APPROXIMATION` in a JSON receipt whose +hashes bind all six package files and the complete mathematical transcript. +It writes no files and imports no predecessor implementation. Both +warning-strict normal and optimized commands are registered in VERIFY.json. + +The checker independently joins all possible first and second columns and +compares that join with the perpendicular-column construction. It then +compares every resulting unitary with every declared rational rotation and +reflection using exact integer Hermitian principal minors. There are no +floating-point eigenvalues. The target family uses p=-12..12, q=1..12 in +the rational circle parametrization, with repetitions removed, plus the +missing limiting point. The resulting 368 targets give 35,328 exact +target/unitary comparisons. The emitted receipt also reports the control +counts and a hash of the full sorted transcript. + +One-helper controls exhaust the 96 unitary active blocks paired with each +of 24 nonzero possible unit-vector leakage columns. Every such leakage +fails exact unitarity, while each direct-sum identity helper passes. Six +other rejection controls cover a changed sharp threshold in both +directions, an empty candidate list, a nonpositive denominator, a +rectangular matrix and a nonunitary imaginary perturbation. The closer +nonunitary dyadic control verifies the importance of the hypothesis. + +## Scope and credit + +The finite group of 96 two-dimensional Gaussian-dyadic unitaries is +classical. Credit Alexis De Vos, Raphael Van Laer and Steven Vandenbrande, +[The Group of Dyadic Unitary Matrices, 2012, section 5](https://backoffice.biblio.ugent.be/download/2069554/2069555). +The new claim is the sharp distance formula and its restored-helper +interface consequence, with no worldwide literature-priority claim. + +Credit Jose Manuel / jmbarrancoml for PR4205's rational-unitary child; +Vlado Vojdanovski for the retained FFT and Toeplitz schedules; Chafik +Boukhalfa for rational unit-phase construction; Mason Hale for the retained +interval arithmetic; Jeremy Kothe / IdeaOuter and Cinna Davis for the +credited Gaussian/caller lineage. Predecessor files and credit are unchanged. +MatShep's PR5549 studies tensor faithfulness of the same 96-element group; +this package does not repeat its tensor-rank result or scientific replay. + +The scientific base is canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected +PR6030. SOURCES.json pins the motivating source documents as provenance. +No source scientific checker is run. Live open/account PRs, active +Discussions, local reservations and main/merged searches for the object, +general dyadic-unitary form and formula preceded the +[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373396). +The overlap helper was also run; its coverage and freshness are recorded +in the PR body. Sparse notes and bounded searches do not establish absence +of unpublished overlap. The selected result and all five framework assumptions remain. + +This excludes only a linear, exactly unitary, Gaussian-dyadic replacement +at a restored two-active-coordinate boundary. It excludes no global FFT +approximation, large native operator, nonunitary lifting method or changed +helper-return contract. Exact coefficient unitarity and rounded data +restoration are separate claims. Physical coefficient delivery, tapes, +precision, stock, compilation and complete multiplication remain unproved. +Selected cold replay, Lean, Docker, independent human and formal +proof-kernel review are unrun or unclaimed. + +## Open next questions + +Can a nonunitary dyadic lifting replacement of one rational butterfly meet +its full composed error/restoration budget with a cheaper complete +coefficient-delivery bill? Start with the pinned PR4205 butterfly, an exact +dyadic shear factorization, explicit rounding sites and inverse, and bound +its intermediate norms. Stability, fixed-grid restoration and a favorable +physical invoice are missing. This result does not reserve that follow-up. +The structured question is in TASK.json. + +## Implementation bounds + +The fixed checker uses no recursion, external process, network access, +dynamic import or mutable global state. The target generator has at most +602 outputs; each has exactly 96 candidates. Matrix dimensions are at most +three. Integer target denominators are at most 288. The transcript has at +most 602 records. Package hashing reads six files, each capped at 1 MB. +Every function is shorter than 60 lines and executable contracts remain +enabled under optimized Python. + +Power of Ten rule 3 has a managed-runtime deviation: Python integers, +tuples, sets and JSON allocate during execution inside the fixed finite +bounds above. Interpreter/library allocation is not statically controlled +or measured. Rule 9's rejection-test helper dispatches only to the two +named local check functions; its finite targets and call sites are explicit. +Warning-strict normal/optimized replay is the Python diagnostic check. diff --git a/research/dyadic-two-wire-approximation/SOURCES.json b/research/dyadic-two-wire-approximation/SOURCES.json new file mode 100644 index 0000000000..bf9ada994b --- /dev/null +++ b/research/dyadic-two-wire-approximation/SOURCES.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/rational-unitary-fft/README.md", + "usage": "provenance", + "git_blob": "33000ee73067f27e87a04953ed0ba3e356d96bc6", + "sha256": "b334df2d512f971626aa69a2b94dab4e51acee19bc0f9f6ee42ea709636b8d9f" + }, + { + "path": "research/rational-unitary-fft/PROOF.md", + "usage": "provenance", + "git_blob": "99a55596f67ae3b94ef02ebb159b313f33bf22af", + "sha256": "50e31e33e1275a133d10e87208ceb50dddce67d0678d2a89de9f7ba28d8380d9" + } + ], + "external_reference": { + "url": "https://backoffice.biblio.ugent.be/download/2069554/2069555", + "title": "The Group of Dyadic Unitary Matrices", + "authors": [ + "Alexis De Vos", + "Raphael Van Laer", + "Steven Vandenbrande" + ], + "year": 2012, + "usage": "Classical credit only; no fetched bytes or external theorem are required by the self-contained proof/checker." + } +} diff --git a/research/dyadic-two-wire-approximation/TASK.json b/research/dyadic-two-wire-approximation/TASK.json new file mode 100644 index 0000000000..d76f9efe66 --- /dev/null +++ b/research/dyadic-two-wire-approximation/TASK.json @@ -0,0 +1,98 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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": "Determine the exact operator-norm distance from every real two-coordinate orthogonal gate to U_2(Z[i,1/2]); prove the unchanged floor with any number of exactly restored arbitrary dirty helpers.", + "scope_change_reason": "This is a self-posed denominator-elimination obstruction for the rational-unitary FFT child of PR4205, rather than a completed query-demand supplier or an audit of its rational theorem.", + "bottleneck_link": "A dyadic exact-unitary replacement would simplify coefficient arithmetic and adjoint restoration at this recursive boundary. The sharp positive error floor excludes that option at two active coordinates, even with exactly restored helpers; changing exact unitarity or the active boundary is necessary.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved approximation floor, exact finite corroboration and focused PR; put further synthesis questions in Open next questions.", + "outcome": "negative-result", + "evidence": "PROOF.md gives the all-real approximation theorem and arbitrary-helper block proof; verify.py independently joins possible columns and checks exact Hermitian principal minors for rational fixtures.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a nonunitary dyadic lifting replacement of one rational butterfly meet its full composed error and restoration budget with a cheaper coefficient-delivery bill?", + "why_it_matters": "The theorem eliminates the exact-unitary two-wire route, but the explicit closer nonunitary dyadic control changes that premise.", + "first_step": "Take the pinned PR4205 butterfly and state its exact dyadic shear factorization, data rounding sites, inverse, intermediate norm bounds and complete coefficient/access costs.", + "blocked_by": "No stability, fixed-grid restoration or favorable complete physical invoice is supplied." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373396", + "claim_type": "scoped written mathematical proof with exact finite corroboration", + "scientific_base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "freshness": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_at_utc": "2026-11-03T12:14:54.892072+00:00", + "priority_revision": 8, + "selected_pr": 6030 + } +} diff --git a/research/dyadic-two-wire-approximation/VERIFY.json b/research/dyadic-two-wire-approximation/VERIFY.json new file mode 100644 index 0000000000..73c7724ef4 --- /dev/null +++ b/research/dyadic-two-wire-approximation/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": "Exact finite sharp approximation and restored-helper controls; generated hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact checks with Python assertions disabled." + } + ] +} diff --git a/research/dyadic-two-wire-approximation/verify.py b/research/dyadic-two-wire-approximation/verify.py new file mode 100644 index 0000000000..847a8fb433 --- /dev/null +++ b/research/dyadic-two-wire-approximation/verify.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the sharp real two-wire dyadic approximation floor.""" + +import hashlib +import itertools +import json +import math +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def conjugate(z): + return z[0], -z[1] + + +def multiply(z, w): + return z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0] + + +def inner(v, w): + require(len(v) == len(w) <= 3, "inner-product dimension") + terms = [multiply(conjugate(z), t) for z, t in zip(v, w)] + return sum(z[0] for z in terms), sum(z[1] for z in terms) + + +def columns(matrix): + return tuple(zip(*matrix)) + + +def unitary_numerator(matrix): + """All matrices here have common denominator two.""" + size = len(matrix) + require(1 <= size <= 3, "matrix dimension") + require(all(len(row) == size for row in matrix), "square matrix") + cols = columns(matrix) + return all(inner(cols[i], cols[j]) == (4 * (i == j), 0) + for i in range(size) for j in range(size)) + + +def first_columns(): + axes = [] + for index in range(4): + for sign in (-2, 2): + vector = [0] * 4 + vector[index] = sign + axes.append(tuple(vector)) + vectors = axes + list(itertools.product((-1, 1), repeat=4)) + return tuple(((v[0], v[1]), (v[2], v[3])) for v in vectors) + + +def dyadic_group(): + vectors = first_columns() + require(len(set(vectors)) == 24, "24 possible first columns") + matrices = set() + for v in vectors: + z = conjugate(v[1]) + perpendicular = ((-z[0], -z[1]), conjugate(v[0])) + for phase in ((1, 0), (0, 1), (-1, 0), (0, -1)): + w = tuple(multiply(phase, z) for z in perpendicular) + matrices.add(((v[0], w[0]), (v[1], w[1]))) + blind = {((v[0], w[0]), (v[1], w[1])) + for v in vectors for w in vectors if inner(v, w) == (0, 0)} + require(matrices == blind and len(matrices) == 96, "complete column join") + require(all(unitary_numerator(m) for m in matrices), "group unitarity") + return tuple(sorted(matrices)) + + +def real_targets(): + targets = set() + for p in range(-12, 13): + for q in range(1, 13): + a, b, d = q * q - p * p, 2 * p * q, p * p + q * q + common = math.gcd(math.gcd(a, b), d) + targets.add((a // common, b // common, d // common)) + targets.add((-1, 0, 1)) + result = [] + for a, b, d in sorted(targets): + require(a * a + b * b == d * d and d <= 288, "circle parametrization") + result.append((((a, -b), (b, a)), d)) + result.append((((a, b), (b, -a)), d)) + return tuple(result) + + +def error_gram(target, denominator, candidate): + """Return the Hermitian error Gram times 4*denominator**2.""" + delta = tuple(tuple((denominator * candidate[i][j][0] - 2 * target[i][j], + denominator * candidate[i][j][1]) for j in range(2)) + for i in range(2)) + left, right = columns(delta) + aa, bb = inner(left, left), inner(right, right) + require(aa[1] == bb[1] == 0, "real Gram diagonal") + return aa[0], bb[0], inner(left, right) + + +def spectral_relations(gram, threshold): + """Use exact two-by-two principal minors, without numerical eigenvalues.""" + aa, bb, off = gram + x, y = threshold - aa, threshold - bb + determinant = x * y - off[0] ** 2 - off[1] ** 2 + strictly_below = x > 0 and determinant > 0 + at_most = x >= 0 and y >= 0 and determinant >= 0 + return strictly_below, at_most + + +def check_target(target, denominator, group, threshold=None): + require(denominator > 0, "positive target denominator") + maximum = max(abs(x) for row in target for x in row) + expected = 8 * denominator * (denominator - maximum) + threshold = expected if threshold is None else threshold + attainments = 0 + real_attainments = 0 + for candidate in group: + gram = error_gram(target, denominator, candidate) + below, at_most = spectral_relations(gram, threshold) + require(not below, "candidate improves the stated minimum") + if at_most: + attainments += 1 + if all(z[1] == 0 for row in candidate for z in row): + require(gram == (threshold, threshold, (0, 0)), "scalar error Gram") + real_attainments += 1 + require(attainments > 0 and real_attainments > 0, "sharp real attainer") + divisor = math.gcd(expected, 4 * denominator * denominator) + return [expected // divisor, 4 * denominator * denominator // divisor, + attainments, real_attainments] + + +def restored_helper_controls(group): + """Enumerate nonzero leakage with an exactly unchanged independent helper.""" + count = 0 + for matrix in group: + for coupling in first_columns(): + padded = ((matrix[0][0], matrix[0][1], coupling[0]), + (matrix[1][0], matrix[1][1], coupling[1]), + ((0, 0), (0, 0), (2, 0))) + require(not unitary_numerator(padded), "uncharged helper leakage") + count += 1 + padded = ((matrix[0][0], matrix[0][1], (0, 0)), + (matrix[1][0], matrix[1][1], (0, 0)), + ((0, 0), (0, 0), (2, 0))) + require(unitary_numerator(padded), "restored-helper positive control") + return count + + +def expect_failure(function, *args): + try: + function(*args) + except ValueError: + return + raise ValueError("mutation was not rejected") + + +def controls(group): + target = ((3, -4), (4, 3)) + baseline = check_target(target, 5, group) + require(baseline[:2] == [2, 5], "3/5,4/5 sharp example") + expect_failure(check_target, target, 5, group, 41) + expect_failure(check_target, target, 5, group, 39) + expect_failure(check_target, target, 5, ()) + expect_failure(check_target, target, 0, group) + expect_failure(unitary_numerator, (((2, 0),), ((0, 0),))) + damaged = (((2, 0), (0, 1)), ((0, 0), (2, 0))) + require(not unitary_numerator(damaged), "nonunitary imaginary mutation") + # (5I+6J)/8 is dyadic and far closer, but its norm square is 61/64. + require(5 * 5 + 6 * 6 == 61 != 64, "nonunitary dyadic escape") + require((5 * 5 - 3 * 8) ** 2 + (6 * 5 - 4 * 8) ** 2 == 5, + "dyadic escape squared error is 5/1600=1/320") + require(5 * 5 + 6 * 6 != 8 * 8 and 1 * 5 < 2 * 320, + "escape beats 2/5 only outside exact unitarity") + return {"rejected_mutations": 6, "nonunitary_escape_squared_error": "1/320", + "rational_unitary_escape_squared_error": "0"} + + +def package_hashes(): + directory = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result = {} + for name in names: + path = directory / name + require(path.stat().st_size <= 1_000_000, "bounded package input") + result[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return result + + +def main(): + require(len(sys.argv) == 1, "this fixed-domain checker accepts no arguments") + group = dyadic_group() + transcript = [] + for target, denominator in real_targets(): + transcript.append([target, denominator, check_target(target, denominator, group)]) + payload = json.dumps(transcript, separators=(",", ":"), sort_keys=True).encode() + result = {"status": "PASS_DYADIC_TWO_WIRE_APPROXIMATION", + "claim_type": "scoped written proof with exact finite corroboration", + "dyadic_unit_vectors": 24, "dyadic_unitaries": len(group), + "rational_orthogonal_targets": len(transcript), + "operator_comparisons": len(transcript) * len(group), + "restored_helper_leakage_rejections": restored_helper_controls(group), + "restored_helper_positive_controls": len(group), + "controls": controls(group), + "transcript_sha256": hashlib.sha256(payload).hexdigest(), + "package_sha256": package_hashes()} + canonical = json.dumps(result, separators=(",", ":"), sort_keys=True).encode() + result["receipt_sha256"] = hashlib.sha256(canonical).hexdigest() + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()