Verify a complete Clifford provider and exclude 30,328 paid-pair fusions

research/clifford-tensor-gram/ADVANCES-MUTATIONS.json

@@ -0,0 +1,45 @@
+{
+  "cases": [
+    {
+      "mutation": "conjugate native C factor",
+      "optimized": false,
+      "rejection": "Native trace phase"
+    },
+    {
+      "mutation": "conjugate native C factor",
+      "optimized": true,
+      "rejection": "Native trace phase"
+    },
+    {
+      "mutation": "ignore native inverse sign",
+      "optimized": false,
+      "rejection": "Native entry phase"
+    },
+    {
+      "mutation": "ignore native inverse sign",
+      "optimized": true,
+      "rejection": "Native entry phase"
+    },
+    {
+      "mutation": "omit output prefix constraint",
+      "optimized": false,
+      "rejection": "Native partial inner product"
+    },
+    {
+      "mutation": "omit output prefix constraint",
+      "optimized": true,
+      "rejection": "Native partial inner product"
+    },
+    {
+      "mutation": "omit final native return",
+      "optimized": false,
+      "rejection": "Compact complete endpoint"
+    },
+    {
+      "mutation": "omit final native return",
+      "optimized": true,
+      "rejection": "Compact complete endpoint"
+    }
+  ],
+  "status": "PASS_CLIFFORD_ADVANCE_MUTATIONS"
+}

research/clifford-tensor-gram/ADVANCES-RESULT.json

@@ -0,0 +1,50 @@
+{
+  "code_fourier_values": 256,
+  "complete_programs": 48,
+  "controls": [
+    "singular permutation",
+    "diagonal parity",
+    "asymmetric diagonal",
+    "wrong C sign",
+    "unknown gate",
+    "coordinate out of range",
+    "invalid prefix",
+    "negative axes"
+  ],
+  "exact_native_relations": 9,
+  "exhaustive_quadratic_forms": 640,
+  "filter_axis_counts": 65,
+  "general_test_widths": "8n-3 through 8n+4 for n>=2",
+  "large_native_programs": [
+    {
+      "axes": 64,
+      "base_dimension": "18446744073709551616",
+      "equivalent": false
+    },
+    {
+      "axes": 65,
+      "base_dimension": "36893488147419103232",
+      "equivalent": true
+    }
+  ],
+  "literal_witnesses": 48,
+  "native_entries": 3328,
+  "native_traces": 128,
+  "native_words": 128,
+  "one_axis": {
+    "group_sha256": "32481fd502c5f388244bcd56d20fbc0e0ca3933f47dbbdbbd8215397cea0238d",
+    "image_of_i": 256,
+    "prime": 65537,
+    "rank": 96,
+    "widths": [
+      5,
+      6,
+      7,
+      8
+    ]
+  },
+  "partial_inner_products": 304,
+  "scalar_phase_traps": 1,
+  "stable_separation": "75/76",
+  "status": "PASS_CLIFFORD_ADVANCES_NO_NEW_KAPPA"
+}

research/clifford-tensor-gram/ADVANCES.md

@@ -0,0 +1,251 @@
+# Fewer widths and exact computation without dense matrices
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+This note extends [PROOF.md](PROOF.md). It uses the same group C_n, exact
+global phases, complete register endpoints and coefficients that do not
+depend on the positive tensor width f. Set D=2^n. No result changes kappa.
+
+## 1. Eight widths suffice for every axis count
+
+For n>=1, a fixed residual vanishes at every positive width if and only if
+it vanishes at the eight widths
+
+    8n-3, 8n-2, ..., 8n+4.
+
+For n=0, use widths 1,2,3,4. For n=1, Section 3 improves the test to
+widths 5,6,7,8. The number of tests and the largest tested width are
+different quantities. The general maximum 8n+4 has not decreased.
+
+Let E be the binary code generated by the four length-eight rows
+11111111, 11110000, 11001100 and 10101010. It has dimension four. Its
+weights are 0,4,8, and E=E-perp for the binary dot product. Define T_n
+in (C^D) tensor-power 8 by summing the basis vectors whose n binary rows
+all belong to E. This vector is nonzero.
+
+The vector T_n is fixed by the eighth tensor power of each native generator:
+
+- S on one axis contributes i to the power of that row's weight. This is 1.
+- CNOT adds one code row to another. It permutes the summands.
+- The native Hadamard is ((1+i)/2) times the binary Fourier matrix.
+  Its eighth tensor power has coefficient 1/16. The Fourier sum of E
+  is 16 times the indicator of E-perp=E. Thus it fixes T_n, with phase 1.
+- The scalar iI has eighth power 1.
+
+These gates generate C_n. Here is a direct reduction argument. The image
+of Z_1 under a Clifford is a nonidentity Pauli. Single-axis H and S gates
+convert each nonzero component to Z. CNOT gates reduce the resulting
+nonempty Z string to Z_1. An X gate corrects its sign. The image of X_1
+then anticommutes with Z_1. CNOT and controlled-Z gates with control 1
+remove its components on the other axes. An S gate removes its remaining
+Z_1 component, and Z_1 corrects its sign. These changes preserve Z_1.
+The remaining operator fixes X_1 and Z_1, so it has the form I tensor V.
+Repeat on V. The final scalar is a dyadic Gaussian unit of absolute value
+one, hence one of 1,i,-1,-i, as proved in PROOF.md. Replace each ordinary
+H in this argument by the native Hadamard. The Pauli action is unchanged;
+the final scalar still belongs to the same four-element group.
+
+Normalize T_n to a unit vector tau. The injection J_f(v)=v tensor tau
+satisfies
+
+    (sum_g c_g g^(tensor(f+8))) J_f
+      = J_f (sum_g c_g g^(tensor f)).
+
+Thus vanishing at f+8 implies vanishing at f. Every integer from 1 to
+F=8n+4 can be increased by a multiple of eight to a member of F-7,...,F.
+The first theorem in PROOF.md now gives the stated eight-width test.
+Apply the argument separately to every input and output role.
+
+This argument does not transfer the dimension-free stability constant
+to the eight selected widths. The bound in Section 2 uses all widths
+1,...,8n+4. A direct restriction argument loses powers of D.
+
+The code invariant is classical. See Runge's prior results as credited in
+[Nebe, Rains and Sloane, The invariants of the Clifford groups, Sections 4
+and 6](https://arxiv.org/pdf/math/0001038). The contribution here is its
+use in the fixed-coefficient endpoint test, with the native phase checked.
+
+## 2. Uniform separation improves from 14/15 to 75/76
+
+For distinct exact operators and M=sum_g |c_g|^2, let
+E_f=D^(-f)||sum_g c_g g^(tensor f)||_HS^2. Then
+
+    max_(1<=f<=8n+4) E_f >= (75/76) M.
+
+Use the same filter as PROOF.md. Write r=-1/4, m=2n and
+
+    P_m(t) = product_(j=1..m) (t-r^j)/(1-r^j),
+    q_n(z) = (z+z^2+z^3+z^4) P_m(z^4)/4.
+
+The four residue classes of coefficients do not overlap. Therefore the
+sum of absolute coefficients of q_n equals that of P_m.
+
+In descending degree, the coefficient with index l has sign
+s_l=(-1)^(l(l+3)/2), namely ++--++--. To check this, the elementary
+symmetric function in r,...,r^m equals
+
+    r^(l(l+1)/2) product_(k=1..l) (1-r^(m-l+k))/(1-r^k).
+
+This identity follows by separating subsets that contain the last root;
+the empty product gives the initial case. Every factor in the product
+is positive. Include the coefficient sign (-1)^l to get s_l.
+
+Let u_l be the absolute coefficients of P_(2n), L their sum, and U_odd
+their sum over odd l. Add the next two roots -a,b, where
+b=16^(-(n+1)) and a=4b. The new factor is
+(t^2+(a-b)t-ab)/((1+a)(1-b)). The sign rule gives
+
+    L_new - L = [2ab L - 2(a-b) U_odd]/((1+a)(1-b)).
+
+For n>=1, the unnormalized coefficient of t^(2n-1) has magnitude
+(1-16^(-n))/5 >=3/16. The sum of the unnormalized absolute coefficients
+is at most product_j(1+4^(-j)) <=3/2. The last inequality follows by
+expanding the product and bounding it by the geometric series whose
+ratio is sum_j 4^(-j)<=1/3. Hence U_odd/L>=1/8. On the other hand,
+ab/(a-b)=4b/3<=1/192. Thus L_new<L for n>=1.
+
+For n=1, P_2(t)=(64t^2+12t-1)/75, so L=77/75. For n=0, L=1.
+Consequently the positive coefficient mass of q_n is at most
+(1+77/75)/2=76/75. The exact identity sum_f b_f E_f=M and E_f>=0
+give the claimed bound. This is a bound for this filter; optimality of
+the operator stability constant is not claimed.
+
+The implementation forms the integer numerator
+product_j(4^j t-(-1)^j) and the common denominator
+product_j(4^j-(-1)^j) first. It reduces fractions only when it emits q_n.
+This gives the same polynomial and avoids repeated large rational reductions.
+
+## 3. The one-axis maximum cutoff is exactly eight
+
+The frozen native C and S gates generate all 96 exact operators of C_1.
+Their closure and phases are checked in verify.py. Let
+
+    K[g,h] = sum_(f=5..8) (tr(g* h)/2)^f.
+
+The file [ONE-AXIS-RANK.json](ONE-AXIS-RANK.json) contains an inverse of K
+after reduction to F_65537 with i mapped to 256. The checker reconstructs
+K, checks that 65537 is prime and 256^2=-1, and multiplies K by this
+inverse. It does not use the elimination routine to check the inverse.
+All original denominators are powers of two. A nonzero reduced determinant
+therefore proves that the characteristic-zero determinant is nonzero.
+The positive semidefinite Gram sum K has zero kernel. This proves that
+widths 5,6,7,8 suffice for every fixed residual on C_1.
+
+The Reynolds example in PROOF.md vanishes at widths 1 through 7 and is
+nonzero at width 8. The maximum cutoff eight is therefore sharp.
+At least four tested widths are required: for each residue r modulo four,
+the four scalar operators give the residual
+
+    sum_(k=0..3) i^(-rk) (i^k I)^(tensor f).
+
+It vanishes unless f is congruent to r modulo four. A test set that omits
+one residue cannot detect this residual. Thus four is also the minimum
+number of widths for a fixed universal test on C_1. Neither conclusion
+establishes a sharp cutoff for n>=2.
+
+## 4. A phase-exact quadratic path calculation
+
+[quadratic.py](quadratic.py) accepts the frozen native P, X, D, C and
+phase gate grammar. It keeps a list of binary affine output bits and a
+phase polynomial modulo four. The polynomial has arbitrary linear
+coefficients and even cross coefficients. It also keeps an exact Gaussian
+scalar factor. It never allocates an array indexed by the 2^n base states.
+
+Start with n input variables. P and X change only the affine output bits.
+D adds its stated linear and even quadratic phase. For C(q,s), use
+
+    C(q,s) = ((1+s i)/2) (I + i^(-s) X_q).
+
+Add one binary path variable a, multiply the scalar factor by (1+s i)/2,
+add -s a to the phase and add a q to the output bits. Keep the literal
+phase gate. The formula also covers q=0. The number of variables is
+m=n+h, where h is the number of C gates in the literal word.
+
+An affine parity has, modulo four, its constant and linear terms plus
+even pair terms. Terms of degree at least three vanish modulo four.
+Twice a product of parities needs only the product over F_2. Thus every
+gate preserves this representation, including affine translations.
+
+An entry fixes the input and output bits. A trace equates them. Binary
+elimination either rejects inconsistent equations or gives an affine
+parametrization with one assignment per solution. Substitute this map
+in the phase. The remaining unconstrained sum is evaluated as follows:
+
+- For an odd linear coefficient a of variable x, write its part as
+  a x+2 x L. Summing x gives (1+i^a) i^(-a L). Remove x and add the
+  indicated parity phase. This keeps the same quadratic form class.
+- If every linear coefficient is even and a cross term remains, sum one
+  variable x. The result is twice the sum subject to a binary affine
+  constraint on its neighbors. Eliminate that constraint.
+- If no cross terms remain, a linear coefficient 2 makes the sum zero.
+  Otherwise each remaining variable supplies a factor two.
+
+Each step removes at least one variable. The code uses direct polynomial
+substitution. A conservative bound is O(m^5) arithmetic operations per
+sum, plus O(L m^4) to build a path form for L native gates. It uses
+polynomial space. This bound is not a
+claim of optimal stabilizer simulation or constant-time integer arithmetic.
+Coefficient bit lengths are polynomial in the literal word length.
+
+The use of binary quadratic forms for Clifford operations is classical;
+see [Dehaene and De Moor, Sections III-V](https://arxiv.org/pdf/quant-ph/0304125).
+The new implementation derives its phases directly from the pinned native
+kernel. The dense frozen kernel remains a separate finite test oracle.
+
+## 5. Bitwise witness extraction removes the D^2 scan
+
+For two operators g,h and fixed prefixes of the output and input bits,
+define B(g,h) as the sum of conjugate(g[x,y])h[x,y] over the unspecified
+bits. Combine two path sums, negate the left phase, equate their input
+and output bits, and impose the prefix equations. Section 4 computes B
+in polynomial time, with at most the sum of both path-variable counts.
+
+With r tensor factors still after the current factor, the conditional
+squared norm is
+
+    sum_(g,h) conjugate(c_g)c_h B(g,h) (tr(g* h)/D)^r.
+
+It is real and nonnegative. The two choices for the next coordinate bit
+partition its sum. Choose the larger child. After 2n choices, the current
+base coordinate pair is fixed; multiply each coefficient by g[x,y] and
+continue with the next tensor factor. There are 2nf bit choices, each
+with two children, instead of fD^2 coordinate trials.
+
+At the start of one factor the conditional norm is D E. The 2n splits
+lose at most D^2. Induction gives the same final entry bound as PROOF.md:
+
+    |entry|^2 >= E_f D^(-f).
+
+[compact.py](compact.py) also expands complete register endpoints as
+signed native words. It retains every input and return role. It merges
+two unitary words exactly when tr(g* h)/D=1; the identity
+||g-h||_HS^2=2D-2 Re tr(g* h) proves this test. Global phases stay inside
+the operator keys, not in coefficients outside the tensor power.
+
+For expanded support s and a maximum literal path size m, pair traces
+cost O(s^2 poly(m)). A witness costs O(n f s^2 poly(m)) arithmetic
+operations, with polynomial space in these parameters. No 2^n matrix or
+2^(nf) tensor is built. The symbolic support s can still grow exponentially
+in the register-program length. This result does not remove that obstacle.
+
+## Verification and limits
+
+[verify_advances.py](verify_advances.py) checks the code invariant, exact
+filter bounds, modular inverse certificate, exhaustive small quadratic
+sums, frozen native entries and traces, conditional inner products, and
+complete programs against the original dense compiler. It checks larger
+native examples without a dense matrix. ADVANCES-RESULT.json records the
+executed counts. Normal and optimized Python must produce the same receipt.
+
+The proofs above are written arguments, not proof-kernel certificates.
+The code invariant and quadratic-form method have classical predecessors.
+The sparse full-program adapter, finite-width refinements and native phase
+bindings are the present contribution. No complete current provider or
+physical cost invoice has been run. No selected frontier changes here.
+
+## Open next questions
+
+1. Prove a sharper maximum cutoff for n>=2, or give a matching obstruction.
+2. Bound support growth on one complete current provider before a large run.
+3. Derive a useful stability constant for the eight selected widths.
+4. Improve the quadratic elimination cost after a measured provider needs it.