Part 1: Proposition 5.1 on random rational lattices (exact arithmetic)
[PASS] 240 lattices: w_i = t_i w_1 + u_i with u_i orthogonal to w_1
[PASS] u_2, ..., u_k are linearly independent (they span a lattice in V)
[PASS] iota(sigma, v) = sigma w_1/L + v preserves the product metric
[PASS] the i-th generator acts on R^k/Z w_1 as the translation by w_i

Part 2: the scaled isometry at infinity for m = 1 (symbolic)
[PASS] Psi^*(dsigma^2 + dy_1^2 + dy_2^2) = lambda^2 (dr^2 + F^2 dtau^2 + (r-c)^2 dtheta^2)
[PASS] the circle at infinity has length 2 pi lambda F = L
[PASS] the rotation tau -> tau + alpha becomes sigma -> sigma + L alpha/(2 pi)

Part 3: the constants of Proposition 5.2 (m = 1, a = 1/4, b = 1/2, rho_0 = 9/8)
[PASS] rho_0 = h(b) = 9/8
[PASS] a + (8/9)(b-a)/2 = 13/36
[PASS] rho_0/(2 F_min) = 81/52, so rho_1/|w_1| <= 81/(52 pi)
[PASS] 81/(52 pi) < 1/2 (interval arithmetic for pi) (81/(52 pi) = 0.4958288612)
[PASS] equivalently pi > 81/26 = 3.11538..., which follows from pi > 3.14
[PASS] rigorous enclosure of F (m = 1) lies above 13/36 (F in [0.374175954, 0.374188737], 13/36 = 0.361111...)
[PASS] rho_1/|w_1| = rho_0/(2 pi F) < 1/2 from the rigorous enclosure (rho_1/|w_1| in [0.4785, 0.47851635])
[PASS] so the hypothesis could be weakened to dist(w_{n-1}, H) > 0.9572 |w_1| (the note uses >= |w_1|)

Part 4: the cut-and-paste of Proposition 5.2
[PASS] A = 0.5: A > rho_1, collar half-width eps = (A - rho_1)/2 = 0.01074 > 0
[PASS] A = 0.5001: A > rho_1, collar half-width eps = (A - rho_1)/2 = 0.01079 > 0
[PASS] A = 0.6: A > rho_1, collar half-width eps = (A - rho_1)/2 = 0.06074 > 0
[PASS] A = 1.0: A > rho_1, collar half-width eps = (A - rho_1)/2 = 0.26074 > 0
[PASS] A = 3.7: A > rho_1, collar half-width eps = (A - rho_1)/2 = 1.61074 > 0
[PASS] both collars {| |y_1| - A | < eps} lie in the flat region {|y| > rho_1}
[PASS] T(theta, y_1, y_2) = (theta + s, y_1 + 2A, y_2) maps the collar of {y_1 = -A} onto that of {y_1 = A}, exchanging inner and outer sides
[PASS] dT is the identity matrix, so T preserves dtheta^2 + dy_1^2 + dy_2^2
[PASS] strip {|y_1| <= 1/2} minus the disc {|y| <= rho_1} is connected (grid flood fill; gap 1/2 - rho_1 = 0.0215)
       note: the region {|y_1| <= A, |y_2| <= rho_1} added to the core lies in the ball of radius sqrt(A^2 + rho_1^2) of R^2, so the core of M is compact (no computation needed)
[PASS] 160 random lattices: w_(n-1) = s + (2A) nu with s in H, and (2A)^2 = det Gram(w_1..w_(n-1)) / det Gram(w_1..w_(n-2)), i.e. 2A = dist(w_(n-1), H) = covol(Lambda~)/covol(Lambda)

Part 5: the lattice condition dist(w_{n-1}, span(w_1..w_{n-2})) >= |w_1|
[PASS] Z^(n-1), any n >= 3: distance 1 >= |w_1| = 1, A = 1/2, and A > rho_1 (rigorous bound on rho_1) (A - rho_1 >= 0.02148)
[PASS] square lattice Z^2: min |w|^2 / covol = 1 <= 1, condition holds
[PASS] hexagonal lattice: min |w|^2 / covol = 2/sqrt(3) = 1.1547 > 1, condition FAILS for every basis (ratio = 1.154701)
[PASS] a thin rectangular-type lattice: condition holds (ratio = 0.2000)
[PASS] random rank-2 lattices (Gauss-reduced): the condition holds for some but not all of them (3749 of 3997 Gaussian samples satisfy it; it fails exactly when the reduced shape parameter has imaginary part < 1)

sympy 1.14.0
RUN2 TORUS / TWO ENDS: ALL CHECKS PASSED
