S1a e1 perp p: True
S1b e1 perp ip (theta(e1)=0): True
S1c e2 perp p: True
S1d theta(e2)=0: True
S1e dtheta matrix = 2*(dx1^dy1+dx2^dy2): True
S1f dtheta(e1, J e1) = 2|p|^2 (=2 on S^3): True
S1g dtheta(X,JX) = 2(a^2+b^2)|p|^2: True
S2a sigma preserves |p|^2: True
S2b sigma J = -J sigma: True
S2c sigma e1 in H_sigma(p): True
S2d sigma e2 in H_sigma(p): True
S2e sigma* theta = -theta: True
S2f sigma orthogonal (Euclidean isometry, length of horizontal curves preserved): True
S3 (conj z, w) pullback proportional to theta? (expect False): False
H1a theta(X)=0: True
H1b theta(Y)=0: True
H1c dtheta(X,Y) = 4: True
H1d Re Z = X/2, Im Z = -Y/2 (so J X = Y): True
H1e (d_z + 2i zb d_w) rho = 0: True
H2a tau* theta = -theta: True
H2b dtau X = X(tau p): True
H2c dtau Y = -Y(tau p): True
H3a inversion maps boundary to boundary: True
H3b F* theta = u theta: True
H3c u = 1/|w|^2: True
H3d dF(H) in H': True
H3e dF(JX) = J' dF(X)  [CR]: True
H3f (tau o F)* theta = -u theta (u<0 case): True
H3g tau o F anti-CR: dF(JX) = -J' dF(X): True
H4a A* theta = 2 theta (contact): True
H4b A neither CR nor anti-CR (expect True): True
L41a similarities commute or anticommute with J, never both: True
L41b invertible integer B: (similarity) <=> (commutes or anticommutes with J): True
