PASS [C1] design: 6 pairs partition the 3x4 grid, distinct rows and columns in each pair; theta = (1,1,1,1,1,w), gauge invariant prod_p theta_p^n_p = w^1 on the design cycle n = (-1,2,1,-2,-1,1)
PASS [C1] trace preservation: sum_p (sqrt3 K_p)^dag (sqrt3 K_p) = 3*I_4 exactly, so Psi is CPTP
PASS [C7 guard] Bareiss self-test: PD 2x2 accepted; indefinite 2x2 and singular PSD 2x2 rejected
PASS [C7 guard] Gram self-test: exact 2x2 decomposition P = GG^dag + I accepted; boundary ||E||_F = 1 (P = 0) and indefinite 2x2 rejected
PASS [C2] W and h(y,v): W = N^dag N (144x144 over Z[w], N_ab[(s,s'),(k,k')] = K_a[s,k] K_b[s',k']); h(y,v) = sum_ab |tr(Y^dag K_a V K_b^T)|^2 equals x^dag W x for x = conj(y) (x) v and is >= 2^-14 |x|^2, on 4 exact test pairs over Z[w]
PASS [C3 data] certificates: R 144x110 over 2^-32 Z[w] (sha256 80a51490a7a429a5), G' lower-triangular 144x144 over 2^-24 Z[w] (sha256 bb2b91236f8bc1be) decoded
PASS [C3a guard] Hermitian: P := W - c0*I - Q^Gamma over 2^-64 Z[w], c0 = 2^-14, Q = R R^dag (PSD by construction), partial transpose on the 16-dim factor
PASS [C3a guard] rounding: P = L/2^28 + E with L Hermitian over Z[w] and ||E||_F <= 2^-20 (exact integer comparison)
PASS [C3a] Bareiss route: all 144 leading principal minors of L - 2^8*I are positive integers (fraction-free elimination over Z[w]), so P >= L/2^28 - 2^-20 I > 0
PASS [C3b] Gram route: E := P - G'G'^dag - 2^-14 I computed exactly (all 144^2 entries): ||E||_F^2 < 2^-38 < 2^-28 (exact integer comparison), so x^dag P x >= (2^-14 - ||E||_F)|x|^2 > 0 for x != 0, i.e. lambda_min(P) > 0 (no elimination, no Sylvester)
PASS [C3] conclusion: for product x = u (x) v: x^dag Q^Gamma x = z^dag Q z >= 0 with z = u (x) conj(v) (identity checked on 2 exact test vectors), so x^dag W x >= 2^-14 |x|^2 on product vectors and lambda_min((Psi(x)Psi)(rho)) >= 2^-14/9 for every state rho: r2 = 9, r1 = 3
PASS [C4a] control theta=(1,...,1): F = I3, G = diag(1,1,-1,-1) is an exact product kernel vector there: x^dag W1 x = 0, so r2 <= 8
PASS [C4b] same vector, claimed theta: x^dag W x = 3 > 0
PASS [C4c] same Q fails at control: x^dag (W1 - c0*I - Q^Gamma) x < 0: the same Q is not a certificate for theta = (1,...,1)
PASS [C5] three-copy witness: psi^dag (K_a x K_b x K_c) phi = 0 exactly for all 216 (a,b,c), phi ~ |000>+|111>-|222>-|333>, psi = |000>+|111>+|222> != 0, so rank Psi^(x3)(|phi><phi|) <= 27 - 1 = 26, the bound used in step (4)
PASS [C6a] rational bounds: mu = 2^-14/9 = 1/147456, p = 1/1000: a = 0.988169 <= mu^p < 0.988170 and b = 0.999999 <= (1-8mu)^p < 1.000000 (big-integer comparisons of 1000-th powers)
PASS [C6b] step (4) inequality: (2/3)(1-p) = 333/500, so (3/2) log(8mu^p + (1-8mu)^p)/(1-p) > log 26 <=> X^500 > 26^333 with X = 8mu^p + (1-8mu)^p >= 8a+b; exact: (8a+b)^500 > 26^333; with rank <= 26 (C5): s3 <= log 26 < (3/2) s2
PASS [C6c] exact margin: 8a+b = 8.905351 > 8.757341 >= 26^(333/500) > 8.757340, gap >= 0.148010; (8a+b)^500 >= 2^12 * 26^333
PASS [C6d] explicit tau, lower side: tau = diag(1-2^-20, 2^-21, 2^-21) (trace 1); c = 0.999999 <= (1-2^-20)^p and d = 0.985549 <= 2^(-21 p) (big-integer 1000-th powers), so T = Tr tau^p >= c+2d = 2.971097 > 2.959281 >= 26^(333/1000), gap >= 0.011816; (1-p)/3 = 333/1000, so T^1000 > 26^333, i.e. S_p(tau) > log2(26)/3 >= s3/3; margin S_p(tau) - log2(26)/3 >= 19/3330 >= 0.005705 bits
PASS [C6e] explicit tau, upper side: (1-2^-20)^p < 1.000000 and 2^(-21 p) < 0.985550 (big-integer 1000-th powers), so T <= 2.971100 and T^2 <= 8.827435210000 <= 8a+b = 8.905351 <= X, i.e. S_p(tau) <= B(p)/2 <= s2/2; margins X - T^2 >= 0.077915790000 and B(p)/2 - S_p(tau) >= 7/1110 >= 0.006306 bits
VERDICT PASS: r2 = 9 certified exactly by two independent routes (so r1 = 3); rank <= 26 three-copy witness; s3 < (3/2) s2 at p = 1/1000; explicit tau = diag(1-2^-20, 2^-21, 2^-21) with log2(26)/3 < S_p(tau) <= B(p)/2
