
=== Lemma K(b): f(0) for K = sum of 2m centred uniforms (EXACT Irwin-Hall) ===
sqrt(3/pi)+2/pi^2 = 1.1798473910905154 (< 1.18: True )
max over m<=80 of exact f(0)/bound = 0.999062
max over m<=150 of sqrt(m) f(0) = 1.0 (m=1 gives 1: f(0)=1 for triangular)
consecutive-ratio claim (< sqrt2/pi^2) holds for m<200
max_{u in (0,pi)} (sin u/u - exp(-u^2/6)) = -1.1102230246251565e-16 (should be <= 0)

=== Lemma K(c): P(|K|<eps) >= (3/4) eps/(eps+2 sqrt(m/6)) (EXACT cdf, float compare) ===
violations: 0  min slack: 0.008228807603332468

=== Theorem CD(a): Y for U(-1,2) ===
E Y = 4/27 (claimed 4/27)
P(Y<0) = 4/9 (claimed 4/9)
mu^2/8 = 2/729 (claimed 2/729); 730*2/729 = 1460/729 > 2: True
MONTE CARLO: E Y ~ 0.14847115781857134  P(Y<0) ~ 0.4441175
nu((-eps,eps)) for U(-1,2), eps=1/2: 1/3 (= 2 eps/3)

=== Remark (ferromagnetic, U(0,1), m_k = ceil(9 log(|k|+2))) ===
E min(U,U') = 1/3 (=int (1-t)^2 = 1/3)
Hoeffding simplification valid on grid: True

=== Theorem CD(b): gadget 0 = K_{2,3}, U(0,1): P(K0<=1) ===
P(K0<=1) = 47/90 (claimed 47/90)
P(K0<=1) via polynomial convolution = 47/90

=== Theorem CD(b): rigorous lower bound for P(E) (EXACT, directed rounding) ===
P(E) >=  0.10596461727188013  (claimed >= 0.1059; theorem states 0.105)
check >= 0.1059: True
sum_{j>3000} 1/j^2 < 1/3000 since sum_{j>N} 1/j^2 < int_N^inf dt/t^2 = 1/N

=== Theorem CD(b): NUMERIC estimate of the true P(|G|=4) (evidence only) ===
  j=2: MC P(K<=1) ~ 0.0322   Cantelli c_k = 0.2577
  j=3: MC P(K<=1) ~ 0.0022   Cantelli c_k = 0.1273
  j=4: MC P(K<=1) ~ 0.0000   Cantelli c_k = 0.0722
  j=5: MC P(K<=1) ~ 0.0000   Cantelli c_k = 0.0457
MONTE CARLO estimate P(E) ~ 0.445 (j>=6 ignored, their contribution is tiny) -> P(|G|=4) ~ 0.555

=== Theorem B, Step 3 constants ===
q>=100: 2^{1/3} = 1.2599210498948732 <= 1.26: True
1.26q+2 <= 1.28q iff q>=100 ; q^2/2.56 >= 39q iff q >= 99.84 ; 2.26q+4 <= 2.3q iff q>=100
at q=100: True True True True
NUMERIC: last a <= 10^6 where E_a/2 > w(a)+w(2a)+2 FAILS (exact E_a): 390
NUMERIC: last a <= 10^6 where (a+1)/(2(w(2a)+1)) > w(a)+w(2a)+2 FAILS (proof's lower bound): 527
partial sum_{a<10^6} exp(-(a+1)/(2(w(2a)+1)^2)) = 348.1586918010772 (finite; tail ~ exp(-c a^{1/3}))

=== Theorem B, Step 6: L_x, ell_x and sum (3w(x)+2) 2^{-ell_x} ===
violations of the three elementary inequalities for 1<=x<2e6: 0
sum_{0<|x|<2e6} (3w(x)+2) 2^{-ell_x} = 10661.701334386224
L_1 = 2  (Lemma len, case a=b needs L_1 = 2)
delta = 1/(6e) ; e*delta = 1/6 ; union bound factor 2*3^{l-1}*6^{-l} = (2/3) 2^{-l}
l! >= (l/e)^l for l=1..200: True

=== Proposition mf: Hoeffding for A_k, m_k=|k|+1 ===
sum_k exp(-2(m_k/3-1)^2/m_k) over m_k>=3 (both sides) = 13.564451961717692 (finite)
E min(|J|,|J'|) for U(-1,1) = E min(U,U') = 1/3

=== Series in Theorem A / Corollary A ===
sum (|k|+1)^{-3/2} converges (p=3/2>1); sum (|k|+1)^{-1} diverges; sum (|k|+1)^{-2} converges
Remark: m_k>=1 => m_k^{-1} <= m_k^{-1/2}, so sum m^{-1/2}<inf => sum m^{-1}<inf

ALL ASSERTIONS PASSED
