== A. Lemma 5.1
PASS A1 y(0.98-y) at y = 0.1 and y = 0.88 equals 0.088 (minimum on [0.1,0.88]: concave)
PASS A2 one strip holds at most 1.02/5 = 0.204 (in units m^2)
PASS A3 first sliding square with >= 0.1 blue has < 0.1 + 0.204 = 0.304 <= 0.88 blue
PASS A4 five balanced strips hold between 0.98 and 1.02
== B. Corollary 5.3 (delta = 1/2000, k >= 16000)
PASS B1 ceil(dk)^2 <= 2 d^2 k^2 for every integer 16000 <= k <= 200000
PASS B2 k/400 - 4 ceil(dk) >= k/4000 for every integer 16000 <= k <= 200000
PASS B3 delta*16000 = 8 and 8 >= 1 + sqrt(2)  (FLOAT for sqrt)
PASS B4 k/400 - 4*(delta k + 1) - k/4000 = k/4000 - 4 (vanishes at k = 16000)
     largest k < 16000 at which B2 fails: 14222 (the bound k >= 16000 is used only through B1, B2)
== C. Lemma 5.4
PASS C1 E1: Var N / (0.01 m^2 k^2)^2 = 10^4/(m^2 k^2)  (tested at m^2 k^2 = 7, 10^6)
PASS C2 E2: Chebyshev 2 m^4 k^2 / (m^2 k^2 psi / 2)^2 = 8/(k^2 psi^2)
PASS C3 E2: E N_sigma^2 = m^4 + m^2 <= 2 m^4 (m = 1..999)
     psi(m) = 4 q_m^(1/2) <= 0.003 iff q_m <= 9/16000000 = 5.625e-07
PASS C4 block: ceil(dk/2) + 2 <= ceil(dk) for 16000 <= k <= 200000 (analytically: dk >= 6)
PASS C5 Case A: (dk + 1)^2 <= 0.001 k^2 at k = 16000, 16001, 10^5, 10^7 (increasing margin)
PASS C6 Case A: min of y(0.98 - y) on [0.09, 0.93] = min(0.09*0.89, 0.93*0.05) = 0.0465  [93/2000]
PASS C7 beta_0 = 0.088 * (1/4000) / 4 = 11/2000000  [11/2000000]
PASS C8 Case A: 0.0465 * (0.005 - 0.001) = 1.86e-4 >= beta_0 (so the Case A bound exceeds beta_0 m^4 k)
     Case B LP: min S^< = 194/775 = 0.2503226 at ['194/775', '1/200', '4617/6200']
     Case B LP: min S^> = 663/1550 = 0.4277419 at ['3517/6200', '1/200', '663/1550']
PASS C9 Case B: exact LP minimum of S^< is 194/775
PASS C10 Case B: exact LP minimum of S^> is 663/1550
PASS C11 Case B: elimination formulas (0.237 - 0.84*0.005)/0.93 and (0.402 - 0.84*0.005)/0.93
PASS C12 Case B: 194/775 >= 1/4 + 2 delta^2 and 663/1550 >= 1/4 + 2 delta^2  [194/775 - 1/4 = 1/3100]
PASS C13 colours: yellow (b < 0.1) contains S^< (b < 0.09); green (b >= 0.1) contains S^> (b > 0.93)
PASS C14 Lemma 5.1 applies to a yellow-green pair: yellow b < 0.1 <= 0.88
     with threshold 0.93 and both colours only >= 0.33: min S^< = 194/775, min S^> = 194/775 (symmetric)
== D. Section 6: the tail constant
PASS D1 (1/2) n^2 r^2 = m^4 k^2 for n = mk, r^2 = 2 m^2, and d/r = delta k/(2 sqrt2) for d = delta n/2 (m, k = 1..60; the second identity squared, exact)
     c = beta_0 delta / (8 sqrt2 pi) = 11/(32 sqrt2 pi 10^9) = 7.737093e-11  (FLOAT)
PASS D2 c = 11/(32 sqrt(2) pi 10^9) and 7.7e-11 < c < 7.75e-11  (FLOAT)
PASS D3 for t >= delta/(2 sqrt2), k = ceil(2 sqrt2 t/delta): t <= delta k/(2 sqrt2) <= 2t and k <= 4 sqrt2 t/delta (200000 values of t; FLOAT)
PASS D4 for the same t and k: beta_0/(2 pi k) >= c/t, the last step of the tail bound (FLOAT)
== E. Lemma 4.1 on all trees with at most 10 vertices
PASS E1 numbers of trees with 1..10 vertices up to isomorphism = 1,1,1,2,3,6,11,23,47,106 (OEIS A000055)  [[1, 1, 1, 2, 3, 6, 11, 23, 47, 106]]
     130947 pairs (tree, W) with 3 <= |W| <= n <= 10; 1272912 walks
PASS E2 the walk never reverses, stops within n steps, and stops at a vertex all of whose branches have weight <= N/2 (from every start vertex)  [violations = 0]
PASS E3 the merge gives N/3 <= |B| <= N/2  [violations = 0]
PASS E4 every tree path from B to W \ B passes through v_*  [violations = 0]
PASS E5 negative control: moving one vertex of a piece across the bipartition is always detected by the path test  [98340 of 98340]
PASS E6 negative control: without the complement step |B| > N/2 occurs  [1908 cases]
== F. Section 8: the published inequality (2.16) of Aldous (2021)
     published bookkeeping (thresholds 0.09/0.89, both colours >= 0.33 m^2k^2, psi = 0): min S^< = 98/445 = 0.220225, min S^> = 118/465 = 0.253763
PASS F1 exact LP minimum of S^< with the published bookkeeping is 98/445 < 1/4
PASS F2 exact LP minimum of S^> with the published bookkeeping is 118/465 >= 1/4
PASS F3 the same with blue >= 0.495 m^2k^2: min S^< is still 98/445
     Example 8.1 with m = 1000, k = 200: S^< = 9860, S = 200, k^2/4 = 10000, |B| = 13335370060, N = 40000000000, |B|/N = 0.3333843
PASS F4 Example 8.1 (m = 1000, k = 200): all squares balanced with exactly m^2 points; S = 0.005 k^2; (2.13) holds; N/3 <= |B| <= N/2; but S^< < k^2/4
PASS F5 Example 8.1 for every m in {130, 140, ..., 390} and k in {100, 200, 300}
PASS F6 |B| - N/3 = k^2((0.333385 - 1/3) m^2 - 0.7485) >= 0 iff m^2 >= 14487.1..., so all m >= 130 work  [threshold m^2 = 14487.097]
PASS F7 repaired bookkeeping (threshold 0.93, blue >= 0.495, psi = 0.003): LP minima 194/775 and 663/1550
TOTAL: 39 checks, 0 failed; ALL CHECKS PASSED  (9.1 s)
