================ S2 ================
PASS S2 1.0 V is A-orthogonal to P
PASS S2 1.1 rho_P o rho_P = id
PASS S2 1.2 rho_P(P) = P
PASS S2 1.3 rho_P(V) = -V on the A-polar plane of P
PASS S2 1.4 <rho X, rho Y>_A = <X, Y>_A (A-isometry)
PASS S2 1.5 <rho X, P>_A = <X, P>_A (equal distance to P)
PASS S2 1.6 rho_P(aP + bV) = aP - bV
PASS S2 1.7 frames: <P,P>_A = eps, <V,V>_A = <N,N>_A = 1, pairwise A-orthogonal (3 rational frames)
PASS S2 1.8 x = cP + sV lies on Sigma~ = {<x,x>_A = eps}
PASS S2 1.9 x has unit speed in the arc-length parameter t(theta)
PASS S2 1.10 rho_P(x(theta)) = x(-theta), i.e. t -> -t
PASS S2 2.1 chart(rho_P(P0 + t w)) = P0 + mu(t) w, mu = -c t/(c + b t)
PASS S2 2.2 mu(mu(t)) = t, mu(0) = 0, mu'(0) = -1
PASS S2 2.3 Q(P0 + mu w)(c + b t)^2 = c^2 Q(P0 + t w): mu preserves the pair L cap I
PASS S2 2.4 second fixed point t* = -2c/b; Q(P0 + t* w) b^2 = c(4ac - b^2) (on I iff L tangent to I)
PASS S2 2.5 [rho_P] fixes every line through P0: det(P, Y, rho_P Y) = 0
PASS S2 2.6 [rho_P] fixes the polar line of P0 pointwise
PASS S2 2.7 equal distance: cos^2 d (S2) / cosh^2 d (H2) to P0 agree at P0 + t w and P0 + mu w
PASS S2 3.1 <B rho x, rho x> - <Bx,x> = -4ab<BP,V> on W_P (every symmetric B)
PASS S2 3.2 general conic C through P0 tangent to w: C(P0) = 0 and dC(P0).w = 0
PASS S2 3.3 (C - lambda Q)(P0 + mu w)(c + b t)^2 = c^2 (C - lambda Q)(P0 + t w) for all lambda
PASS S2 3.4 C/Q is invariant: (C/Q)(P0 + mu w) = (C/Q)(P0 + t w)
PASS S2 3.5 geodesic circle of radius r about the pole: x1^2 + x2^2 - k x3^2 = 0, k = (tan r)^2 resp. (tanh r)^2
PASS S2 3.6 geodesic circle with centre c: <rho_P x, c>_A = <x, c>_A on W_P (P on the circle, V its tangent)
PASS S2 4.0 rational parametrisation of Sigma~ (for H2 both sheets)
PASS S2 4.1 F = F+ + F-, F+ even, F- odd
PASS S2 4.2 homogenisations of F+ (degree 4) and (F-)^2 (degree 10) are homogeneous
PASS S2 4.3 they agree with F+ and (F-)^2 on Sigma~
PASS S2 4.4 R+ = G+/s^m and R- = G-/s^m' are 0-homogeneous (rational functions on RP^2, poles on I)
PASS S2 4.5 conic, integral C + 3C^2 + (s-1)(x1 + x2x3 + x1x2x3): R+ invariant under mu on tangent lines (3 points)
PASS S2 4.6 geodesic circle, odd integral L + 2L^3 + (s-1)(x1 + x2x3): R- = (F-)^2 descended is invariant and non-constant on tangent lines (3 points)
PASS S2 6.1 control: the Euclidean central symmetry t -> -t of the chart does not preserve C/Q
PASS S2 6.2 control: 1.01 mu(t) violates the equal-distance identity
PASS S2 6.3 control: 2 eps <x,P>_A P - x is the point reflection on Sigma (P normalised), 2 (-eps) <x,P>_A P - x is not
================ H2 ================
PASS H2 1.0 V is A-orthogonal to P
PASS H2 1.1 rho_P o rho_P = id
PASS H2 1.2 rho_P(P) = P
PASS H2 1.3 rho_P(V) = -V on the A-polar plane of P
PASS H2 1.4 <rho X, rho Y>_A = <X, Y>_A (A-isometry)
PASS H2 1.5 <rho X, P>_A = <X, P>_A (equal distance to P)
PASS H2 1.6 rho_P(aP + bV) = aP - bV
PASS H2 1.7 frames: <P,P>_A = eps, <V,V>_A = <N,N>_A = 1, pairwise A-orthogonal (3 rational frames)
PASS H2 1.8 x = cP + sV lies on Sigma~ = {<x,x>_A = eps}
PASS H2 1.9 x has unit speed in the arc-length parameter t(theta)
PASS H2 1.10 rho_P(x(theta)) = x(-theta), i.e. t -> -t
PASS H2 2.1 chart(rho_P(P0 + t w)) = P0 + mu(t) w, mu = -c t/(c + b t)
PASS H2 2.2 mu(mu(t)) = t, mu(0) = 0, mu'(0) = -1
PASS H2 2.3 Q(P0 + mu w)(c + b t)^2 = c^2 Q(P0 + t w): mu preserves the pair L cap I
PASS H2 2.4 second fixed point t* = -2c/b; Q(P0 + t* w) b^2 = c(4ac - b^2) (on I iff L tangent to I)
PASS H2 2.5 [rho_P] fixes every line through P0: det(P, Y, rho_P Y) = 0
PASS H2 2.6 [rho_P] fixes the polar line of P0 pointwise
PASS H2 2.7 equal distance: cos^2 d (S2) / cosh^2 d (H2) to P0 agree at P0 + t w and P0 + mu w
PASS H2 3.1 <B rho x, rho x> - <Bx,x> = -4ab<BP,V> on W_P (every symmetric B)
PASS H2 3.2 general conic C through P0 tangent to w: C(P0) = 0 and dC(P0).w = 0
PASS H2 3.3 (C - lambda Q)(P0 + mu w)(c + b t)^2 = c^2 (C - lambda Q)(P0 + t w) for all lambda
PASS H2 3.4 C/Q is invariant: (C/Q)(P0 + mu w) = (C/Q)(P0 + t w)
PASS H2 3.5 geodesic circle of radius r about the pole: x1^2 + x2^2 - k x3^2 = 0, k = (tan r)^2 resp. (tanh r)^2
PASS H2 3.6 geodesic circle with centre c: <rho_P x, c>_A = <x, c>_A on W_P (P on the circle, V its tangent)
PASS H2 4.0 rational parametrisation of Sigma~ (for H2 both sheets)
PASS H2 4.1 F = F+ + F-, F+ even, F- odd
PASS H2 4.2 homogenisations of F+ (degree 4) and (F-)^2 (degree 10) are homogeneous
PASS H2 4.3 they agree with F+ and (F-)^2 on Sigma~
PASS H2 4.4 R+ = G+/s^m and R- = G-/s^m' are 0-homogeneous (rational functions on RP^2, poles on I)
PASS H2 4.5 conic, integral C + 3C^2 + (s-1)(x1 + x2x3 + x1x2x3): R+ invariant under mu on tangent lines (3 points)
PASS H2 4.6 geodesic circle, odd integral L + 2L^3 + (s-1)(x1 + x2x3): R- = (F-)^2 descended is invariant and non-constant on tangent lines (3 points)
PASS H2 6.1 control: the Euclidean central symmetry t -> -t of the chart does not preserve C/Q
PASS H2 6.2 control: 1.01 mu(t) violates the equal-distance identity
PASS H2 6.3 control: 2 eps <x,P>_A P - x is the point reflection on Sigma (P normalised), 2 (-eps) <x,P>_A P - x is not
================ S2 duality ================
PASS S2 5.1 Q x R(v) = rho_P(Q x v) for all v orthogonal to Q = P x V (P orthogonal to V)
PASS S2 5.2 (P x V) x V = <P,V>V - <V,V>P and P x (P x V) = <P,V>P - <P,P>V (= -P, -V for orthonormal P, V)
PASS S2 5.3 the moment q x dq/dt equals P x V along the great circle q = cP + sV (3 rational frames)
================
TOTAL: ALL 71 CHECKS PASSED
(running time 4.5 s)
