A  constants and inequalities in b
   1/54 = (1/3)^2/(2*3); b-inequalities at 9 values of b in (1/8,1/6]: ok
B  Lemma 3.1 against the literal generator sum
   geometric sums (j <= 6): max error 5.4e-13; 1152 entries, 6 values of b: max |literal - formula| 1.7e-15
C  structure lemmas from the definition (exact), window 0 < |y| <= R
   b = 1/8 and 9 values of b in (1/8, 1/6]; R = 128
   88 fibers (60 random + 28 near-exceptional), 2816 vertices with all neighbours in the window:
   Lemmas 3.2, 4.1-4.4 and the row-sum bound hold; 244 simple vertices, all with a branching child;
   flow p <= 3 (max 9/4); 3520 random sets F with |dF|/|F| >= 1/3 (min 8/11);
   G_W - I/54 and 6I - G_W positive definite in every fiber (exact); tree vs dense elimination agree in 30 cases
D  Remark 4.5: b > 1/6
   [2-8b, 4b] invariant for 4 values of b in (1/6, 1/5]; c_1-chains of simple vertices with d = 2;
   exact tent quotients <G w, w>/|w|^2: b=9/50 L=8: 3/14, b=9/50 L=16: 1/20, b=1/5 L=8: 3/14, b=1/5 L=16: 1/20
E  Section 7: the map P(t) = position of 1 - t
   P(1-t/2) = P(1-t/4) = t at 2000 rational t; positions within 2^-n/12 of 2/3 need more than n steps
time 16 s
ALL CHECKS PASSED
