Negative control of run2_certificate.py (not part of the checks): sigma replaced by diag(1,-1,1,1) and tau by (x,-y,t) (two-line sed edit of a scratch copy).
FAIL  S3: sigma is orthogonal (Euclidean isometry), sigma^2 = 1, det sigma = 1
FAIL  S3: sigma anticommutes with J (sigma(iv) = -i sigma(v))
FAIL  S3: sigma maps X0(p), JX0(p) into H_{sigma p} (orthogonal to sigma p and i sigma p)
FAIL  S3: sigma^* theta = -theta on all of R^4 (theta_{sigma p}(sigma v) = -theta_p(v))
FAIL  S3: on H, d sigma(J X) = -J d sigma(X) for X = X0 and X = J X0 (anti-CR)
FAIL  Hopf: sigma o phi(a, b, c) = phi(a, -b, -c)
FAIL  Heis: tau^* theta = -theta (u = 1)
FAIL  Heis: d tau maps H into H and has frame matrix diag(1, -1) (Euclidean isometry of (H, g))
FAIL  Heis: Phi o tau = (conj z, -conj w) o Phi
FAIL  tau o inversion: u = -(-t**2 + 3*x**4 + 6*x**2*y**2 + 3*y**4)/(t**2 + x**4 + 2*x**2*y**2 + y**4)**2 < 0, anti-CR, not CR (sign rule of Theorem 1.1(3))
36 checks, 26 passed, 10 failed
SOME CHECKS FAILED
