Strengthen uniform Clifford tensor Gram bound from 1/9 to 1/3

research/clifford-residual-count-bound/PROOF.md

@@ -0,0 +1,211 @@
+# A uniform Clifford Gram bound from nonsingular residual forms
+
+kumagi, with substantial OpenAI Codex assistance. Apache-2.0.
+
+This sharpens the sufficient constant in Ali Romman's
+[pointwise-faithfulness proof](../clifford-pointwise-faithfulness/PROOF.md),
+PR #5526, Sections 3–5. The tensor-width threshold and operator alphabet
+are unchanged. This is a scoped algebraic result, not a multiplication
+algorithm or an improvement to the selected κ.
+
+## Statement
+
+Let n >= 1, D = 2^n, and choose one unitary representative U_g of each
+projective n-qubit Clifford class. For every integer f >= 4n+4, and arbitrary
+complex coefficients b_g chosen at that width,
+
+    α sum_g |b_g|²
+      <= D^(-f) ||sum_g b_g U_g^(tensor f)||_HS²
+      <= (2-α) sum_g |b_g|²,                         (1)
+
+where
+
+    α = 1491359 / 4161536 > 358367/1000000 > 1/3.
+
+Thus (1/3) I <= Gram_f <= (5/3) I is a convenient weaker statement,
+improving the predecessor's sufficient interval [1/9,17/9] at the same
+width. It applies to subsets and is invariant under representative phases.
+Neither α nor the width threshold is asserted to be spectrally optimal.
+
+More generally, for an integer s >= 0 and f >= 4n+4+2s, the absolute
+off-diagonal row sum is at most
+
+    T_s = sum_(k>=1) 2^(-k(k+1)/2-sk).               (2)
+
+Consequently [1-T_s,1+T_s] is a sufficient spectral interval.
+
+## 1. Residual forms, with a fixed coordinate convention
+
+Work over F_2. Let V have even dimension N = 2n and nondegenerate
+alternating form ω(x,y) = x^T J y. For S in Sp(V), put W = im(S-I) and
+k = dim W. The identity ker(S-I) = W-perp follows from
+
+    ω(x,(S-I)y) = ω((S^(-1)-I)x,y).
+
+Define B on W by
+
+    B((S-I)x,w) = ω(x,w).                            (3)
+
+It is well-defined by that kernel identity. If the left argument has zero
+pairing with all w, then x is in W-perp and (S-I)x = 0; hence B is
+nonsingular. Expanding S's preservation of ω gives
+
+    B(u,v) + B(v,u) = ω(u,v).                        (4)
+
+For example, with u=(S-I)x and v=(S-I)y, both sides of (4) reduce to
+ω(x,Sy)+ω(Sx,y). This also fixes the convention: interchanging the two
+arguments of B changes the reconstruction formula.
+
+Choose an ordered basis of W and let E be its N by k column matrix. Write
+B for the k by k matrix of the residual form in this basis. Then
+
+    E^T J E = B+B^T,                                 (5)
+    S = I + E B^(-T) E^T J.                          (6)
+
+Indeed (3) says B^T a = E^T J x for (S-I)x = E a.
+This proves uniqueness of S given (E,B).
+
+Conversely, any injective E and nonsingular B satisfying (5) give a
+symplectic S by (6), with displacement rank k. To check symplecticity,
+expand S^T J S: the extra middle factor is
+
+    B^(-T) + B^(-1) + B^(-1)(B+B^T)B^(-T) = 0.
+
+The rank follows because E is injective and E^T J is surjective. This
+converse is also checked in the finite enumeration, although only the
+forward direction and uniqueness are needed for the upper bound below.
+
+## 2. Count embeddings before forms
+
+Let c_(N,k) count S in Sp(V) with rank(S-I)=k. Each S has exactly
+|GL(k,2)| ordered bases for W, so the number of pairs (E,B) above is
+c_(N,k) |GL(k,2)|.
+
+Fix instead any nonsingular k by k matrix B. Construct the columns
+e_0,...,e_(k-1) of E in order. After i independent columns have been
+chosen, (5) imposes i linear equations on e_i:
+
+    ω(e_j,e_i) = B_(j,i)+B_(i,j),   0 <= j < i.
+
+The i linear functionals are independent by nondegeneracy of ω and
+independence of the previous columns. Thus there are exactly 2^(N-i)
+solutions before requiring e_i to lie outside their span, and at most
+that many after. Diagonal equations are automatic in characteristic two.
+Therefore, for every fixed B, the number of injective E is at most
+
+    product_(i=0..k-1) 2^(N-i) = 2^(Nk-k(k-1)/2).
+
+There are |GL(k,2)| possible nonsingular B. Dividing the resulting pair
+bound by the number of bases gives
+
+    c_(N,k) <= 2^(Nk-k(k-1)/2),   1 <= k <= N.        (7)
+
+The cancellation is the improvement: singular forms are never included,
+and the count is organized by B before E. In comparison, the predecessor
+first chooses W and bounds by all forms with its prescribed symmetrization.
+At k=1, (7) is slightly weaker than the exact 2^N-1 transvection count;
+the improvement comes from the other ranks. No formula for |GL(k,2)| is
+needed, and no independence between choices of E and B is assumed.
+
+## 3. From rank counts to the Gram envelope
+
+We retain the predecessor's signed-Pauli trace argument, restated here to
+make the multiplicity and normalization explicit. For a Clifford U with
+symplectic Pauli action S, let L=ker(S-I). Conjugation by U on the
+Hermitian Pauli basis has trace |tr U|². Its signs at the fixed labels
+form a character of L. Their sum is either zero or 2^dim L.
+
+All projective lifts of a fixed S differ by the 2^N Paulis. Their signs
+on L run through every character of L, with multiplicity 2^(N-dim L).
+Consequently, for rank(S-I)=k, exactly 2^k projective lifts have nonzero
+trace, with normalized trace modulus
+
+    |tr U|/D = 2^(-k/2).
+
+For k=0 only the identity projective class contributes; the other Paulis
+have trace zero. Relative products U_g^* U_h give the same trace-modulus
+distribution about every projective class. Therefore the exact absolute
+row sum of the full tensor Gram matrix is
+
+    R_(n,f) = sum_(k=1..N) 2^k c_(N,k) 2^(-kf/2).
+
+Using (7) at f >= 2N+4+2s gives, term by term,
+
+    2^k c_(N,k) 2^(-kf/2)
+        <= 2^(Nk+k-k(k-1)/2-k(N+2+s))
+         = 2^(-k(k+1)/2-sk).
+
+Extending this finite nonnegative sum to infinity proves (2). Larger
+widths, including odd widths, only decrease the absolute row sum.
+For a Hermitian matrix with diagonal one and row sum at most t, bounding
+each off-diagonal quadratic term by |b_g|²+|b_h|² gives the spectral
+interval [1-t,1+t]. This proves the claimed Gram inequalities.
+
+For an exact rational constant, keep k=1,...,5 in T_0. The first omitted
+term is 2^(-21); the ratio of each later term to its predecessor is at
+most 2^(-7). Hence
+
+    T_0 <= sum_(k=1..5) 2^(-k(k+1)/2)
+                + 2^(-21)/(1-2^(-7))
+         = 2670177/4161536 < 2/3.
+
+Subtracting from one gives α in (1). More generally the same cutoff gives
+an explicit rational upper bound on T_s, with first omitted term
+2^(-21-6s) and tail ratio at most 2^(-7-s). The verifier uses integer
+arithmetic and exact fractions for these bounds.
+
+## 4. Consequences and scope
+
+If a unitary Clifford target T is absent from a set of projective classes
+S, then at any f >= 4n+4,
+
+    D^(-f) ||T^(tensor f) - sum_(g in S) b_g U_g^(tensor f)||_HS²
+        >= α (1 + sum_g |b_g|²) >= α.
+
+Thus its operator norm approximation error is at least sqrt(α), in
+particular at least 1/sqrt(3). The implication uses
+||A||_HS <= sqrt(D^f) ||A||_op. This is a worst-case unit-input error;
+it is not a lower bound on every input's error.
+
+The predecessor's fixed-residual four-width theorem also inherits α.
+For its exact Gaussian-dyadic Clifford group, write each exact operator
+as i^j U_g and let M = sum_(g,j) |c_(g,j)|² after equal exact operators
+are combined. At residue r put β_(g,r)=sum_j c_(g,j)i^(jr). Parseval says
+(1/4) sum_(g,r)|β_(g,r)|²=M. Apply (1) separately at the four widths
+4n+4,...,4n+7 and average: at least one normalized squared residual norm
+is >= α M. Vanishing at all four widths is still equivalent to all
+coefficients being zero. The residual coefficients must be fixed across
+these tests; pointwise (1) itself permits width-dependent coefficients.
+
+Scalar-phase copies must be combined with the phase raised to f. The
+projective Gram bound does not hold for repeated exact-phase copies as
+separate columns. Four phase residues are specific to the predecessor's
+Gaussian-dyadic scalar group; this is not a four-test theorem for arbitrary
+unitary phases or nonunitary scalar multiples.
+
+We do not change the threshold 4n+4, determine sharp one-/two-axis spectra,
+improve the rectangular stabilizer-map theorem, or validate any new complete
+caller. In particular this is not a new paid-call count, matched QQ16 bill,
+physical routing bound, affordable supplier, or selected-frontier admission.
+Applying the stronger error constant to an actual caller still requires
+checking its full operator alphabet and retained state. No such new source
+application is claimed here.
+
+## 5. Evidence and attribution
+
+The written argument proves the all-n statement subject to mathematical
+review. The checker independently constructs signed Clifford actions from
+literal H, S and controlled-X conjugations, and constructs symplectic maps
+from every small residual subspace and nonsingular form. It compares the
+entire sets for n=1,2, not just their cardinalities. It also checks trace
+multiplicities, exact row sums, rational tails and invalid conventions.
+Finite enumeration corroborates the proof; it does not establish its
+universal quantifiers or constitute formal-kernel/human acceptance.
+
+The residual-form method is classical. Ali Romman's #5526 supplies the
+explicit residual/trace-lift framework and tensor Gram/four-width
+consequences reused above; its attribution to earlier stabilizer and
+finite-alphabet work remains in the pinned input. The contribution here
+is the nonsingular-form-first double count and the resulting improved
+uniform constants within this repository, not a literature-priority claim
+for residual forms, Clifford counts, Gershgorin bounds or Fourier inversion.

research/clifford-residual-count-bound/README.md

@@ -0,0 +1,142 @@
+# Stronger uniform Clifford tensor separation
+
+kumagi, with substantial OpenAI Codex assistance. Apache-2.0.
+
+For the same projective n-axis Clifford alphabet and the same sufficient
+width `f >= 4n+4`, this package improves the guaranteed tensor Gram interval
+from **[1/9,17/9] to [1/3,5/3]**. The proof actually gives the stronger
+lower constant `α = 1491359/4161536 > 0.358367` and upper constant `2-α`.
+The coefficients may be arbitrary complex numbers chosen at the tested width.
+This makes the existing algebraic separation guarantee more robust; it does
+not improve the multiplication exponent or supply a physical caller.
+
+The new step is a short double count: pair an ordered basis of the residual
+space with its nonsingular residual form, and count in the opposite order
+from the predecessor's loose estimate. For `1 <= k <= 2n`,
+
+```
+#{S in Sp(2n,2): rank(S-I)=k} <= 2^(2nk-k(k-1)/2).
+```
+
+With the existing `2^k` nonzero-trace Pauli lifts per such `S`, the absolute
+Gram row sum at `f >= 4n+4+2s` is at most
+`sum_{k>=1} 2^(-k(k+1)/2-sk)`. An exact geometric tail gives the constant
+above. See [PROOF.md](PROOF.md) for the all-dimension argument, including
+normalization, reconstruction transpose, phases and quantifiers.
+
+A missing projective target therefore has worst-case operator norm
+approximation error at least `sqrt(α)`, and in particular `1/sqrt(3)`,
+instead of the predecessor's `1/3`. For a fixed Gaussian-dyadic residual
+with squared coefficient norm `M`, one of the four widths `4n+4,...,4n+7`
+has normalized squared residual norm at least `α M`, improving `M/9`.
+These are direct algebraic corollaries, not a newly audited caller application.
+
+## Selection, sources and overlap
+
+Started from canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`,
+priority revision 7, after reading the root guidance and #1166 handoffs.
+The current picker returned track `recursive-interfaces`, seed
+`1f66e16685e4ef83d568f7fabb3db680`. This is an explicit scope change from
+`joint-query-controller`: an enabling separation lemma, not the card's
+complete matched QQ16 bill. The card's resolved first example,
+`scripts/research_selected_baseline.py`, passed binding checks only.
+The selected κ and all inherited assumptions remain unchanged.
+
+The direct predecessor is Ali Romman's [PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526),
+head `45f7de73b168721cdf7ec8c1769b1b594493716a`; its retained
+[proof](../clifford-pointwise-faithfulness/PROOF.md) is byte-pinned in
+[SOURCES.json](SOURCES.json). Its Section 3 supplies the signed trace-lift
+argument and residual forms; Sections 4–5 supply the Gram and four-width
+framework. We strengthen the count, preserving their attribution and that
+of their classical and repository predecessors. No predecessor executable
+is imported or rewritten.
+
+[Claim and canonical discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19189185).
+The initial 05:37–05:40 UTC search on 2026-10-26 paginated all 374 open PRs
+and 5,002 Discussion records, supplemented by Git HEAD searches of package
+README/TASK notes and relevant proofs. The helper's sparse local coverage
+was incomplete; the supplemental searches are not a full proof audit or
+novelty certificate. A pre-submission refresh at 05:53–05:54 UTC covered 376 open PRs and
+5,007 Discussion records; targeted full-cache checks found the predecessor
+and this claim, but no competing nonsingular-form count claim. Canonical
+main was unchanged. The sharp one-axis work in #5549/#5594 and sharp
+two-axis work in #5675 concern different claims. This package changes the
+uniform all-n sufficient constant at the existing width, not those exact
+finite spectra or thresholds. #5547 and the paid-return/application audits
+remain their authors' independent work.
+
+## Verification
+
+The package uses only Python's standard library. Run from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/clifford-residual-count-bound
+python3.12 -B scripts/check_research_commit.py --package research/clifford-residual-count-bound --check-source-history
+```
+
+[VERIFY.json](VERIFY.json) registers both ordinary and optimized (`-O`)
+execution. Both passed on macOS with CPython 3.12.14. Checks use explicit
+exceptions, not removable Python assertions.
+The standalone verifier also runs in an exported tree without Git, with
+its declared predecessor proof present at the repository-relative path:
+
+```sh
+python3.12 -B research/clifford-residual-count-bound/verify.py
+```
+
+Two constructions agree on the entire small symplectic sets:
+
+| n | Projective signed Clifford actions | Symplectic rank histogram, k=0,...,2n | Exact Gram row sum at f=4n+4 |
+|---|---:|---|---|
+| 1 | 24 | 1, 3, 2 | 13/32 |
+| 2 | 11,520 | 1, 15, 100, 300, 304 | 37739/65536 |
+
+The first construction closes signed Pauli permutations under H, S and
+controlled-X. Each generator's full signed table is independently checked
+against literal Gaussian-integer matrix conjugation (unnormalized H with
+its factor two retained); these small integers are exactly representable
+in Python complex arithmetic. The second enumerates every binary subspace
+and compatible nonsingular residual form, then reconstructs the symplectic
+map. No group-enumeration or linear-algebra library is used.
+
+The verifier also checks every fiber's `2^k` nonzero-trace lifts, exact row
+sums and the infinite-tail rational certificate. Five negative controls
+reject a singular form, the wrong reconstruction transpose, a lost Pauli
+sign, an omitted lift multiplicity and a width below this sufficient bound.
+A failed sufficient bound is not evidence of dependence at smaller widths.
+
+The finite checks corroborate the written proof; neither they nor the
+metadata/replay checks constitute independent mathematical acceptance.
+No full selected-frontier replay is needed or claimed for this separate
+algebraic package. Source hashes, commit availability and source-export
+checks authenticate the declared evidence, not the theorem's correctness.
+
+## Limits
+
+The Gram columns must represent distinct **projective** Clifford operators.
+Scalar copies are combined with their phase raised to the tested width.
+Four-width testing requires the predecessor's fixed residual and four-element
+Gaussian-dyadic scalar group. The theorem does not cover arbitrary nonlinear,
+rounded, cross-column or non-Clifford operations, or arbitrary nonunitary
+scalings. It does not sharpen the predecessor's rectangular stabilizer-map
+bound, establish a least tensor width, or give an optimal spectral constant.
+
+A complete caller still needs its exact alphabet, retained dirty state,
+ownership and physical costs audited. No paid-call count, matched caller
+budget, new algorithm, unconditional multiplication theorem or frontier
+admission follows from this constant improvement alone.
+
+## Open next questions
+
+- Can phase cancellation yield a stronger all-n spectral bound than the
+  absolute-row estimate? Start from the existing #5594/#5675 finite spectra
+  and seek a uniform representation argument, without repeating those censuses.
+- Does one exact complete caller satisfy the alphabet premise for the
+  stronger error guarantee? Pin its operations and retained state and consult
+  the existing application audits before substituting this constant.
+
+The corresponding dependencies and first steps are in [TASK.json](TASK.json).
+The count is presented as an improvement to the repository's retained proof,
+not a claim of priority in the mathematical literature. All derivation, code
+and writing received substantial OpenAI Codex assistance for kumagi; no
+independent human review or formal-kernel proof is claimed.

research/clifford-residual-count-bound/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/clifford-pointwise-faithfulness/PROOF.md",
+      "usage": "input",
+      "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c",
+      "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764"
+    }
+  ]
+}