Prove exact constant-weight phase COPY error (no new κ)

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 <P,Q> = 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
+
+    <V_A,V_B> = [((1-i)/2)^j ((1+i)/2)^j]^f = q^j,
+    <V_A,I> = 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.

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.

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