PASS [B1] Baer-Haah bounds at n=4: (4^n+16)/(16(4^n-1)) = 1/15 = 17/255 <= Delta_4 <= 2^n(2^n-3)/(8(4^n-1)) = 26/255, and 1 - 26/255 = 229/255; at n=3 both bounds equal 5/63 (Delta_3 = 5/63); for n = 1..64 the lower bound equals 1/(2^n-1) only at n = 4 (below it for n <= 3, above it for n >= 5)
PASS [W1] the 30 sets A(s,c) = {x : s.x = c} (s != 0, c = 0,1) are distinct 8-subsets, A(s,0) and A(s,1) are complementary, and they are exactly the affine 3-flats among all 12870 8-subsets of F_2^4; w = sum_A e_A (ascending binary order) has 30 coefficients +1 and |w|^2 = 30
PASS [W2] Z-type counting: for each of the 15 Z-type Paulis Z_s = P_(0,s), e_A has Z_s-charge sum_{x in A} (-1)^{s.x} = 0 on the 28 hyperplanes with normal != s and +8, -8 on A(s,0), A(s,1); hence <w, Pi_0^{Z_s} w> = 28 = (14/15)|w|^2
PASS [W3] order lemma: for each of the 30 hyperplanes A(s,c), deleting the lowest set bit of s maps A (binary order) increasingly and bijectively onto F_2^3 (echelon coordinates are order isomorphisms); all 1344 elements of AGL(3,2) are even permutations of F_2^3, i.e. AGL(3,2) < A_8
PASS [W4] all 20160 elements of GL(4,2) and all 16 translations map each e_A to +e_{g(A)} with g(A) a hyperplane (sorting signs checked on all 30 wedges), so every affine bijection of F_2^4 fixes w; listing each A in bit-reversed order or in Gray-code order changes no sign: the same w exactly
PASS [W5] RM(1,3) is self-dual: the 16 affine functions F_2^3 -> F_2 (words of length 8) form a linear [8,4] code C, and brute force over all 256 words gives C^perp = C
PASS [W6] 20 Clifford generators, exact expansion over Z[i] with ascending-order wedge signs: Lambda^8(sqrt2 H_j) e_A = 16 e_A for the 14 hyperplanes with s_j = 0; each of the 16 with s_j = 1 expands to 256 terms +-e_B and their sum is mapped to 16 times itself (the RM(1,3) character sum); so Lambda^8(sqrt2 H_j) w = 16 w (j = 0..3), Lambda^8(S_j) w = w (4), Lambda^8(CNOT_jk) w = w (12 pairs)
PASS [W7] local Clifford reduction: for each of the 255 non-identity P, C_P = tensor of 1, sqrt2 H, (sqrt2 H)S by qubit letter (I or Z, X, Y) satisfies C_P P = +-Z^{supp P} C_P exactly over Z[i] (135 with +, 120 with -), with (sqrt2 H)^dag(sqrt2 H) = 2; by [W6] Lambda^8(C_P) w is a multiple of w, so <w, Pi_0^P w> = <w, Pi_0^{Z^{supp P}} w> = 28 for all 255 P
PASS [W8] Rayleigh quotient: <w, M w>/<w, w> = (1/255) sum_P 28/30 = 14/15 = 238/255 > 229/255 = 1 - 26/255 (the 3^|s| Paulis of support s all give 28); so ||M_(1^8,0^8)|| >= 14/15
PASS [W9] Lie route (all 255 P, exact integers): t_P = prod_{c=2,4,6,8}(H_P^2 - c^2) w satisfies H_P t_P = 0, so t_P = 147456 Pi_0^P w; <w, t_P> = 147456*28 for every P and sum_P t_P = 147456*238*w, i.e. M w = (14/15) w exactly [largest support of t_P: 142 of 12870; hopping signs agree with the Leibniz-rule wedge expansion on 48 basis vectors for all 255 P]
PASS [W10] Casimir upper bound: all 255 P are Hermitian involutions with tr P = 0, so H_P has spectrum in {-8,...,8} on Lambda^8 and Pi_0^P <= 1 - H_P^2/64; sum_P H_P^2 e_B = 1088 e_B (= d k(d-k+1) - k^2, d = 16, k = 8) on the 30 hyperplane wedges and 18 seeded random basis vectors; hence M <= 1 - 1088/(64*255) = 14/15, i.e. ||M_(1^8,0^8)|| <= 14/15
PASS [S1] Walsh divisibility: 2^m sum_{x in y+W^perp} mu_x = sum_{S in W} (-1)^{S.y} c_S(mu) holds on all unit weights for every subspace W (dim m >= 1) and every y, n = 3 (15 subspaces) and n = 4 (66), hence for all integer weights; over all 0/1 weights (256 and 65536), c_S = 0 on W\0 forces 2^m | |mu|
PASS [S2] Bose-Burton (q = 2), exhaustive: max |Z|, Z in F_2^n\0 with Z+0 containing no (v+1)-dim subspace, is [0, 4, 6] (n = 3) and [0, 8, 12, 14] (n = 4) = 2^n - 2^(n-v); attained by Walsh zero sets (max number of vanishing Z-charges over the 65536 0/1 weights, v = 0..4: [0, 8, 12, 14, 15]); the 20 generators map every P to +-P' exactly and act transitively on the 255 Paulis; so ||M_lambda|| <= (2^n - 2^(n-v))/(2^n - 1), at n = 4: 0, 8/15, 4/5, 14/15 for v = 0..3
PASS [S3] sharpness: on Lambda^2 C^d (n = 2, 3, 4, all basis vectors, all Paulis) H_P(H_P^2 - 4) = 0 and sum_P H_P^2 = 2d(d-1) - 4, so M = d/(2(d-1)) = (2^n - 2^(n-1))/(2^n - 1) (v = 1); on Lambda^4 C^8 3456*1 - sum_P (H_P^2-4)(H_P^2-16) is PSD with nullity 7 (exact LDL), so ||M|| = 3456/4032 = 6/7 (v = 2); Lambda^8 C^16 attains 14/15 (v = 3) through w
PASS [S4] corollary, n = 3..64 (exact): if 8 does not divide |lambda| then v <= 2 and ||M_lambda|| <= (2^n - 2^(n-2))/(2^n - 1) < 1 - 2^n(2^n-3)/(8(4^n-1)), margin (4^n - 3*2^n - 8)/(8(4^n-1)) > 0; the v = 3 bound (2^n - 2^(n-3))/(2^n - 1) exceeds 1 - 2^n(2^n-3)/(8(4^n-1)) by (4*2^n + 8)/(8(4^n-1)); at n = 4: 204/255 < 229/255 < 238/255
PASS [C1] positive control n = 3: the Lambda^4 code projector (rank 7) in End(Lambda^4 C^8), traceless part, has Rayleigh quotient 58/63 = 1 - 5/63 = 1 - Delta_3 for each of the 7 Z-type P, with the same wedge-sign and charge conventions; it exceeds the v = 2 bound 6/7 (balanced irreps have v = n)
PASS [C2] positive control n = 4: the Lambda^4 code projector (rank 35) in End(Lambda^4 C^16), traceless part, has Rayleigh quotient 229/255 = 1 - 26/255 (the t = 4 value behind Eq. (2)) for each of the 15 Z-type P; 229/255 < 14/15
PASS [N1] negative control: three seeded random sign patterns on the 30 hyperplane wedges give exact Rayleigh quotients [764/1275, 2386/3825, 2362/3825] (all < 229/255 < 14/15); the all-+1 pattern w gives 14/15 by the same routine
PASS [N2] negative control: ascending wedges in non-affine orders of F_2^4 break the witness: weight-then-binary order: 23 signs flip, quotient 154/225; seeded random order: 20 signs flip, quotient 2434/3825 (both < 229/255)
PASS [N3] negative control: over all 12870 8-subsets B, the number of Z-type Paulis with charge 0 on e_B is 5, 7, 11 or 14 (multiplicities 10080, 1920, 840, 30), and 14 occurs exactly for the 30 hyperplanes; every other 8-subset is non-neutral for at least 4 of the 15 Z-type Paulis
PASS [E1] (floating point; relative tolerance 1e-9) f(U) = sum_A det U[A,B0] has f(1) = 1 for B0 = {0,...,7}; at 3 seeded pseudo-random U in SU(16) (|U^dag U - 1|, |det U - 1| < 1e-9) with seeded 8-sets B0 and |f(U)| > 1e-3, (K_4 f)(U) = (1/255) sum_P mean_theta f(e^{i theta P} U), theta on 17 equally spaced angles (exact for this trigonometric polynomial of degree <= 8), equals (14/15) f(U); f(omega U) = -f(U) for the central omega = e^{2 pi i/16}, so f has Haar mean 0
PASS [T] Theorem: M w = (14/15) w ([W9]; Rayleigh route [W8]) and ||M_(1^8,0^8)|| <= 14/15 ([W10]; independently the selection bound with v = nu_2(8 mod 16) = 3, (16-2)/15 [S1],[S2]), so ||M_(1^8,0^8)|| = 14/15 > 229/255; hence ||K_4 on L^2_0|| >= 14/15, Delta_4 <= 1/15 < 26/255 and Eq. (2) fails at n = 4; with Baer-Haah Thm 3.16 (Delta_4 >= 1/15), Delta_4 = 1/15
VERDICT PASS: all 22 checks passed (21 exact, [E1] floating point); M w = (14/15) w, ||M_(1^8,0^8)|| = 14/15, Delta_4 = 1/15 < 26/255
