== [1] the sphere S^3 in C^2 = R^4, coordinates (x1, y1, x2, y2)
PASS  J0^2 = -I
PASS  e1, J0 e1 orthogonal to p and to J0 p (they span H_p)
PASS  |e1|^2 = |J0 e1|^2 = |p|^2
PASS  theta = <J0 p, dp> has d theta = 2(dx1^dy1 + dx2^dy2)
PASS  Levi form: d theta(v, J0 v) = 2|v|^2 for all v (positive on H, theta adapted)
PASS  d theta(e1, J0 e1) = 2|p|^2
PASS  sigma orthogonal (S^T S = I)
PASS  sigma anticommutes with J0 (S J0 = -J0 S)
PASS  d sigma maps H_p onto H_sigma(p)
PASS  sigma^* theta = -theta
PASS  det sigma = 1 and sigma(p) is the normal at sigma(p): sigma preserves the orientation of S^3
      non-example (z,w) -> (conj z, w) at p = (3/5, 0, 0, 4/5): e1(p) = ['0', '4/5', '3/5', '0']  theta(image of e1(p)) = -24/25
PASS  non-example: p on S^3, e1(p) in H_p, image not in H (value -24/25)
== [2] the Heisenberg group R^3, theta = dt + 2(x dy - y dx)
PASS  theta(X) = theta(Y) = 0
PASS  d theta = 4 dx^dy
PASS  d theta(X, JX) = d theta(X, Y) = 4 > 0 (theta adapted)
PASS  [X, Y] = -4 d_t, so theta([X, Y]) = -d theta(X, Y) != 0 (bracket generating)
PASS  Siegel boundary: d Phi(Y) = J0 d Phi(X), i.e. the induced CR structure has J X = Y
PASS  d Phi(X), d Phi(Y) tangent to the boundary {rho = 0}
PASS  Z = d_z + i conj(z) d_t = (X - iY)/2
PASS  tau: d tau X = X o tau, d tau Y = -Y o tau (anti-CR, maps (X, Y) to (X, -Y))
PASS  tau^* theta = -theta (u = -1)
PASS  det d tau = 1 (tau preserves the orientation of R^3)
== [3] the sign rule of Theorem 1.1(3) on polynomial maps of the Heisenberg group
PASS  dilation (2x, 2y, 4t): frame matrix and F^* theta = 4 theta; CR = True, anti-CR = False; CR <=> u > 0
PASS  rotation by (3/5, 4/5): frame matrix and F^* theta = 1 theta; CR = True, anti-CR = False; CR <=> u > 0
PASS  tau o dilation: frame matrix and F^* theta = -4 theta; CR = False, anti-CR = True; CR <=> u > 0
PASS  tau o rotation: frame matrix and F^* theta = -1 theta; CR = False, anti-CR = True; CR <=> u > 0
== [4] Lemma 4.1 for all nonzero integer 2x2 matrices with entries in [-3, 3]
      2400 matrices, 96 similarities
PASS  similarity <=> (AJ = JA or AJ = -JA), and never both
== [5] Remark 4.4: a non-Hermitian sub-Riemannian metric
PASS  A = (2x, y/2, t): d A X = 2 X o A, d A Y = (1/2) Y o A, A^* theta = theta
PASS  R = rotation by pi/2: d R X = Y o R, d R Y = -X o R, R^* theta = theta
PASS  dF = dA^{-1} dR dA = [[0, -1/4], [4, 0]] in the frame (X, Y)
PASS  F preserves A^* g (dF^T G dF = G), so F is an isometry for A^* g
PASS  F is CR for J_A = dA^{-1} J dA, and A^* g is Hermitian for J_A
PASS  dF is not a similarity for g, and neither commutes nor anticommutes with J
== 33 of 33 checks passed
ALL CHECKS PASSED
