[1] G_k and Ghat_k, 3 <= k <= 200
    G_k: 39 subtrees, 7 in the family (maximal: 2); Ghat_k: 67 subtrees, 9 in the family (maximal: 3)
    Ghat_k maximal family members: [[('q', 'm'), ('q', 'w'), ('q', 'z'), ('s', 'z'), ('t', 'm')], [('p', 'm'), ('p', 'z'), ('q', 'm'), ('q', 'w'), ('s', 'z'), ('t', 'm')], [('p', 'm'), ('p', 'z'), ('q', 'w'), ('q', 'z'), ('s', 'z'), ('t', 'm')]]
    denominators, Table 1 combinations (4 spanning trees each), LP relaxation, values 2(k-1)^2/(2k-3) < k, facet ranks 5 and 6: OK
[2] reduction of Lemma 4.2: H_k(x) = F_k(xbar), xbar in S(G_k), on random points of S(Ghat_k)
    783 random points of S(Ghat_k), 3 <= k <= 8: OK
[3] certificates of Proposition 5.3 (validity via the lifted difference system)
    lifting lemma: 3929 points of S(G_3) in a box, all lifts satisfy every row: OK
    lifting lemma: 929 points of S(Ghat_3) in a box, all lifts satisfy every row: OK
    lifting lemma: 323 points of S(G_4) in a box, all lifts satisfy every row: OK
    36 certificates for F_k >= k on G_k and H_k >= k on Ghat_k (3 <= k <= 20): OK
[4] the normalised K_{2,3} instance N of Remark 5.4 (k = 3)
    788 subtrees, 116 in the family; explicit convex combinations for all of them: OK
    x in LP relaxation, c.x = 223/9; flow certificate proves c.x >= 25 on S(N): OK
    sanity: 1040 (1/3)-integral points of S(N) in a box (l1 = 0): lifts satisfy all rows and c.x >= 25: OK

ALL CHECKS PASSED
