check_note.py -- OWR-14299911-020, the travelling polytope constant of a product of trees
[A] constants and exact identities
    k=1: c_k = 3, C_k = 1/(4c_k+1) = 1/13
    k=2: c_k = 8, C_k = 1/(4c_k+1) = 1/33
    k=3: c_k = 19, C_k = 1/(4c_k+1) = 1/77
    k=4: c_k = 44, C_k = 1/(4c_k+1) = 1/177
    k=5: c_k = 101, C_k = 1/(4c_k+1) = 1/405
    k=6: c_k = 230, C_k = 1/(4c_k+1) = 1/921
    Lemma 3.2: n <= m^k <= 2^k n, M^k <= 2^(k(k-1)) n^(k-1) and the final bound, for 2<=k<=6, n<=20000 (100000 cases)
    Proposition 4.1 counting inequalities for 1<=k<=6, 2<=n<=200 (1194 cases)
    (part done in 0.1 s)
[B] Lemmas 2.1, 2.3, Proposition 2.4, Lemma 2.6(a): literal brute force
    P5: |V|=5, convex sets=15 (= products of subtrees), steps=20, triples=700: OK
    K_{1,4}: |V|=5, convex sets=20 (= products of subtrees), steps=36, triples=700: OK
    P3 x P3: |V|=9, convex sets=36 (= products of subtrees), steps=120, triples=4698: OK
    K_{1,3} x P3: |V|=12, convex sets=66 (= products of subtrees), steps=288, triples=13104: OK
    spider(2,1,1) x P2: |V|=10, convex sets=51 (= products of subtrees), steps=188, triples=6800: OK
    P2 x P2 x P3: |V|=12, convex sets=54 (= products of subtrees), steps=256, triples=13104: OK
    K_{1,3} x K_{1,3}: |V|=16, convex sets=121 (= products of subtrees), steps=690, triples=38144: OK
    P4 x P4: |V|=16, convex sets=100 (= products of subtrees), steps=480, triples=38144: OK
    total 115394 triples; negative control 'TP = hyp' rejected on 115224 of them
    (part done in 1.7 s)
[C] Lemma 3.1 (Euler tour, as built in the proof)
    all 201 trees with at most 10 vertices (up to isomorphism; counts [1, 1, 1, 2, 3, 6, 11, 23, 47, 106]) and 200 random trees with at most 40 vertices: domain 2h-1, surjective, steps equal or adjacent, 1-Lipschitz: OK
    (part done in 0.1 s)
[D] Lemma 3.2 (strip walk), exact rational arithmetic
    1000 point sets (k=1..4, n<=200, uniform/corner/one-cell/lattice): OK; largest ratio length/bound by k: 1: 0.489, 2: 0.285, 3: 0.131, 4: 0.070
    (part done in 0.4 s)
[E] Proposition 3.3: the walk of the proof and the inequality, exact
    1200 random triples in products of d trees, k unbounded-role factors and d-k bounded factors, (d,k) in [(1, 1), (2, 2), (2, 1), (3, 3), (3, 2), (3, 1), (4, 4), (4, 2)]: OK
    largest (TS+N)^(k/(2k-1))/(TP+N) by (d,k): (1, 1): 1.000, (2, 1): 1.150, (2, 2): 0.500, (3, 1): 1.231, (3, 2): 0.500, (3, 3): 0.500, (4, 2): 0.500, (4, 4): 0.398  (the proof allows 4c_k+2D+1 >= 13)
    (part done in 0.3 s)
[F] Proposition 4.1: the grid family on geodesic segments
    k n  L  extra   N   TP  TS(x,F,x)  TP+N <= (2k+1)n^k   TS+N >= n^(2k-1)   literal TP
    1 2  1  0       2   2    2             4 <= 6               4 >= 2           2
    1 3  1  1       3   4    4             7 <= 9               7 >= 3           4
    1 6  1  1       6   10   10           16 <= 18             16 >= 6           10
    2 2  2  0       4   8    8            12 <= 20             12 >= 8           8
    2 2  2  1       4   8    8            12 <= 20             12 >= 8           8
    2 3  3  0       9   24   30           33 <= 45             39 >= 27          24
    2 4  4  0       16  48   64           64 <= 80             80 >= 64          
    3 2  4  0       8   24   32           32 <= 56             40 >= 32          24
    3 2  4  1       8   24   32           32 <= 56             40 >= 32          
    (part done in 0.8 s)
[G] Theorem 1.2(b): TS + N <= (2D+1)(TP + N) when all factors are bounded (D = sum of diameters)
    400 random triples in products of 1-3 bounded trees: OK
    (part done in 0.1 s)
TOTAL: 354889 checks, 0 failures (running time 3.4 s)
ALL CHECKS PASSED
