Prove odd-axis Clifford tensor Gram lower bound above one half

research/clifford-seven-rotation-gap/PROOF.md

@@ -0,0 +1,203 @@
+# A seven-rotation improvement to the odd-axis Clifford Gram bound
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written mathematical proof, with exact finite corroboration.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Statement and cited inputs
+
+Let n be odd, n>=3, D=2^n, and choose one unitary representative U_g
+of each projective n-axis Gaussian-dyadic Clifford operator. The scalar
+kernel of the exact group is {1,i,-1,-i}. For every integer f>=4n+4,
+define the normalized tensor Gram matrix
+
+    G_f[g,h] = (tr(U_g* U_h)/D)^f.
+
+Then
+
+    G_f >= gamma I,
+    gamma = 14601049/29130752 > 1/2.                    (1)
+
+Equivalently, arbitrary complex coefficients, including coefficients chosen
+separately at each width, satisfy
+
+    D^(-f) ||sum_g b_g U_g^(tensor f)||_HS^2
+        >= gamma sum_g |b_g|^2.                       (2)
+
+Principal submatrices inherit the bound. Changing representative phases
+conjugates G_f by a diagonal unitary and preserves it.
+
+We cite, without re-enumerating or auditing, the following inputs from Ali
+Romman's #5526 and Hiroki KUMAZAKI's #5694. Put N=2n and let c_(N,k)
+count symplectic Pauli actions S with rank(S-I)=k.
+
+* c_(N,k) <= 2^(Nk-k(k-1)/2).
+* Exactly 2^k projective lifts of each such S have nonzero trace. Their
+  normalized trace modulus is 2^(-k/2).
+* Every rank-one S is the transvection associated with a unique nonzero
+  binary Pauli label v. Its two nonzero-trace lifts are C_P and C_P^(-1),
+  where P is a Hermitian Pauli with label v and
+
+      C_P = ((1+i)I + (1-i)P)/2.
+
+The last item also follows directly from C_P's Pauli conjugation action:
+C_P^2=P, its symplectic action is that transvection, and the cited lift
+count is two. The two projective lifts are distinct because P is nonscalar.
+
+The cited count and trace formula bound the absolute row contribution at
+each displacement rank k, when f>=2N+4, by
+
+    2^k c_(N,k) 2^(-kf/2) <= 2^(-k(k+1)/2).          (3)
+
+Set T=sum_(k>=1) 2^(-k(k+1)/2). The exact rational upper tail certificate
+in #5694 gives
+
+    T <= T_plus = 2670177/4161536.
+
+Javier Vera's #5714 proves that T is the limiting absolute row sum, and
+explicitly leaves spectral improvement open. We change the treatment of
+rank one, rather than strengthen that asymptotically sharp count.
+
+## 1. Seven commuting quarter turns
+
+Take three independent commuting Hermitian Paulis P_1,P_2,P_3. For each
+nonzero a in F_2^3 put P_a=product_j P_j^(a_j) and C_a=C_(P_a).
+The seven C_a commute and have fourth power I. Moreover,
+
+    product_(a!=0) C_a = I.                            (4)
+
+To see this, simultaneously diagonalize the three commuting involutions.
+Write their joint eigenvalues as (-1)^(x_j). On this eigenspace C_a has
+eigenvalue i^(a dot x). If x=0 all seven exponents vanish. If x!=0,
+exactly four a have a dot x=1, so the product is i^4=1.
+
+This relation holds as an exact operator identity, before taking a
+projective quotient. For a general isotropic label space, choosing the
+signed products P_a is essential. Arbitrary independent sign choices
+need not give (4).
+
+Let R be any unitary representation of the projective Clifford group.
+The seven R(C_a) still commute, have fourth power I, and have product I.
+On a simultaneous eigenspace their eigenvalues lambda_a are fourth roots
+with product one. Therefore
+
+    sum_(a!=0) (lambda_a + conjugate(lambda_a)) >= -10. (5)
+
+Here is an elementary proof. Each summand belongs to {-2,0,2}. A sum
+below -10 is either -14, requiring seven eigenvalues -1, or -12,
+requiring six eigenvalues -1 and one eigenvalue i or -i. Their products
+are respectively -1 and i or -i, contradicting product one. Six -1
+and one +1 give -10 and product one, so this root constraint alone
+cannot give a larger constant. Thus, in operator order,
+
+    sum_(a!=0) (R(C_a)+R(C_a)*) >= -10 I.              (6)
+
+## 2. Average over Clifford conjugation
+
+For each of the m=2^(2n)-1 nonzero unsigned Pauli labels v choose a
+Hermitian representative P_v and define
+
+    A = sum_(v!=0) (R(C_(P_v))+R(C_(P_v))*).
+
+The pair of summands is independent of the sign choice. Indeed
+C_(-P)=i C_P^(-1), so their projective classes are inverses. Clifford
+conjugation acts transitively on the nonzero labels, and consequently
+averaging a conjugate of the left side of (6) gives (7/m) A. Every
+conjugate obeys the same operator inequality. Hence
+
+    A >= -(10/7) m I.                                 (7)
+
+This is the new step. The absolute row bound for this adjacency operator
+would only give A>=-2m I. Its lower coefficient improves by the factor 5/7.
+We assert a sufficient bound, not the exact full-group minimum eigenvalue.
+
+## 3. Apply the bound to the tensor Gram matrix
+
+First take f_0=4n+4. Since n is odd, f_0 is divisible by eight. Its
+Gram kernel is well-defined on the projective group because the exact
+scalar kernel has order four. Choose the right-regular convention
+(R(a)b)(g)=b(ga). Then the kernel convolution has entries
+G_(f_0)[g,h]=(tr(U_g*U_h)/D)^(f_0). Products of representatives can differ
+by a scalar fourth root, whose f_0-th power is one.
+
+For C_P and its inverse,
+
+    tr(C_P)/D = (1+i)/2,
+    (tr(C_P)/D)^(f_0) = 2^(-f_0/2) = w > 0.
+
+Thus the complete displacement-rank-one contribution is exactly w A in
+the right-regular representation. All other nonidentity nonzero-trace
+contributions have displacement rank at least two. Write
+
+    G_(f_0) = I + w A + H.
+
+The remaining matrix H is Hermitian. Equation (3) bounds its absolute
+off-diagonal row sum by T-1/2, so H>=-(T-1/2)I. This uses the elementary
+inequality 2|b_g b_h|<=|b_g|^2+|b_h|^2 in its quadratic form.
+Meanwhile (7) and m<2^(2n) give
+
+    w A >= -(10/7) m 2^(-2n-2) I >= -(5/14) I.
+
+Combining the two bounds yields
+
+    G_(f_0) >= (1-5/14-(T-1/2)) I
+             = (1-T+1/7) I
+             >= (1-T_plus+1/7) I
+             = (14601049/29130752) I.                 (8)
+
+The improvement over #5694's rational lower constant is exactly 1/7
+in this odd-axis domain. The new constant exceeds 1/2 by
+35673/29130752. No sharpness for the complete Gram matrix is claimed.
+
+For later widths, G_(f+1)=G_f entrywise-multiplied by G_1. The matrix G_1
+is positive semidefinite with diagonal one. If G_f>=gamma I, its entrywise
+product with G_1 preserves the same lower bound. Explicitly, write
+G_1=sum_j v_j v_j*. Then
+
+    (G_f-gamma I) entrywise-multiplied by G_1
+      = sum_j diag(v_j)(G_f-gamma I)diag(v_j)* >= 0.
+
+This proves (1) at every f>=f_0. It also explains why the projective
+convolution argument only needs to be used at the initial width.
+
+## 4. Scope, finite evidence and remaining questions
+
+The written argument supplies all odd n>=3 and all f>=4n+4. The finite
+verifier checks its new local ingredients, not those universal quantifiers
+or the cited predecessor counts. In F_2^6 it enumerates every isotropic
+three-space and checks uniform point incidence. For a chosen signed basis
+in each space it applies all seven literal 8-by-8 quarter turns to every
+input basis column, using Gaussian integers and an explicit denominator.
+An abstract fourth-root enumeration and a separate 512-character diagonal
+subgroup calculation both give minimum -10. Wrong words and the excluded
+phase residue supply rejection controls. The emitted receipt binds the
+package and cited input bytes by SHA-256.
+
+For the diagonal calculation the three coordinate turns generate the
+three order-four single-axis phases. The turn on e_i+e_j, divided by
+the two coordinate turns, gives the order-two controlled phase on i,j.
+These six independent parameters give Z4^3 x Z2^3. The turn on v has
+coordinates (v_i; v_i v_j), since binary parity modulo four is
+sum_i v_i x_i - 2 sum_(i<j) v_i v_j x_i x_j. Thus the 512 parameter
+choices in the verifier enumerate all characters of this subgroup.
+
+The even-n initial width is congruent to four modulo eight. Its rank-one
+coefficient is negative, so the lower bound (7) is the wrong side of the
+inequality there. The verifier's trivial-character control detects this
+sign distinction. We make no improved claim for that starting width.
+
+No one-/two-axis spectrum is recomputed. No complete caller, native cost,
+owned-state restoration, finite compiler, precision/tape, stock, outer
+bound, new kappa or complete multiplication theorem is supplied.
+
+## Credit
+
+Javier Vera / #5714 supplies the explicit spectral-strengthening question
+and the sharp limitation of the absolute row method. Hiroki KUMAZAKI /
+#5694 supplies the rank count and rational tail certificate. Ali Romman /
+#5526 supplies the trace-lift and projective Gram framework. Their classical
+symplectic, Pauli and Clifford provenance and retained native/kernel credit
+remain with the pinned source packages. The seven-rotation operator bound,
+conjugation average and resulting odd-axis constant are the new step here.
+No global literature-priority claim is made.

research/clifford-seven-rotation-gap/README.md

@@ -0,0 +1,134 @@
+# Odd-axis Clifford tensor Gram lower bound above one half
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For every odd n>=3 and every tensor width f>=4n+4, the normalized Gram
+matrix of the full projective Gaussian-dyadic Clifford alphabet satisfies
+
+    Gram_f >= (14601049/29130752) I > (1/2) I.
+
+This improves Hiroki KUMAZAKI's #5694 sufficient lower constant
+1491359/4161536 by exactly 1/7 in this domain. The new constant is
+approximately 0.501224582187. It answers the odd-axis part of the
+phase-aware spectral-strengthening question in Javier Vera's #5714.
+The exact spectrum and optimal constant remain open.
+
+Claim type: scoped written mathematical proof with exact finite
+corroboration. Independent human and formal proof-kernel review are
+unclaimed. No new kappa or physical supplier follows.
+
+## New step and dependencies
+
+Seven quarter turns associated with the nonzero vectors of a
+three-dimensional isotropic Pauli space commute and multiply to I.
+Their regular-action adjacency sum is at least -10 I. Averaging over
+Clifford conjugation improves the rank-one displacement contribution
+by the factor 5/7. At the odd-axis initial width its coefficient is
+positive. The cited higher-rank count bounds the remaining terms.
+Entrywise Gram multiplication propagates the result to later widths.
+
+[PROOF.md](PROOF.md) gives the argument, normalization and phase restriction.
+We cite Ali Romman's #5526 trace framework and #5694's count and rational
+tail certificate. No predecessor executable, group census or caller replay
+is run. [SOURCES.json](SOURCES.json) pins their proof bytes and #5714's
+explicit open question on canonical main
+de5ec2e7a6074068452f45b1a191b5c72832df4a.
+
+This is a side result with scope changed from the `scalar-to-moment`
+suggestion. The revision-8 selected baseline binding example passed;
+the result concerns quantitative native-alphabet separation rather than
+a complete paid/target invoice. The selected record is unchanged.
+
+## Reproduction and evidence
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clifford-seven-rotation-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clifford-seven-rotation-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clifford-seven-rotation-gap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clifford-seven-rotation-gap --check-source-history
+```
+
+Another CPython 3.12 path can replace the absolute interpreter path.
+[VERIFY.json](VERIFY.json) registers both warning-strict normal and
+optimized commands, each with a 120-second limit. The verifier writes
+only to stdout, including a generated SHA-256-bound receipt. No saved
+receipt is maintained by hand.
+
+The exact finite checks enumerate:
+
+* All 135 isotropic three-spaces in F_2^6, with each of the 63 points
+  occurring exactly 15 times. This tests the new averaging geometry.
+* All 1,080 basis columns of their signed seven-rotation words, using
+  literal Pauli actions and integer Gaussian arithmetic.
+* All 4,096 fourth-root tuples with product one. Their adjacency
+  minimum is -10.
+* All 512 characters of the diagonal subgroup Z4^3 x Z2^3. Its adjacency
+  spectrum has multiplicities {-10:7, -6:56, -2:203, 2:168, 6:77, 14:1}.
+* Forty-nine omitted/replaced-word controls, two semantic controls and
+  five out-of-scope controls, plus 120 width fixtures and exact arithmetic
+  for the new rational constant.
+
+Finite corroboration does not enumerate the full three-axis Clifford
+group or prove the all-dimension quantifiers. Those are supplied by the
+written argument using the cited inputs. The receipt authenticates bytes,
+not mathematical correctness. The verifier neither imports nor executes
+the predecessor checks.
+
+## Limits and implementation constraints
+
+The initial-width improvement requires odd n>=3. For even n, the starting
+width is four modulo eight and the rank-one coefficient has the opposite
+sign. Arbitrary non-Clifford operators, nonunitary scales, nonlinear leaves
+and rounded equalities are outside the theorem. Exact scalar-phase copies
+must be combined before using a projective Gram matrix. Source-dependent
+physical costs, ownership, restoration and the five selected framework
+assumptions are not discharged.
+
+The standalone verifier has fixed finite domains, no recursion, no child
+processes and no output files. Functions remain below 60 physical lines.
+Explicit exceptions keep every check active under optimized execution.
+Managed Python allocation is a deviation from Power of Ten rule 3:
+the root scan streams at most 4^7 tuples, stores seven spectral bins,
+135 seven-point spaces and at most 512 eight-entry character tuples.
+The source inventory has at most eight rows, its JSON at most 64 KiB,
+and each authenticated input/package file at most 1 MiB. Runtime/library
+allocation is not inspected. A port to a restricted runtime would require fixed arrays
+before a constant-allocation claim. Library iteration and dispatch are
+bounded by these domains; there are no user-supplied callbacks.
+Warning-strict execution and the repository metadata/commit checks provide
+the available diagnostics; no external static analyzer is required by the
+package.
+
+## Open next questions
+
+1. Can a phase-aware argument improve the even-axis bound at f=4n+4?
+   Its rank-one sign is negative, so the new lower adjacency estimate
+   does not help there. First seek an upper adjacency or joint-rank
+   inequality that accounts for the trivial character. No such bound
+   or complete even-axis spectrum is provided.
+2. What is the best odd-axis Gram lower constant? The seven-root
+   inequality is sharp for that local relation, while the full-group
+   averaging and higher-rank triangle bounds can lose information.
+   First relate the higher displacement classes to the same local
+   subgroups. A full representation argument remains missing.
+
+## Credit and overlap
+
+Credit Javier Vera / #5714 for the explicit open question and row-method
+limitation, Hiroki KUMAZAKI / #5694 for the count and tail certificate,
+and Ali Romman / #5526 for the trace-lift/projective Gram framework.
+Their classical Pauli, symplectic and Clifford sources and retained
+native/kernel attribution remain with those pinned packages.
+MatShep's #5549/#5594/#5675 one-/two-axis spectra and Ali Romman's #5727
+finite-span contraction tools concern distinct results and are not replayed.
+No global literature-priority claim is made.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214984)
+states the odd-axis scope. Overlap checking covered live open titles,
+recent account contributions, recent handoffs, active Discussions,
+relevant PR bodies, distinctive main README/proof terms and merged searches.
+The card overlap helper reported incomplete local sparse coverage, which
+was supplemented by Git-object searches. These checks do not establish
+universal novelty or cover unpublished work.

research/clifford-seven-rotation-gap/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-pointwise-faithfulness/PROOF.md",
+      "usage": "input",
+      "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c",
+      "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764"
+    },
+    {
+      "path": "research/clifford-residual-count-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "1a604a44071dd65bbf070ac151ad2e85ce7e6d46",
+      "sha256": "c7e99a80da4c651edce8ffa854ee70e7fed6d68db8474ae3f8a66ac554d79dd9"
+    },
+    {
+      "path": "research/clifford-row-sharpness/README.md",
+      "usage": "input",
+      "git_blob": "70ab9d3a62fd0cf6589e034c89f22a49a9411084",
+      "sha256": "8fc1af282142444ba9a3b910bb890fc48b4dec032774e77ba3a7111306681e92"
+    }
+  ]
+}