A  Sections 1 and 2: coordinates, diagonals, cylinders, twists
  ok   (1), (2): |X_{k+1}| = lambda_k, arg X_{k+1} = (n-2-k) pi/n, X_2 = xi + (lambda^2-1) eta, X_{n-2} = eta + (lambda^2-1) xi, n = 3..60
  ok   Lemma 2.4: K(delta_k) = k for 0 <= k <= n-2, n = 3..60
  ok   Lemma 2.8: circumference lambda*lambda_{j-2}, height sin((j-1) pi/n), modulus 2 cot(pi/n) for all 20501 strips, n = 3..40
  ok   Lemma 8.11: T_1 T = -R_{2 pi/n}, n = 3..60
B  Definition 1.1, Lemma 2.3, Lemma 7.1 on all reachable points of radius <= 20, n = 4..12 (exact)
  ok   1899 reachable points: 0 <= alpha <= omega and 2 pi/n <= beta <= pi
  ok   the rule on the parity of N, and formulas (5), (6) with the index s of the end point in the last polygon
  ok   the type of Definition 1.1 (computed from alpha, beta, N) equals the type of the program reach.py
  ok   Lemma 7.1 and (3): type A_0 <=> a side, or N even and last polygon = B - P_0; then B/2 is the midpoint of the middle side
C  Theorems B and C on the reachable points of radius <= 6, n = 4..12 (exact tracer)
  ok   Theorem B: 1526 instances (point, l, eps): the short trajectory of slope l pi/n + eps alpha exists and has type A_(eps k - l)
  ok   Theorem C: in all these instances the lengths are in the ratio sin((k+1) pi/n) : sin((k'+1) pi/n), exactly
D  Theorem D, Remark 4.2, Theorem E on all pairs with det = S of radius <= 12, n = 5..9 (exact)
  ok   Remark 4.2: the 377 pairs of reachable points with det(u,v) = S have the types (A_0,A_0), (A_1,A_0) or (A_0,A_{n-3})
  ok   Theorem D: a pair spans a reachable n-gon iff it is unitary; 125 reachable n-gons, all with the vertex types A_0, A_1, ..., A_{n-3}, A_0; v_2 and v_{n-2} reachable implies all reachable
  ok   Theorem E(a),(b): on 66 lines through unitary pairs the reachable points of length <= 19.5 are exactly the 496 predicted points, with the predicted types
E  Theorem F: formulas of Lemma 6.1 and of the proof of (c); the point w_n; the printed Conjecture 2.5
  ok   all formulas of Lemma 6.1, of Steps 1 and 2 of the proof of Theorem D, and of the proof of Theorem F(c), n = 5..60 (floating point)
  ok   w_n = 2 + 3 zeta + zeta^2 is reachable of type A_{n-3} with three segments, and X_2 has type A_1, n = 5..12 (exact tracer)
  ok   Theorem E(c), n = 6..12: lambda and lambda+1 are not in Lambda, lambda^2 is; for n = 7, 9, 11 the points xi + (lambda+1) eta and xi + lambda eta are not reachable and xi + lambda^2 eta is (exact tracer)
F  Example 6.2: the hexagon with the formulas of the source
  ok   31 reachable hexagons with v_1, v_5 in [0,14]^2: the vertex types are A_0, A_1, A_2, A_3, A_0
  ok   X_2 = (1,2) is a vertex of exactly one of them, (4,5) and (5,4) of none (for these points the search is exhaustive: coordinates of v_1, v_5 are bounded by those of the point, or the type excludes the position)
  ok   (4,5) is reachable of type A_1, (5,4) of type A_3, (1,2) of type A_1
  ok   the description of the source for n = 6 agrees with the exact enumeration: 215 reachable points of radius <= 20, 0 mismatches
G  Lemma 7.2: half-turns of the dodecahedron (exact, see dodecahedron_halfturns.py)
  ok   for all 20 vertices v the 15 distances d(v, h(v)) are 1 (3 times), 3 (6 times), 4 (3 times), 5 (3 times); the table of the proof is reproduced
H  Proposition 8.2, Table 3, Remark 8.4: a floating-point billiard in the n-gon
  ok   Proposition 8.2 for n = 5, 7, ..., 45: 504 trajectories; two segments (one for the midpoint), length l_j, rotation r^(-4j), factor n/gcd(n,j)
  ok   Table 3 (n = 15) as printed
  ok   Corollary 8.3: gcd of the factors n/gcd(n,j) is 1 and d_1 = n for n = 15, 21, 33, 35, 39, 45; it is > 1 for the prime powers 5, 7, 9, 11, 13, 25, 27, 49
  ok   Remark 8.4(a), n = 6, 8, 10, 12: the n-gon through the midpoints has a one-segment preclosed piece and the factor n; its neighbours two segments and n/2
I  Lemmas 8.8 to 8.10 for odd n <= 61 (integers), Theorem H(a) for n = 6, 8, 10, 12 (floating-point billiard)
  ok   Lemma 8.8(b)-(d), Lemma 8.9 with the sums (19), rot(c_j) = 4j, and Lemma 8.10(c) (orbit of (4,-4) = all primitive pairs), odd n = 5..61
  ok   Theorem H(a): 708 closed trajectories for n = 6, 8, 10, 12 with an even number of segments in the simple preclosed piece: the factor divides n/2
J  Theorem H(b) against the floating-point billiard: words in the twists, n = 9, 15
  ok   for 20 words and n = 9, 15: the bands in the direction D psi (1,0) have the m lengths c l_j and the factors n/gcd(n, alpha j), with (alpha, beta) computed by the rule of Lemma 8.10(b) with one sign eps = [-1] for all words
K  The tables and numbers of the note against the recorded outputs of the package
  ok   Table 2: the exact enumeration of the original program
  ok   Table 2: the same twelve numbers in verification run B
  ok   Section 7.4: the facts on the census (bounds 119.22 and 120.86, 655, 18, 3752, variants)
  ok   Section 7.4: N(L) for L = 60, ..., 130 and the quotients N(L)/L^2
  ok   Remark 7.4: the numbers of witness_check_output.txt
  ok   Remark 7.4(b): t_8 = 0.584, sums between 0.976 and 1.192
  ok   Remark 7.4(d): 6875 points (n = 4) and 7605 points (n = 6) of radius <= 120 agree with the descriptions of the source (run A)
  ok   Table 4: the numbers of classes for n = 9, 15, 21, 25, 27, 45 (run B); in every class m bands, lengths proportional to sin(2j pi/n), factors n/gcd(n, alpha j)
  ok   Section 8.7: 2407 classes for 14 odd values of n in run B
  ok   Table 4: the factors n'/gcd(n',j), their greatest common divisors and the column 'a quotient is n'
  ok   Table 5: the factors of the bands and the numbers of classes for n = 6, 8, 9, 10, 12 (run B)
  ok   Table 5: the computed ratios of the simple preclosed lengths are those of the source
  ok   the original program: the same patterns for n = 6, 8, 9, 10, 12, and the factors 15, 15, 5, 15, 3, 5, 15 for n = 15
  ok   Remark 6.3: n = 5..12, X_2 on exactly one reachable n-gon; of the points of type != A_0 and length <= 9 between 37 and 54 per cent on none, the others on one
  ok   Remark 6.3: the shortest points on no reachable n-gon have three segments
  ok   run A: n = 5, radius 150: 11637 reachable points, 1421 reachable pentagons, no failure
L  Veech's formulas (Section 8.5 of the note) against the factors found by direct unfolding (run B)
  ok   odd n = 9, 15, 21, 25, 27, 45: formula (17), over all first rows (a, b), gives exactly the patterns n'/gcd(n', j), n' | n, and every pattern found by run B is one of them
  ok   even n = 6, 8, 10, 12: the formulas of [Ve92, (8.13), (8.15)], as transcribed, give exactly the factors of Table 5 (vertical direction of Veech = class 'even' of the source, direction of a side = class 'odd')
TOTAL failures: 0   (9 s)
