Prove the sharp fifth-root threshold for tensor phase recovery

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], s<s_* exactly when s<5/2 and s^2-5s+5>0.
+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.

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.

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))"
+  }
+}

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"
+    }
+  ]
+}

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"
+  }
+}