r2_chain.py -- independent verification run 2, OWR-14299911-020 (the inequalities, exactly)
[K] constants and exact identities
    c_k = [3, 8, 19, 44, 101, 230]; 4c_k+1 = [13, 33, 77, 177, 405, 921]
    Lemma 3.2: (m-1)^k < n <= m^k <= 2^k n, M^k <= 2^(k(k-1)) n^(k-1) and the final bound: 80000 cases (2<=k<=7)
    Proposition 4.1 counting inequalities: 2392 cases (1<=k<=8, 2<=n<=300)
[E] Lemma 3.1 (Euler tour, as built in the proof)
    all 18249 labelled trees with at most 7 vertices (Pruefer codes) and 300 hulls in random trees: domain 2h-1, surjective, steps equal or adjacent, 1-Lipschitz
[S] Lemma 3.2 (strip walk of the proof), exact arithmetic
    6000 point sets (k=1..5, n<=400, L<=5000; uniform/corner/one-cell/lattice/diagonal/equal; cells in lexicographic or random order): OK; largest length/bound by k: 1: 0.500, 2: 0.309, 3: 0.173, 4: 0.092, 5: 0.046
[P] Proposition 3.3: the walk of the proof and the inequality, with factors of finite diameter
    6000 random triples, (d,k) in [(1, 1), (2, 2), (3, 3), (4, 4), (2, 1), (3, 1), (3, 2), (4, 1), (4, 2), (4, 3), (5, 2), (5, 3)];
    first k factors: random trees with 6-40 vertices; the other d-k: stars, short paths, brooms, small random
    trees (D = sum of their diameters); in a quarter of the cases the points of F sit at far-apart vertices
    of the factors of finite diameter
    every link checked (preimages, ell <= 2 sigma, strip bound, inequality (4), TS <= walk <= strip + (N+1)D,
    TS <= 4c_k N^(1-1/k) sigma + 2ND, AM-GM, final inequality in exact integer form): OK
    largest (TS+N)^(k/(2k-1))/(TP+N) by (d,k): (1, 1): 1.000, (2, 2): 0.585, (3, 3): 0.459, (4, 4): 0.271, (2, 1): 1.103, (3, 1): 1.182, (3, 2): 0.450, (4, 1): 1.328, (4, 2): 0.481, (4, 3): 0.358, (5, 2): 0.405, (5, 3): 0.358  (the proof allows 4c_k+2D+1 >= 13)
[U] Proposition 4.1: the grid family in k factors of unbounded diameter, with d-k further factors
    k n  L  extra factors        N   TP=2k(n-1)L  TS(x,F,x)  TS>=(N-1)L  TP+N<=(2k+1)n^k  TS+N>=n^(2k-1)
    1 2  1  -                     2     2            2        True        True              True 
    1 3  1  P2                    3     4            4        True        True              True 
    1 5  1  P3,K1,2               5     8            8        True        True              True 
    1 8  1  P5                    8    14           14        True        True              True 
    2 2  2  -                     4     8            8        True        True              True 
    2 2  2  K1,6                  4     8            8        True        True              True 
    2 2  2  broom(2,3),P3         4     8            8        True        True              True 
    2 3  3  -                     9    24           30        True        True              True 
    2 3  3  K1,4                  9    24           30        True        True              True 
    3 2  4  -                     8    24           32        True        True              True 
    3 2  4  P2                    8    24           32        True        True              True 
    2 4  4  -                    16    48           64        True        True              True 
    2 4  4  P2                   16    48           64        True        True              True 
    1 10  1  P4,P3                10    18           18        True        True              True 
    4 2  8  broom(2,3)           16    64          128        True        True              True 
    exponent test: (2k+1)n^k / n^((2k-1)(alpha0+0.02)) at n = 2^10, 2^20, 2^30 decreases to 0 for k = 1..4: OK
[B] Theorem 1.2(b): all factors of finite diameter, D = sum of the diameters
    1500 random triples in products of 1-3 trees of finite diameter: TS <= (N+1)D, TS+N <= (2D+1)(TP+N), and TS <= TP for F empty: OK
[R] Remark 5.1: the direct walk in T x K (K of diameter D)
    1200 random triples: the walk visits F and ends at y, length <= 3(|H_1|-1) + D(|F|+1), TS <= (3/2)TP + D(|F|+1): OK
[H] hill climbing on (TS+N)^(k/(2k-1))/(TP+N) with factors of finite diameter (sanity check)
    largest ratio found by (d,k): (2, 1): 1.129, (3, 1): 1.379, (3, 2): 0.367, (4, 2): 0.309 (the proof allows at least 13)
TOTAL: 295262 checks, 0 failures (running time 7.7 s)
ALL CHECKS PASSED
