From f0d87ad28e09055fd44e5a93437be5eeba284491 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:46:18 +0000 Subject: [PATCH] feat(research): prove sharp tensor phase stability threshold --- research/tensor-phase-stability/PROOF.md | 128 +++++++++ research/tensor-phase-stability/README.md | 109 ++++++++ research/tensor-phase-stability/RESULT.json | 26 ++ research/tensor-phase-stability/SOURCES.json | 18 ++ research/tensor-phase-stability/TASK.json | 107 +++++++ research/tensor-phase-stability/VERIFY.json | 32 +++ research/tensor-phase-stability/verify.py | 278 +++++++++++++++++++ 7 files changed, 698 insertions(+) create mode 100644 research/tensor-phase-stability/PROOF.md create mode 100644 research/tensor-phase-stability/README.md create mode 100644 research/tensor-phase-stability/RESULT.json create mode 100644 research/tensor-phase-stability/SOURCES.json create mode 100644 research/tensor-phase-stability/TASK.json create mode 100644 research/tensor-phase-stability/VERIFY.json create mode 100644 research/tensor-phase-stability/verify.py diff --git a/research/tensor-phase-stability/PROOF.md b/research/tensor-phase-stability/PROOF.md new file mode 100644 index 0000000000..c2e2285fce --- /dev/null +++ b/research/tensor-phase-stability/PROOF.md @@ -0,0 +1,128 @@ +# Sharp recovery from tensor-square and tensor-cube tests + +Let A and B be unitary operators on the same nonzero finite-dimensional +complex Hilbert space. All norms below are operator norms. Suppose + + ||A^(tensor 2) - B^(tensor 2)|| <= epsilon, + ||A^(tensor 3) - B^(tensor 3)|| <= epsilon, 0 <= epsilon <= 2. + +Write a = arcsin(epsilon/2) in [0,pi/2] and + + epsilon_* = 2 sin(pi/5) = sqrt((5-sqrt(5))/2). + +Then the best possible dimension-independent bound is + + ||A-B|| <= F(epsilon), + + F(epsilon) = 2 sin(a/3) if 0 <= epsilon < epsilon_*, + 2 sin(pi/3 + a/3) if epsilon_* <= epsilon <= 2. + +Every value of the envelope is attained by scalar unitaries, including in +any fixed positive dimension. The weak inequality belongs to the second +branch. At the threshold a scalar fifth-root phase attains + + F(epsilon_*) = 2 sin(2pi/5) = sqrt((5+sqrt(5))/2). + +The left limit is 2 sin(pi/15). Thus the sharp envelope has a jump. This +is a scoped analytical theorem, not a source-word or multiplication theorem. + +## Reduction to one phase + +Put U = B* A. Unitary invariance and tensor multiplicativity give + + ||A-B|| = ||U-I||, + ||A^(tensor j)-B^(tensor j)|| = ||U^(tensor j)-I||, j=2,3. + +For each eigenvalue z of U, the tensor power has eigenvalue z^j by taking +the same eigenvector in every factor. Consequently |z^2-1| and |z^3-1| +are at most epsilon. The spectral theorem gives +||U-I|| = max_z |z-1|. It suffices to solve the scalar problem. Conversely, +U=zI attains any scalar feasible value in every positive dimension, so +this reduction loses nothing in the dimension-independent optimum. + +## Exact feasible arcs + +Conjugation preserves all three distances. Write z=exp(i theta) with +0 <= theta <= pi. The width-two constraint is + + |z^2-1| = 2 sin(theta) <= 2 sin(a), + +so theta lies in [0,a] or [pi-a,pi]. The width-three constraint is + + |z^3-1| = 2 |sin(3theta/2)| <= 2 sin(a), + +so theta lies in + + [0,2a/3] union [2pi/3-2a/3, 2pi/3+2a/3]. + +These formulas include the endpoints a=0 and a=pi/2. No other interval +meets [0,pi]. The largest feasible point in the first width-two interval +is at most a. Its first width-three component ends at 2a/3. + +The second width-two interval meets the second width-three interval +exactly when + + pi-a <= 2pi/3+2a/3, equivalently a >= pi/5. + +The first width-two interval can meet the second width-three interval +only if a >= 2pi/5. It therefore cannot create another component below +the threshold pi/5. The second width-two interval cannot meet the first +width-three interval, since that would require a >= 3pi/5. + +For a < pi/5 the largest feasible theta is therefore 2a/3. It is +feasible because 2a/3 <= a. For a >= pi/5 the largest feasible theta is +2pi/3+2a/3. It is at most pi, belongs to [pi-a,pi], and exceeds every +point in [0,a]. Since |z-1|=2 sin(theta/2) increases on [0,pi], the two +claimed branches follow. Choosing the displayed largest theta proves +attainment. At a=pi/5 it is 4pi/5, giving a nontrivial fifth root of unity. + +## Exact algebraic certificates + +The squared threshold s_*=(5-sqrt(5))/2 is the smaller root of + + s^2 - 5s + 5 = 0. + +For rational s in [0,4], s0. +There is no rational equality case. The verifier handles equality +separately in Q(sqrt(5)), rather than rounding the threshold. + +Write T=F(epsilon)^2 and s=epsilon^2. The triple-angle identity yields + + T(3-T)^2=s, 0 <= T <= 1, on the low branch; + T(T-3)^2=s, 3 <= T <= 4, on the high branch. + +Each polynomial is strictly increasing on its stated interval, except +for an endpoint derivative equal to zero, which does not affect unique +root selection. Both range over [0,4]. Exact rational bisection therefore +encloses T without trigonometric evaluation. The Q(sqrt(5)) witness has +cos(theta)=-(1+sqrt(5))/4 and T=(5+sqrt(5))/2. Its square and cube defects +both have square s_*. Chebyshev's identity T5(cos(theta))=1 checks its +fifth-root phase algebraically. + +## Consequences and scope + +Exact agreement at widths two and three forces A=B and hence agreement +at every positive tensor width. Width two alone does not suffice, as +A=-B shows. These exact facts are elementary; the new application here +is the full sharp error envelope and its fifth-root threshold. + +Approximate agreement at two finite widths does not supply a uniform +small error over every width. For example, scalar phases approaching +one pass arbitrarily tight tests while some later tensor powers approach +phase minus one. A separately specified all-width error budget remains +necessary. No claim is made about every noisy chart being a tensor power +of one fixed unitary. Nonunitary, independently rounded and projective-only +comparisons are outside the hypotheses. + +The source of the question is unpaidmoon's PR #5837, head +764e7bd6d615d92019445bec92e2a473af021878, which gives a width-two sign +counterexample. DLamdata's PR #5894 separately reports that the selected +native checker already fixes absolute phase using its |0> image. This +package neither audits those claims nor asserts missing phase coverage. +It supplies a quantitative diagnostic for comparisons where the stated +two tensor operator-norm premises have actually been established. + +Classical spectral theory and elementary trigonometry supply the method. +No general literature priority is claimed. This proof and its verifier +were produced by Nick Petalas. Independent human and formal proof-kernel +review are unclaimed. Apache-2.0. diff --git a/research/tensor-phase-stability/README.md b/research/tensor-phase-stability/README.md new file mode 100644 index 0000000000..bc023de68d --- /dev/null +++ b/research/tensor-phase-stability/README.md @@ -0,0 +1,109 @@ +# A sharp fifth-root threshold for two tensor tests + +This scoped analytical proof gives the exact dimension-independent recovery +error for unitary charts whose tensor squares and cubes are both within +operator-norm error epsilon of a reference. It was produced by Nick Petalas. + +Set a=arcsin(epsilon/2) and epsilon_*=sqrt((5-sqrt(5))/2). For any +unitaries A,B of the same positive finite dimension, + + max(||A^(tensor 2)-B^(tensor 2)||, + ||A^(tensor 3)-B^(tensor 3)||) <= epsilon + +implies the sharp bound + + ||A-B|| <= 2 sin(a/3) for epsilon < epsilon_*, + 2 sin(pi/3 + a/3) for epsilon >= epsilon_*. + +Every value is attained by scalar phases. At equality epsilon=epsilon_*, +the phase exp(4pi i/5) gives error sqrt((5+sqrt(5))/2). The small-error +branch has left limit 2 sin(pi/15), so the sharp envelope jumps at this +threshold. [PROOF.md](PROOF.md) proves all dimensions and all epsilon in +[0,2]. The exact threshold and jump witness are checked in Q(sqrt(5)). + +This answers a quantitative version of the finite-width phase boundary +raised in unpaidmoon's [PR #5837](https://github.com/CrocSwap/integer-mult-bounds/pull/5837). +It is an original repository application of elementary spectral theory +and trigonometry, with no general literature-priority claim. It does not +audit the predecessor's scalar lift or selected MOVE coverage. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/tensor-phase-stability/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/tensor-phase-stability/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/tensor-phase-stability +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/tensor-phase-stability --check-source-history +``` + +The marker is `PASS_TENSOR_PHASE_STABILITY`. Default replay writes nothing. +`--output /new/path.json` generates a fresh receipt, refuses overwrites, +and binds all six proof, code and metadata files by SHA256. [RESULT.json](RESULT.json) +is generated by that command. Finite coverage is corroboration of the +written proof; it does not enumerate arbitrary complex unitary matrices. + +The verifier independently multiplies literal rational unit-circle phases +and their powers, compares them with polynomial root enclosures, constructs +near-attaining feasible phases at 33 tolerances, and checks dense two-by-two +unitary pairs through literal four-by-four and eight-by-eight tensors. +Exact defect Gram matrices supply their operator norms. Algebraic threshold, +wrong-branch, false-bracket, invalid-input and width-two-only controls check +the phase distinction. Counts and the enumeration hash are in RESULT.json. + +## Limits and relation to current work + +The hypotheses require one fixed pair of exact unitary charts, honest +operator norms, and absolute phase. They do not cover projective comparisons, +nonunitary maps or independently perturbed tensor factors. Approximate finite +tests alone do not bound every later tensor width by the same small error. + +DLamdata's open [PR #5894](https://github.com/CrocSwap/integer-mult-bounds/pull/5894) +reports existing absolute-phase coverage in the selected native checker. +That source-specific work and #5837's scalar-word proof are separate from +this quantitative theorem. No missing selected phase check is asserted here. +No native replay, source MOVE census, supplier admission, physical tariff, +new kappa, selected-frontier change or complete multiplication theorem is +claimed. All five framework assumptions retain their status. Independent +human and formal proof-kernel review are unclaimed. + +The originating card is `uniform-transfer-audit`, explicitly changed to +this side result. Its selected bindings-only orientation command passed. +[TASK.json](TASK.json) records the exact question source, frozen card, +scope change and [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216906). +[SOURCES.json](SOURCES.json) pins the catalogue and selected record as +historical provenance. No pending Git commit or predecessor program is +needed to replay the theorem. Unpaidmoon's exact question source is +764e7bd6d615d92019445bec92e2a473af021878; it is cited context, not a live input. + +## Implementation limits + +The fixed verifier uses no recursion, subprocess, network or dynamic code. +Rational phases use numerators -24..24 and denominators 1..24; there are +at most 1,177 phase fixtures before deduplication. Bisections take 88 or +96 steps, and reject declared precision outside 16..128. Matrix dimensions +never exceed eight. Every loop has a fixed finite fixture or collection +bound, and functions stay below 60 lines. Explicit guards remain enabled +under optimization. Warning-strict normal and optimized Python are the +interpreted-code diagnostics. CPython/Fraction dynamic allocation is a +Power of Ten deviation; fixed input and matrix bounds constrain live memory. +The receipt writer owns one exclusive-create file and closes it on every exit. + +## Open next questions + +1. Determine the sharp envelope when the width-two and width-three error + budgets differ. Start with the two scalar arc families and classify + their first contacts. Actual comparisons may have asymmetric budgets; + the full two-parameter branch classification is not supplied here. +2. Apply the theorem to one actual fixed unitary chart pair with separately + established tensor operator-norm bounds. Retain existing absolute-phase + coverage, name the resulting error budget and charge its implementation. + A source-specific application and physical error/tape contract are missing. + +The structured questions are in TASK.json. Stop here at the sharp envelope. +Classical spectral theory, tensor identities and trigonometry retain their +standard credit. Credit unpaidmoon for #5837's motivating phase example and +DLamdata for #5894's separate coverage work, and retain Ali Romman, +Pierre-Loic Doulcet / hexapode, Mark / Matarener and the selected native/caller +lineage for their context. New proof and verifier are Apache-2.0. diff --git a/research/tensor-phase-stability/RESULT.json b/research/tensor-phase-stability/RESULT.json new file mode 100644 index 0000000000..af0aa8dfbc --- /dev/null +++ b/research/tensor-phase-stability/RESULT.json @@ -0,0 +1,26 @@ +{ + "controls": 11, + "dense_unitary_pairs": 16, + "enumeration_sha256": "ff4cacdf6a2fc8fe9e7cfa6b6721ba3a8a2e241c8a6d0fb44515d058061cc964", + "files": { + "PROOF.md": "6e83e5806c27820f9bfaf7a1b33b0c312875cd3fba007023aa71efb86877b074", + "README.md": "0b08ceebe90d8c16de0a47c6b137c4cfc8f579146d98697636dbdbcded04ddc8", + "SOURCES.json": "31c143b260707699e659dc37a368cf16853f59d44dff816b66701c0c991fcf0f", + "TASK.json": "ee29a99f7c7432d36a8e5e72cc5223998bfa070502d3c7fde895c9a732567ec4", + "VERIFY.json": "bdd4725c318a6fda27435488887d3f5517e5dfff60fc841a77ad53911b63e8ad", + "verify.py": "43d2e7686775fd3126cb5406fc9f3ba09fd98219558fa8ec3036532011703086" + }, + "near_attainments": 33, + "rational_phases": 720, + "threshold": { + "epsilon_squared": [ + "5/2", + "-1/2" + ], + "error_squared": [ + "5/2", + "1/2" + ], + "field": "Q(sqrt(5))" + } +} diff --git a/research/tensor-phase-stability/SOURCES.json b/research/tensor-phase-stability/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/tensor-phase-stability/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/tensor-phase-stability/TASK.json b/research/tensor-phase-stability/TASK.json new file mode 100644 index 0000000000..a91bd7dbc4 --- /dev/null +++ b/research/tensor-phase-stability/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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": "Sharp dimension-independent operator-norm recovery of unitary A,B from tensor-square and tensor-cube defects, including the fifth-root phase threshold.", + "scope_change_reason": "The original card requests a selected caller-bound assumption discharge. This original side theorem instead quantifies the finite-width absolute-phase boundary raised in PR5837. It does not replay the predecessor or certify any selected MOVE.", + "bottleneck_link": "A diagnostic for native_all_columns chart comparisons: two exact tensor tests identify a fixed unitary, whereas approximate tests have a sharp phase-aliasing jump. Actual chart premises, source operators and every physical charge remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved sharp envelope, exact equality witness and bounded independent finite corroboration; do not extend to other width pairs.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal argument; verify.py generates the exact finite corroboration and hash-bound RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the sharp envelope for unequal width-two and width-three tolerances?", + "why_it_matters": "Actual chart checks may use different certified error budgets.", + "first_step": "Intersect the two scalar feasible-arc families with separate angles, then identify every first contact.", + "blocked_by": "A full two-parameter branch classification; no selected error budgets are supplied here." + }, + { + "question": "Which actual chart comparison needs this finite-width diagnostic?", + "why_it_matters": "The general theorem alone changes no selected assumption or physical cost.", + "first_step": "Name one fixed pair of unitary charts with independently established operator-norm tensor premises, retaining existing absolute-phase coverage.", + "blocked_by": "Source-specific application and complete physical error/tape contract." + } + ], + "question_source": { + "pr": 5837, + "head": "764e7bd6d615d92019445bec92e2a473af021878", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5837", + "role": "Question provenance only; no predecessor code, result, source census or finite numbers are replay inputs." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216906", + "refresh": { + "upstream_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "utc": "2026-10-27T12:38:00Z" + }, + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/tensor-phase-stability/VERIFY.json b/research/tensor-phase-stability/VERIFY.json new file mode 100644 index 0000000000..137f9ebc1d --- /dev/null +++ b/research/tensor-phase-stability/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 rational circle and dense unitary fixtures, near-attainment, algebraic fifth-root threshold, false-bracket and phase-aliasing controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact corroboration with optimized Python; all guards stay active." + } + ] +} diff --git a/research/tensor-phase-stability/verify.py b/research/tensor-phase-stability/verify.py new file mode 100644 index 0000000000..cc0f0e5ad3 --- /dev/null +++ b/research/tensor-phase-stability/verify.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration for the written tensor phase theorem.""" + +import argparse +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def cmul(z, w): + return (z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0]) + + +def conjugate(z): + return (z[0], -z[1]) + + +def chord2(z): + return (z[0] - 1) ** 2 + z[1] ** 2 + + +def phase(t, high=False): + denominator = 1 + t * t + x = (1 - t * t) / denominator + return (-x if high else x, 2 * t / denominator) + + +def scalar_data(z): + need(z[0] ** 2 + z[1] ** 2 == 1, "unit-circle input") + square = cmul(z, z) + cube = cmul(square, z) + return chord2(z), chord2(square), chord2(cube) + + +def low_branch(squared_tolerance): + # The smaller root of s^2-5s+5 is (5-sqrt(5))/2. + s = squared_tolerance + return s < F(5, 2) and s * s - 5 * s + 5 > 0 + + +def residual(t, low): + return t * (3 - t) ** 2 if low else t * (t - 3) ** 2 + + +def enclosure(squared_tolerance, bits=88): + need(isinstance(squared_tolerance, F), "exact rational tolerance required") + need(0 <= squared_tolerance <= 4, "squared tolerance outside [0,4]") + need(type(bits) is int and 16 <= bits <= 128, "bisection bound") + low = low_branch(squared_tolerance) + left, right = (F(0), F(1)) if low else (F(3), F(4)) + for _ in range(bits): + middle = (left + right) / 2 + if residual(middle, low) <= squared_tolerance: + left = middle + else: + right = middle + check_enclosure(squared_tolerance, low, left, right, bits) + return low, left, right + + +def check_enclosure(s, low, left, right, bits): + need(low is low_branch(s), "wrong phase branch") + need((0 <= left <= right <= 1) if low else (3 <= left <= right <= 4), + "wrong root domain") + need(right - left <= F(1, 2**bits), "root enclosure too wide") + need(residual(left, low) <= s <= residual(right, low), "false root bracket") + + +def near_attainment(s, low): + if s == 0: + return (F(1), F(0)) + if s == 4: + return (F(-1), F(0)) + left, right = F(0), F(1, 2) if low else F(1, 3) + for _ in range(96): + middle = (left + right) / 2 + _, _, defect3 = scalar_data(phase(middle, high=not low)) + if (defect3 <= s) is low: + left = middle + else: + right = middle + return phase(left if low else right, high=not low) + + +def rational_phases(): + values = {phase(F(a, b)) for a in range(-24, 25) for b in range(1, 25)} + values.add((F(-1), F(0))) + return sorted(values) + + +def circle_checks(): + rows = [] + for z in rational_phases(): + t, defect2, defect3 = scalar_data(z) + need(defect2 == t * (4 - t), "literal tensor-square polynomial") + need(defect3 == t * (3 - t) ** 2, "literal tensor-cube polynomial") + s = max(defect2, defect3) + low, left, right = enclosure(s) + need(t <= right, "phase violates the proposed envelope") + need((t <= 1) if low else (t <= 4), "phase branch separation") + rows.append([str(z[0]), str(z[1]), str(s), str(left), str(right)]) + return rows + + +def attainment_checks(): + rows = [] + for numerator in range(33): + epsilon = F(numerator, 16) + s = epsilon * epsilon + low, left, right = enclosure(s) + z = near_attainment(s, low) + t, defect2, defect3 = scalar_data(z) + need(max(defect2, defect3) <= s, "infeasible attaining approximation") + need(left - F(1, 2**75) <= t <= right, "attainment gap") + rows.append([str(epsilon), "low" if low else "high", str(t)]) + return rows + + +def qmul(a, b): + # Exact Q(sqrt(5)); pairs encode a0+a1*sqrt(5). + return (a[0] * b[0] + 5 * a[1] * b[1], + a[0] * b[1] + a[1] * b[0]) + + +def qadd(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def qscale(a, coefficient): + return (a[0] * coefficient, a[1] * coefficient) + + +def threshold_checks(): + one, zero = (F(1), F(0)), (F(0), F(0)) + x = (F(-1, 4), F(-1, 4)) # cos(4*pi/5) + x2 = qmul(x, x) + x3 = qmul(x2, x) + t = qadd(qscale(one, 2), qscale(x, -2)) + e2 = qadd(qscale(one, 4), qscale(x2, -4)) + e3 = qadd(qadd(qscale(one, 2), qscale(x3, -8)), qscale(x, 6)) + need(e2 == e3 == (F(5, 2), F(-1, 2)), "exact fifth-root threshold") + need(t == (F(5, 2), F(1, 2)), "exact jump witness") + polynomial = qadd(qadd(qmul(e2, e2), qscale(e2, -5)), qscale(one, 5)) + need(polynomial == zero, "threshold quadratic") + x5 = qmul(qmul(x3, x), x) + need(qadd(qadd(qscale(x5, 16), qscale(x3, -20)), qscale(x, 5)) == one, + "literal fifth-root phase") + difference = qadd(t, qscale(one, -3)) + need(qmul(t, qmul(difference, difference)) == e2, "large cubic endpoint") + return {"epsilon_squared": ["5/2", "-1/2"], + "error_squared": ["5/2", "1/2"], "field": "Q(sqrt(5))"} + + +def sum_complex(values): + result = (F(0), F(0)) + for value in values: + result = (result[0] + value[0], result[1] + value[1]) + return result + + +def matrix_product(a, b): + return [[sum_complex(cmul(x, y) for x, y in zip(row, col)) + for col in zip(*b)] for row in a] + + +def adjoint(a): + return [[conjugate(z) for z in col] for col in zip(*a)] + + +def tensor(a, b): + return [[cmul(a[i][j], b[k][ell]) + for j in range(len(a[0])) for ell in range(len(b[0]))] + for i in range(len(a)) for k in range(len(b))] + + +def tensor_power(a, width): + need(1 <= width <= 3 and len(a) == len(a[0]) == 2, "bounded tensor fixture") + result = [[(F(1), F(0))]] + for _ in range(width): + result = tensor(result, a) + return result + + +def matrix_checks(): + zero = (F(0), F(0)) + b = [[(F(3, 5), F(0)), (F(0), F(4, 5))], + [(F(0), F(4, 5)), (F(3, 5), F(0))]] + phases = [(F(1), F(0)), (F(-1), F(0)), phase(F(1, 4)), phase(F(3))] + cases = 0 + for z, w in product(phases, repeat=2): + diagonal = [[z, zero], [zero, w]] + a = matrix_product(b, diagonal) + defect = F(0) + for width in (2, 3): + aw, bw = tensor_power(a, width), tensor_power(b, width) + dw = tensor_power(diagonal, width) + need(matrix_product(adjoint(bw), aw) == dw, "dense unitary reduction") + size = len(dw) + difference = [[(aw[i][j][0] - bw[i][j][0], + aw[i][j][1] - bw[i][j][1]) + for j in range(size)] for i in range(size)] + gram = matrix_product(adjoint(difference), difference) + for i, row in enumerate(gram): + for j, entry in enumerate(row): + need(entry == ((chord2(dw[i][i]), F(0)) if i == j else zero), + "literal defect Gram matrix") + defect = max(defect, *(gram[i][i][0] for i in range(size))) + _, _, upper = enclosure(defect) + need(max(chord2(z), chord2(w)) <= upper, "matrix envelope") + cases += 1 + return cases + + +def rejection_checks(): + failures = 0 + for value, bits in [(F(-1), 88), (F(5), 88), (F(1), 15), + (F(1), 129), (1, 88)]: + try: + enclosure(value, bits) + except ValueError: + failures += 1 + else: + raise ValueError("invalid input accepted") + low, left, right = enclosure(F(1)) + for values, message in [((not low, left, right), "wrong phase branch"), + ((low, left + 1, right + 1), "wrong root domain"), + ((low, F(0), F(1)), "root enclosure too wide"), + ((low, F(0), F(1, 2**88)), "false root bracket")]: + try: + check_enclosure(F(1), *values, 88) + except ValueError as error: + need(str(error) == message, "wrong rejection guard exercised") + failures += 1 + else: + raise ValueError("forged certificate accepted") + t, square, cube = scalar_data((F(-1), F(0))) + need(t == 4 and square == 0 and cube == 4, "width-two-only phase control") + need(enclosure(F(9, 4))[0] is False, "large-error branch control") + return failures + 2 + + +def run_checks(): + circles = circle_checks() + attainments = attainment_checks() + threshold = threshold_checks() + matrix_cases = matrix_checks() + controls = rejection_checks() + encoded = json.dumps([circles, attainments], separators=(",", ":")).encode() + return {"rational_phases": len(circles), "near_attainments": len(attainments), + "dense_unitary_pairs": matrix_cases, "controls": controls, + "threshold": threshold, "enumeration_sha256": sha256(encoded).hexdigest()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a fresh hash-bound receipt") + args = parser.parse_args() + result = run_checks() + package = Path(__file__).resolve().parent + names = ["PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py"] + result["files"] = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + if args.output: + with args.output.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(json.loads((package / "RESULT.json").read_text()) == result, "receipt differs") + print("PASS_TENSOR_PHASE_STABILITY", json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()