S1 kappa_3 = d^1 G_3(w): True
S1 kappa_4 = d^0 G_4(w): True
S1 kappa_5 = d^1 G_5(w): True
S1 kappa_6 = d^0 G_6(w): True
S1 kappa_7 = d^1 G_7(w): True
S1 kappa_8 = d^0 G_8(w): True
S1 kappa_9 = d^1 G_9(w): True
S1 kappa_10 = d^0 G_10(w): True
S1 kappa_1 = 0, kappa_2 = 1: True
S2 N_n(e) partition formula equals recursion coefficients for n<=10; Gaussian terms (n-1)!!: True
S3 E M^n (enumeration) = sum_e N_n(e) prod (kappa_j p_j)^e_j for n<=10, 7 vectors x 5 values of u: True
S4 Lemma kvec E|chi_1+..+chi_k| = 2k(1-q)^(k-1) tau for q<1/k, k<=7: True
S5 Lemma two (400 random exact cases, q<=1/2): True
S6 Lemma or (random exact cases in the OR region, n<=8): True ; control outside region differs: True
S7 (1-q4)/q4 = 3+2sqrt3, (1-q5)/q5 = 4+2sqrt5, (1-q6)/q6 = 5+sqrt30: True True True
S7 K4: U- <= u4: True  U+ >= u5: True  w-^4 > 1/2 and 2w-^3 > 1: True  U- >= 2: True
S7 K5: U- <= u5: True  U+ >= u6: True  5w-^8 > 1 and 5w-^6 > 2: True  margin (U+^2-5)^2-30 = 5.166e-05
S7 T8 >= sqrt2-1: True
S7 sqrt5^- = 2236067977499789/1000000000000000, (sqrt5^-)^2 <= 5: True
S7 d/du u^7/(1+u^2)^4 = u^6(7-u^2)/(1+u^2)^5: True ; d/du u^9/(1+u^2)^5 = u^8(9-u^2)/(1+u^2)^6: True
S7 parametrisation identities: True True True
S7 tail bound constant 27/256: True
S7 kvec comparisons reduce to s >= sqrt3/2, s <= 2/sqrt5, s >= 2/sqrt5, s <= sqrt(5/6) (hand-checked).
S7 sharpness endpoint inequalities (2/3)^3 < 1/2 and 5(3/4)^8 < 1: True
S7 q4=0.133975 q5=0.105573 q6=0.087129
SUMMARY {'S1': True, 'S2': True, 'S3': True, 'S4': True, 'S5': True, 'S6': True, 'S7': True} ALL PASS
