certificate: pair_A_exact.json sha256 ca6a9b6465c960dfbb6c77e1f95b285b210d5ccefb31a064dcf0cfcc59ba9609
PASS [C1] certificate file is the one recorded in the note
PASS [C1] D has 55 digits and is not a perfect square
PASS [C1] D is the discriminant of the quadratic c2 t^2 + c1 t + c0 of the note
PASS [C1] lambda* is a root of that quadratic, the smaller one (lambda* = 1.127770)
PASS [C1] y = y' = 0, a1, a2 rational as stated, a3 = lambda* (-22/25, -27/100, -22/25)
PASS [C2] P: a1, a2, a3 affinely independent, x and y strictly on opposite sides
PASS [C3] P: no degenerate triangle, no two adjacent faces coplanar (9 edges)
PASS [C4] P: Lemma-1-free embeddedness test, 36 edge/triangle pairs, no violation
PASS [C2] P': a1, a2, a3 affinely independent, x and y strictly on opposite sides
PASS [C3] P': no degenerate triangle, no two adjacent faces coplanar (9 edges)
PASS [C4] P': Lemma-1-free embeddedness test, 36 edge/triangle pairs, no violation
PASS [C5] K has 9 edges and its labelled triangles are coherently oriented
PASS [C5] P and P' induce the same outward orientation (signed volumes of equal sign)
PASS [C6] the two typing methods (Lemma 2 and Lemma 2') agree at all 18 edge instances
PASS [C6] Lemma 2: all 9 interior dihedral angles of P and P' are equal
PASS [C7] Lemma 2' (orientation-free): all 9 interior dihedral angles are equal
      edge y-a1   convex  P: 145.7735974715 deg   P': 145.7735974715 deg
      edge y-a2   convex  P: 32.2559160222 deg   P': 32.2559160222 deg
      edge y-a3   convex  P: 45.9568968578 deg   P': 45.9568968578 deg
      edge x-a1   convex  P: 120.8279275301 deg   P': 120.8279275301 deg
      edge x-a2   convex  P: 27.7621488476 deg   P': 27.7621488476 deg
      edge x-a3   convex  P: 37.9213297766 deg   P': 37.9213297766 deg
      edge a1-a2  convex  P: 71.6166597193 deg   P': 71.6166597193 deg
      edge a1-a3  convex  P: 38.7133075619 deg   P': 38.7133075619 deg
      edge a2-a3  reflex  P: 273.8238518533 deg   P': 273.8238518533 deg
PASS [C7] a2-a3 is the only reflex edge, in P and in P' (both nonconvex)
PASS [C8] exactly 12 of the 18 face angles differ; the 6 at x and y are equal
      face y-a1-a3   at y    47.9368 vs   47.9368 deg
      face y-a1-a3   at a1   39.8173 vs   55.5007 deg
      face y-a1-a3   at a3   92.2459 vs   76.5626 deg
      face y-a2-a1   at y    90.7675 vs   90.7675 deg
      face y-a2-a1   at a1   29.9066 vs   13.1467 deg
      face y-a2-a1   at a2   59.3259 vs   76.0858 deg
      face y-a3-a2   at y   128.5177 vs  128.5177 deg
      face y-a3-a2   at a2   27.1247 vs   41.0243 deg
      face y-a3-a2   at a3   24.3576 vs   10.4580 deg
      face x-a1-a2   at x    33.0198 vs   33.0198 deg
      face x-a1-a2   at a1   22.3380 vs   33.0821 deg
      face x-a1-a2   at a2  124.6423 vs  113.8981 deg
      face x-a2-a3   at x    49.5871 vs   49.5871 deg
      face x-a2-a3   at a2   96.2609 vs   79.3490 deg
      face x-a2-a3   at a3   34.1520 vs   51.0639 deg
      face x-a3-a1   at x    24.3942 vs   24.3942 deg
      face x-a3-a1   at a1   52.9510 vs   44.8633 deg
      face x-a3-a1   at a3  102.6548 vs  110.7425 deg
PASS [C9] P' is not similar to P (ratio of squared lengths a1a2 : a1a3 differs)
PASS [C10] the mirror image of P' is also a valid partner of P (9 equal dihedral angles, 12 face angles differ)
PASS [C10] the similar copy of P' is also a valid partner of P (9 equal dihedral angles, 12 face angles differ)
PASS [C10] the mirror image of P' has the opposite orientation
PASS [C11] control: P against P itself: 9 equal dihedral angles, 0 face angles differ
PASS [C11] control: P against a similar copy of P: 9 equal dihedral angles, 0 face angles differ
PASS [C11] control: P against the mirror image of P: 9 equal dihedral angles, 0 face angles differ
PASS [C11] control: a3' moved by 1e-6: only the edge a1-a2 (whose faces avoid a3) keeps its angle
PASS [C12] R is the rotation of the quaternion (100, 5, -18, 7)
PASS [C12] R^T R = I and det R = 1
PASS [C12] a_k' = t_k a_k and a_k' - x' = s_k R(a_k - x) with t_k, s_k > 0 (k = 1, 2, 3)
PASS [C12] the three conditions A_kl(x) = ((R - I) N_kl) . M_kl = 0 hold exactly
PASS [Lemma 3, float] apex face angles from the polar triangle formula agree (max error 1.6e-13 deg)
ALL CHECKS PASSED
