PASS  S3: (A,B) = (-conj w, conj z) satisfies conj(z) A + conj(w) B = 0
PASS  S3: X0 and J X0 are orthogonal to p and to ip (tangent and in ker theta)
PASS  S3: |X0|^2 = |JX0|^2 = |p|^2 and <X0, JX0> = 0 (so (X0, JX0) is a basis of H_p on S^3)
PASS  S3: J = multiplication by i is orthogonal and J^2 = -1
PASS  S3: d theta computed from the coefficients equals 2 (dx1^dy1 + dx2^dy2)
PASS  S3: Levi form d theta(X, JX) = 2 (alpha^2 + beta^2) |p|^2 for every X = alpha X0 + beta JX0 in H_p
PASS  S3: sigma is orthogonal (Euclidean isometry), sigma^2 = 1, det sigma = 1
PASS  S3: sigma preserves |p|^2 (maps S^3 onto S^3)
PASS  S3: sigma anticommutes with J (sigma(iv) = -i sigma(v))
PASS  S3: sigma maps X0(p), JX0(p) into H_{sigma p} (orthogonal to sigma p and i sigma p)
PASS  S3: sigma^* theta = -theta on all of R^4 (theta_{sigma p}(sigma v) = -theta_p(v))
PASS  S3: on H, d sigma(J X) = -J d sigma(X) for X = X0 and X = J X0 (anti-CR)
PASS  S3 (complex route): sigma_* maps T^{1,0}_p S^3 into T^{0,1}_{sigma p} S^3 (z' A + w' B = 0)
PASS  Hopf: phi^* theta = cos^2(a) db + sin^2(a) dc
PASS  Hopf: sigma o phi(a, b, c) = phi(a, -b, -c)
PASS  Hopf: (a,b,c) -> (a,-b,-c) pulls cos^2 a db + sin^2 a dc back to its negative (u = -1)
PASS  control S3: (conj z, w) maps the horizontal vector X0(p), p=(3/5,0,0,4/5), to a vector with theta = -24/25 != 0
PASS  control S3: theta_{s(p)}(s X0(p)) = -2*(x1*y2 + x2*y1) is not identically zero
PASS  Heis: theta(X) = theta(Y) = 0
PASS  Heis: dPhi(Y) = i dPhi(X) in C^2, i.e. the structure induced from the Siegel domain has JX = Y
PASS  Heis: Phi maps into the boundary Im w = |z|^2
PASS  Heis: d theta = 4 dx ^ dy
PASS  Heis: Levi form d theta(X, JX) = 4 (alpha^2 + beta^2) for every horizontal X (theta adapted)
PASS  Heis: tau^* theta = -theta (u = -1)
PASS  Heis: d tau maps H into H and has frame matrix diag(1, -1) (Euclidean isometry of (H, g))
PASS  Heis: tau is anti-CR and not CR
PASS  Heis: Phi o tau = (conj z, -conj w) o Phi
PASS  Siegel inversion: Im w' = |z'|^2 on the image (maps the boundary to the boundary)
PASS  Siegel inversion: F^* theta = u theta with u = 1/(t**2 + x**4 + 2*x**2*y**2 + y**4) = 1/|w|^2 > 0
PASS  Siegel inversion: dF maps H into H, and dF is J-linear on H (CR), not anti-CR
PASS  Siegel inversion: frame matrix is |w|^{-1} times a rotation (similarity factor 1/|w|)
PASS  tau o inversion: u = -1/(t**2 + x**4 + 2*x**2*y**2 + y**4) < 0, anti-CR, not CR (sign rule of Theorem 1.1(3))
PASS  control Heis: (2x, y, 2t) is contact with u = 2, frame matrix [2, 0, 0, 1], neither CR nor anti-CR, not a similarity
PASS  Remark 4.4: A^{-1} R A preserves theta, frame matrix [[0,-1/4],[4,0]], neither CR nor anti-CR
PASS  Remark 4.4: A^* g has Gram matrix diag(4, 1/4) in (X, Y) (not Hermitian) and F preserves it
PASS  Lemma 4.1: for all 6560 nonzero integer matrices with entries in [-4,4]: similarity <=> commutes or anticommutes with J, never both (160 similarities)

36 checks, 36 passed, 0 failed
ALL CHECKS PASSED
