== (1) Lemma 2.1
PASS m(t).P(t+Delta) = 1
PASS m(t).P(t-Delta) = 1
PASS n(t+Delta).V(t) = 1
PASS n(t-Delta).V(t) = 1
PASS tangency (alpha-lam) p^2 + (beta-lam) q^2 = 1
PASS eq. (c0d0): d0^2/alpha - 1/beta = -k^2/beta
== (2) Lemma 2.2(a)
PASS criterion: (nv.nv) m2 x Ref(m1) = criterion
PASS T is orthogonal to n(u)
PASS c0 D m(u+Delta).T = s0 (X - Y)
PASS c0 D m(u-Delta).T = s0 (X + Y)
PASS c0 D m(u+Delta).n = U + W
PASS c0 D m(u-Delta).n = U - W
PASS d0^2 s^2/alpha + c^2/beta = e^2/beta
PASS XU + YW = 0
PASS criterion for m(u+-Delta) vanishes
== (3) Lemma 2.3
PASS m.m = dn^2 t/(beta c0^2)
PASS n.n = (alpha - (alpha-beta) sn^2)/(alpha beta)
PASS sn^2(K+iK'+-Delta) = alpha/(alpha-beta)
== (4) Lemma 3.1 for generic complex vectors (polynomial identity over Q)
PASS Lemma 3.1 identity, N = 3
PASS Lemma 3.1 identity, N = 4
PASS Lemma 3.1 identity, N = 5
PASS y.z = (y+ z- + y- z+)/2
PASS y x z = (y- z+ - y+ z-)/(2i)
PASS y.y = y+ y-
PASS N = 4: x_{i+2} = -x_i gives w_{i+1} = w_i and c2 = 0
== (5) the N = 4 rhombus (symbolic a, b and M)
PASS rhombus vertices on the ellipse
PASS rhombus sides tangent to the confocal ellipse lambda = a^2 b^2/(a^2+b^2)
PASS reflection law at the four vertices (reflected direction = next direction)
PASS A = 2ab
PASS A_M independent of M
PASS A*A_M = 8 a^4 b^4/(a^2+b^2)^2
PASS feet from O as stated (divided by a^2+b^2)
PASS rectangle of feet: area 4 a^3 b^3/(a^2+b^2)^2, positively oriented
PASS outer polygon of the rhombus: A' = 4ab and A'_M = A'/2 for all M
== (6) Lemma 5.1: r x P(iK'+h)
PASS r x P(iK'+h) = i a b (dn h - 1)/(k^2 sn h)
== (7) coset and index arithmetic, N <= 400, 1 <= tau < N/2, gcd(tau, N) = 1 (K = 1)
families checked: 24338; discrepancies: []
PASS coset and index arithmetic
== (8) negative controls: deliberately false identities must be rejected
PASS rejects XU - YW = 0
PASS rejects m.m = dn^2/(alpha c0^2)
PASS rejects m(t).P(t+2 Delta) = 1 (wrong shift)
PASS rejects Lemma 3.1 with 1/3 instead of 1/4
PASS rejects A*A_M = 8 a^4 b^4/(a^2+b^2) for the rhombus
PASS rejects tangency for a wrong caustic

TOTAL failures: 0 []
