Second independent verification run: certificate r2_cert.py
pi in [3.1415926535897932384626433832795028841971, 3.1415926535897932384626433832795028841972] (2 acos 0, cos-bracket)

[1] Table 1
ok    v0: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2
ok    v1: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2
ok    v2: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2
ok    v3: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2
ok    v4: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2
ok    v5: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2
ok    v6: stereographic data give (X, Y, Z)/D of Table 1 and X^2+Y^2+Z^2 = D^2

[2] Theorem 1.1(a): hypotheses of Lemma 2.2, exactly
ok    Q: |v_i| = 1 exactly
ok    Q: all z_i > 0
ok    Q: h_i x h_(i+1) > 0 for all i (Lemma 2.2(i))
ok    Q: winding number of (h_0..h_(n-1)) about 0 is 1 (Lemma 2.2(ii) <=> 1)
ok    Q: all s_i != 0 (no turn 0 or pi)
ok    Q satisfies Lemma 2.2 with all z > 0
ok    smallest z is z_2 = 43423/206577 > 0.21
ok    largest polar distance acos(z_2) in [1.359014, 1.359015] < 1.36
ok    signs of y_i are + + + + - - -
ok    v0: r = [0.130839, 0.130840], phi = [0.215357, 0.215358] round to Table 1 (0.1308, 0.2154)
ok    v1: r = [0.889221, 0.889222], phi = [0.876058, 0.876059] round to Table 1 (0.8892, 0.8761)
ok    v2: r = [1.359014, 1.359015], phi = [1.128186, 1.128187] round to Table 1 (1.359, 1.1282)
ok    v3: r = [0.299327, 0.299328], phi = [1.139778, 1.139779] round to Table 1 (0.2993, 1.1398)
ok    v4: r = [0.210323, 0.210324], phi = [3.866661, 3.866662] round to Table 1 (0.2103, 3.8667)
ok    v5: r = [0.930183, 0.930184], phi = [5.745499, 5.745500] round to Table 1 (0.9302, 5.7455)
ok    v6: r = [0.777686, 0.777687], phi = [6.076694, 6.076695] round to Table 1 (0.7777, 6.0767)

[3] Table 2: lengths, turning angles, interior angles
ok    i=0: l = [0.7888960631491, 0.7888960631492], tau = [-1.9175737534232, -1.9175737534231], pi - tau = [289.8688, 289.8689] deg, sign s = -1
ok    i=1: l = [0.5203246524735, 0.5203246524736], tau = [0.3996688062736, 0.3996688062737], pi - tau = [157.1006, 157.1007] deg, sign s = +1
ok    i=2: l = [1.0597090726299, 1.0597090726300], tau = [2.7373976261019, 2.7373976261020], pi - tau = [23.1586, 23.1587] deg, sign s = +1
ok    i=3: l = [0.4988494499224, 0.4988494499225], tau = [-0.1637580559965, -0.1637580559964], pi - tau = [189.3826, 189.3827] deg, sign s = -1
ok    i=4: l = [1.0077478840580, 1.0077478840581], tau = [1.7628534681898, 1.7628534681899], pi - tau = [78.9959, 78.9960] deg, sign s = +1
ok    i=5: l = [0.2914633818585, 0.2914633818586], tau = [1.9867793518819, 1.9867793518820], pi - tau = [66.1659, 66.1660] deg, sign s = +1
ok    i=6: l = [0.6600477045583, 0.6600477045584], tau = [1.0494574330733, 1.0494574330734], pi - tau = [119.8705, 119.8706] deg, sign s = +1
      perimeter = [4.827038, 4.827039]

[4] Theorem 1.1(b): development cut at v0
      w0 = ([0.000000, 0.000000], [0.000000, 0.000000])
      w1 = ([0.788896, 0.788897], [0.000000, 0.000000])
      w2 = ([1.268213, 1.268214], [0.202465, 0.202466])
      w3 = ([0.208515, 0.208516], [0.207261, 0.207262])
      w4 = ([-0.283287, -0.283286], [0.290814, 0.290815])
      w5 = ([-0.259333, -0.259332], [-0.716649, -0.716648])
      w6 = ([0.004400, 0.004401], [-0.592568, -0.592567])
      w7 = ([0.058189, 0.058190], [0.065285, 0.065286])
ok    segments 0 and 6 cross (X); the other 14 non-adjacent pairs satisfy (D)
ok    determinant [-0.4674739433856634117259, -0.4674739433856634117258] inside the printed [-0.46747394338566341173, -0.46747394338566341172]
ok    determinant [0.0515031890342307470428, 0.0515031890342307470429] inside the printed [0.05150318903423074704, 0.05150318903423074705]
ok    determinant [0.0347682870378404176870, 0.0347682870378404176871] inside the printed [0.03476828703784041768, 0.03476828703784041769]
ok    determinant [-0.4842088453820537410818, -0.4842088453820537410817] inside the printed [-0.48420884538205374109, -0.48420884538205374108]
ok    all four |determinants| > 0.034
ok    lambda in [0.066993870, 0.066993871] c [0.066993, 0.066994], mu in [0.900760195, 0.900760196] c [0.900760, 0.900761]
ok    distances [0.592567, 0.592568], [0.065285, 0.065286], [0.052675, 0.052676], [0.733596, 0.733597] round to 0.5926, 0.0653, 0.0527, 0.7336
      crossing point at distance lambda*l0 = [0.052851, 0.052852] from w0 (figure: 0.0529); x = [0.052851, 0.052852]

[5] Theorem 1.1(c): the arc of bad cut points
ok    arc length lambda l0 + (1 - mu) l6 in [0.11835420, 0.11835421] c [0.11835, 0.11836]
ok    cut on e0 at t = 0.000001000: segments 0 and 6 (first and seventh) cross
ok    cut on e0 at t = 0.010000000: segments 0 and 6 (first and seventh) cross
ok    cut on e0 at t = 0.030000000: segments 0 and 6 (first and seventh) cross
ok    cut on e0 at t = 0.050000000: segments 0 and 6 (first and seventh) cross
ok    cut on e0 at t = 0.066000000: segments 0 and 6 (first and seventh) cross
ok    cut on e0 at t = 0.066993771: segments 0 and 6 (first and seventh) cross
ok    cut on e6 at t = 0.900760296: segments 1 and 7 (second and eighth) cross
ok    cut on e6 at t = 0.910000000: segments 1 and 7 (second and eighth) cross
ok    cut on e6 at t = 0.950000000: segments 1 and 7 (second and eighth) cross
ok    cut on e6 at t = 0.990000000: segments 1 and 7 (second and eighth) cross
ok    cut on e6 at t = 0.999999000: segments 1 and 7 (second and eighth) cross
ok    just outside the arc: cut on e0 at t = 17/250 is simple (certified)
ok    just outside the arc: cut on e6 at t = 9/10 is simple (certified)

[6] Theorem 1.1(d): cuts at v1..v6
ok    cut at v1: all 15 non-adjacent pairs satisfy (D): simple
ok    cut at v2: all 15 non-adjacent pairs satisfy (D): simple
ok    cut at v3: all 15 non-adjacent pairs satisfy (D): simple
ok    cut at v4: all 15 non-adjacent pairs satisfy (D): simple
ok    cut at v5: all 15 non-adjacent pairs satisfy (D): simple
ok    cut at v6: all 15 non-adjacent pairs satisfy (D): simple

[7] Gauss-Bonnet: exact identity exp(i(sum tau + area)) = 1 and the multiple of 2 pi
ok    prod (k_i + i s_i)/(1 - c_i^2) * prod (den_i + i num_i)^2/(den_i^2 + num_i^2) = 1 exactly
ok    sum tau = [5.8548248761012, 5.8548248761013], area = [0.4283604310783, 0.4283604310784]; sum tau + area - 2 pi in [-0.001, 0.001] (so the multiple of 2 pi is 1 and the identity is Gauss-Bonnet)

[8] Proposition 1.3 and Table 3
ok    Q': |v_i| = 1 exactly
ok    Q': all z_i > 0
ok    Q': h_i x h_(i+1) > 0 for all i (Lemma 2.2(i))
ok    Q': winding number of (h_0..h_(n-1)) about 0 is 1 (Lemma 2.2(ii) <=> 1)
ok    Q': all s_i != 0 (no turn 0 or pi)
ok    Q' satisfies Lemma 2.2 with all z > 0
ok    smallest z is z_5' = 434355078771/19565644921229 (exactly as printed); v5' is the farthest vertex
      denominators of the v_i': [7721804394837, 5237413873049, 551275336701, 25006348007109, 40773609693117, 19565644921229, 100025061728241]
ok    v0': r = [1.53476, 1.53477], phi = [0.00872, 0.00873], interior angle [36.80, 36.81] deg as in Table 3
ok    v1': r = [1.01517, 1.01518], phi = [0.46349, 0.46350], interior angle [143.48, 143.49] deg as in Table 3
ok    v2': r = [0.61983, 0.61984], phi = [0.55984, 0.55985], interior angle [169.18, 169.19] deg as in Table 3
ok    v3': r = [0.03186, 0.03187], phi = [3.26964, 3.26965], interior angle [48.30, 48.31] deg as in Table 3
ok    v4': r = [1.34253, 1.34254], phi = [5.97929, 5.97930], interior angle [142.87, 142.88] deg as in Table 3
ok    v5': r = [1.54859, 1.54860], phi = [6.13711, 6.13712], interior angle [36.99, 37.00] deg as in Table 3
ok    v6': r = [0.03165, 0.03166], phi = [6.26372, 6.26373], interior angle [351.11, 351.12] deg as in Table 3
ok    Q' cut at v0': crossing edge pairs [(2, 5), (2, 6)] as in Table 3
ok    Q' cut at v1': crossing edge pairs [(2, 5), (2, 6)] as in Table 3
ok    Q' cut at v2': crossing edge pairs [(2, 5), (2, 6)] as in Table 3
ok    Q' cut at v3': simple (15 pairs (D))
ok    Q' cut at v4': crossing edge pairs [(5, 3), (6, 3)] as in Table 3
ok    Q' cut at v5': crossing edge pairs [(5, 3), (6, 3)] as in Table 3
ok    cut at v5': the eight determinants have |.| >= 0.2479 > 0.24
ok    Q' cut at v6': crossing edge pairs [(6, 3), (6, 5), (2, 5)] as in Table 3

[9] Remark 4.1: certified interior cut points of Q
ok    cut on e0 at t = 1/20: bad, crossing segment pairs [(0, 6)]
ok    cut on e0 at t = 1/10: good (all pairs (D))
ok    cut on e0 at t = 1/5: bad, crossing segment pairs [(0, 7)]
ok    cut on e0 at t = 201/1000: bad, crossing segment pairs [(0, 7)]
ok    cut on e0 at t = 1/2: good (all pairs (D))
ok    cut on e3 at t = 1/2: good (all pairs (D))
ok    cut on e6 at t = 18/25: bad, crossing segment pairs [(0, 7)]
ok    cut on e6 at t = 403/500: bad, crossing segment pairs [(0, 7)]
ok    cut on e6 at t = 17/20: good (all pairs (D))
ok    cut on e6 at t = 19/20: bad, crossing segment pairs [(1, 7)]

[10] Remark 4.2: copies Q_s
ok    s = 1/2: Lemma 2.2 holds, only the cut at v0 is bad (segments 0, 6), min |det| = 3.739e-03 ~ 3.7e-3
ok    s = 1/5: Lemma 2.2 holds, only the cut at v0 is bad (segments 0, 6), min |det| = 1.137e-04 ~ 1.1e-4
ok    s = 1/20: Lemma 2.2 holds, only the cut at v0 is bad (segments 0, 6), min |det| = 4.586e-07 ~ 4.6e-7

[11] Controls
ok    convex 5-gon about N (stereographic radius 1/3): all vertex cuts certified simple
ok    convex 8-gon about N (stereographic radius 9/10): all vertex cuts certified simple
ok    deliberately wrong input (v1 and v2 swapped) is rejected by the exact checks
ok    deliberately wrong input (v4 moved to the southern hemisphere) is rejected by the exact checks
ok    deliberately wrong input (vertices in reverse order) is rejected by the exact checks

ALL CHECKS OF r2_cert.py PASSED
