ok    Lemma 2.2: the tuple (z,a,b,p,c,q,r,x) uses za, zb, zc and 9 pairs inside K (|K| = 7 used)
ok    Lemma 2.5: the two tuples certify s0s3 and then s0z
ok    Lemma 2.5: the face gadget on K_7 percolates (closure computed)
ok    Lemma 2.5: the face gadget on K_8 percolates (closure computed)
ok    Lemma 2.2: K_7 plus a vertex with two neighbours percolates
ok    Lemma 4.1: ex(2..7) = 1,2,4,5,7,9 (all subsets of Q_3)
ok    Remark 4.2: e_1..e_7 = 2,4,6,7,9,10,11
ok    Remark 4.2: e_i = 11 - ex(8 - i)
ok    Remark 4.2: min_{i<=7} e_i/i = 11/7, min_{i<=6} e_i/i = 5/3
ok    Remark 4.2: g*_2(1) + 11 = e_1 + 11 = 13 < 16
ok    (2): f(8)=11, f(2)=1, 11-8a+c=0, 2a-c=1
ok    (2): slacks a*w-c-ex(w) = 0,2/3,1/3,1,2/3,1/3
ok    Remark 4.2: the scheme allows slope at most (11-ex(2))/6 = 5/3
ok    end game: a - c/8 = 11/8, a - c/2 = 1/2
ok    end game: min over n = 8..80 of the weight w(x) is 15/8
ok    Table 1: ceil((5n-7)/3) for n = 8..18
ok    Table 1: floor((7n+2)/4) for n = 8..18
ok    Theorem 1.3: floor((7(n+4)+2)/4) = floor((7n+2)/4) + 7
ok    Theorem 1.2 agrees with floor((7n+2)/4) for 9 <= n <= 13
ok    Theorem 1.2 is consistent with Theorem 1.4
ok    Proposition 5.1: k = 3,4,6,7,9,11 give the lower bounds 12 + k = 15,16,18,19,21,23
ok    upper bounds: 16+2, 19+2, 16+7
ok    Table 2: S_8 has 15 edges
ok    Table 3: certificates of S_8 as printed: 11 listed steps, complete set [0, 1, 2, 3, 4, 5, 7], then [6] absorbed
ok    S_8: the full closure (computed independently of Table 3) is K_8
ok    Table 2: S_9 has 16 edges
ok    Table 3: certificates of S_9 as printed: 12 listed steps, complete set [0, 1, 2, 3, 4, 5, 7], then [6, 8] absorbed
ok    S_9: the full closure (computed independently of Table 3) is K_9
ok    Table 2: S_11 has 19 edges
ok    Table 3: certificates of S_11 as printed: 15 listed steps, complete set [0, 1, 2, 3, 4, 6, 7], then [5, 8, 9, 10] absorbed
ok    S_11: the full closure (computed independently of Table 3) is K_11
ok    S_9 restricted to {0..7}: 14 edges, closure not complete
ok    Corollary 2.3 instance: S_9 plus a vertex joined to 0, 1 percolates (18 edges)
ok    Corollary 2.3 instance: S_11 plus a vertex joined to 0, 1 percolates (21 edges)
ok    other seed for n = 10 (18 edges) percolates
ok    other seed for n = 12 (21 edges) percolates
ok    Section 3: the explicit graph for n = 13 (23 edges) percolates
ok    graphs with gadgets, 13 <= n <= 24: percolate with floor((7n+2)/4) edges, every step certified
ok    Proposition 5.1 / controls: n=8 k=3: 560 sets with (R1), 0 work
ok    Proposition 5.1 / controls: n=8 k=4: 1820 sets with (R1), 768 work
ok    Proposition 5.1 / controls: n=9 k=4: 4326 sets with (R1), 0 work
ok    Proposition 5.1 / controls: n=9 k=5: 23576 sets with (R1), 6864 work
ok    Proposition 5.1 / controls: n=10 k=6: 272048 sets with (R1), 0 work
ALL CHECKS PASSED
real 78.46
user 78.04
sys 0.30
