== Part 1: Lemma 2.1(a),(b) ==
PASS S2 rho o rho = id
PASS S2 rho is an A-isometry
PASS S2 rho fixes P
PASS S2 rho = -1 on P^perp
PASS S2 <rho X, P> = <X, P>
PASS S2 rho(aP + bV) = aP - bV for V in P^perp
PASS S2 frame 1/3,-2/7,1/5: L^T A L = A
PASS S2 frame: <P,P> = eps, <V,V> = 1, <P,V> = 0
PASS S2 frame: geodesic x(t) on Sigma~
PASS S2 frame: unit speed
PASS S2 frame: rho_P(x(t)) = x(-t)
PASS S2 frame 2/9,1/4,-3/11: L^T A L = A
PASS S2 frame: <P,P> = eps, <V,V> = 1, <P,V> = 0
PASS S2 frame: geodesic x(t) on Sigma~
PASS S2 frame: unit speed
PASS S2 frame: rho_P(x(t)) = x(-t)
PASS H2 rho o rho = id
PASS H2 rho is an A-isometry
PASS H2 rho fixes P
PASS H2 rho = -1 on P^perp
PASS H2 <rho X, P> = <X, P>
PASS H2 rho(aP + bV) = aP - bV for V in P^perp
PASS H2 frame 1/3,-2/7,1/5: L^T A L = A
PASS H2 frame: <P,P> = eps, <V,V> = 1, <P,V> = 0
PASS H2 frame: geodesic x(t) on Sigma~
PASS H2 frame: unit speed
PASS H2 frame: rho_P(x(t)) = x(-t)
PASS H2 frame: rho_P maps sample points of H2 into H2
PASS H2 frame 2/9,1/4,-3/11: L^T A L = A
PASS H2 frame: <P,P> = eps, <V,V> = 1, <P,V> = 0
PASS H2 frame: geodesic x(t) on Sigma~
PASS H2 frame: unit speed
PASS H2 frame: rho_P(x(t)) = x(-t)
PASS H2 frame: rho_P maps sample points of H2 into H2
== Part 2: Lemma 2.1(c), the I-angular symmetry, over C ==
PASS S2 rho^_C o rho^_C = <C,C>^2 id
PASS S2 rho^_C(C) = <C,C> C
PASS S2 <rho^ y, rho^ y> = <C,C>^2 <y,y>
PASS S2 every line through [C] is invariant: det(C, y, rho^ y) = 0
PASS S2 polar line of [C] fixed pointwise: rho^(y) = -<C,C> y on C^perp
PASS S2 no cross term on span(C, y)
PASS S2 rho^(aC + by) = <C,C>(aC - by)
PASS S2 explicit basis of C^perp
PASS S2 tangency point of a line tangent to I is fixed (2 tangent lines)
PASS H2 rho^_C o rho^_C = <C,C>^2 id
PASS H2 rho^_C(C) = <C,C> C
PASS H2 <rho^ y, rho^ y> = <C,C>^2 <y,y>
PASS H2 every line through [C] is invariant: det(C, y, rho^ y) = 0
PASS H2 polar line of [C] fixed pointwise: rho^(y) = -<C,C> y on C^perp
PASS H2 no cross term on span(C, y)
PASS H2 rho^(aC + by) = <C,C>(aC - by)
PASS H2 explicit basis of C^perp
PASS H2 tangency point of a line tangent to I is fixed (2 tangent lines)
== Part 3: Lemma 2.1(d), the chart identity ==
PASS S2 chart image of rho_P(z0+tw) is z0 + mu(t) w
PASS S2 third coordinate of rho_P(Y) is (c+bt)/c
PASS S2 Q(z0+mu w)(c+bt)^2 = c^2 Q(z0+tw)
PASS S2 mu o mu = id
PASS S2 mu(0) = 0, mu'(0) = -1
PASS S2 mu swaps the two points of the line on I
PASS S2 the swapped pair is harmonic w.r.t. the two fixed points 0 and -2c/b
PASS S2 second fixed point -2c/b lies on the polar line of z0
PASS H2 chart image of rho_P(z0+tw) is z0 + mu(t) w
PASS H2 third coordinate of rho_P(Y) is (c+bt)/c
PASS H2 Q(z0+mu w)(c+bt)^2 = c^2 Q(z0+tw)
PASS H2 mu o mu = id
PASS H2 mu(0) = 0, mu'(0) = -1
PASS H2 mu swaps the two points of the line on I
PASS H2 the swapped pair is harmonic w.r.t. the two fixed points 0 and -2c/b
PASS H2 second fixed point -2c/b lies on the polar line of z0
== Part 4: Lemma 4.1 ==
PASS S2 v(C) = grad f x C is tangent: grad f . v = 0 and C . v = 0
PASS S2 coefficients of H(C, lam C + nu v(C)) homogeneous of degree 3i+(d+2)j
PASS S2 H(C, .) = 0 on the tangent line at every point of the conic (f | coefficients)
PASS S2 same for R = (f+3s)^2/s^2
PASS S2 control: on a cubic the same R is not invariant (division fails)
PASS S2 on {x.x = 0} the vector v(C) vanishes identically (reason for excluding it)
PASS H2 v(C) = grad f x C is tangent: grad f . v = 0 and C . v = 0
PASS H2 coefficients of H(C, lam C + nu v(C)) homogeneous of degree 3i+(d+2)j
PASS H2 H(C, .) = 0 on the tangent line at every point of the conic (f | coefficients)
PASS H2 same for R = (f+3s)^2/s^2
PASS H2 control: on a cubic the same R is not invariant (division fails)
PASS H2 on {x.x = 0} the vector v(C) vanishes identically (reason for excluding it)
== Part 5: Proposition 1.3 ==
PASS S2 <Bx,x> on W_P = a^2<BP,P> + 2ab<BP,V> + b^2<BV,V> (so = b^2<BV,V> on gamma)
PASS S2 pencil identity (C - la Q)(z0+mu w)(c+bt)^2 = c^2 (C - la Q)(z0+tw)
PASS S2 C/Q invariant under mu on the tangent line
PASS S2 <rho_P x, c> - <x,c> = 2(eps<c,P><x,P> - <x,c>)
PASS H2 <Bx,x> on W_P = a^2<BP,P> + 2ab<BP,V> + b^2<BV,V> (so = b^2<BV,V> on gamma)
PASS H2 pencil identity (C - la Q)(z0+mu w)(c+bt)^2 = c^2 (C - la Q)(z0+tw)
PASS H2 C/Q invariant under mu on the tangent line
PASS H2 <rho_P x, c> - <x,c> = 2(eps<c,P><x,P> - <x,c>)
== Part 6: formula (3) and Lemma 3.2 on an example ==
PASS S2 homogenisations are homogeneous (degrees 4, 10)
PASS S2 G~ - G divisible by s - 1
PASS S2 R_+ and R_- invariant under sigma on three tangent lines of the circle
PASS S2 R_+ and R_- take one value each at the three points (constancy on the curve)
PASS S2 R_- is not constant on the tangent line
PASS H2 homogenisations are homogeneous (degrees 4, 10)
PASS H2 G~ - G divisible by s - 1
PASS H2 R_+ and R_- invariant under sigma on three tangent lines of the circle
PASS H2 R_+ and R_- take one value each at the three points (constancy on the curve)
PASS H2 R_- is not constant on the tangent line
== Part 7: Proposition 4.2, duality identities on S^2 ==
PASS frame 1/3: varrho(Q) = Q
PASS frame 1/3: Q x varrho(v) = rho_P(Q x v)
PASS frame 1/3: Q x v lies in W_P
PASS frame 1/3: (P x V)' = -kappa V
PASS frame 1/3: q x q' = P x V along the great circle
PASS frame 1/3: (P x V) x V = -P
PASS frame 5/2: varrho(Q) = Q
PASS frame 5/2: Q x varrho(v) = rho_P(Q x v)
PASS frame 5/2: Q x v lies in W_P
PASS frame 5/2: (P x V)' = -kappa V
PASS frame 5/2: q x q' = P x V along the great circle
PASS frame 5/2: (P x V) x V = -P
== Part 8: controls (must fail) ==
PASS S2 control: central symmetry of the chart does not satisfy the Q-identity
PASS S2 control: 2<x,P>P/<P,P> + x is not an involution
PASS H2 control: central symmetry of the chart does not satisfy the Q-identity
PASS H2 control: 2<x,P>P/<P,P> + x is not an involution

TOTAL: 114 PASS, 0 FAIL
(running time 34.5 s)
