# r2_general.py (independent verification run 2, AI-assisted, own code); p = 2147480641
[n=4] V=[(23, 10), (23, 24), (-21, 36), (-26, 6)]: Lemma 2.1(b),(c) exact at 3 rational x: True; exact in Q[rho]/(rho^2-q) at x=(47, -11): definition == three-point form True, Pitot sum_i (-1)^i w_i rho_i = 0: True
[n=4] V=[(-33, -3), (-21, -33), (34, -6), (4, 11)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=4] V=[(25, 37), (-7, -37), (-9, 24), (-13, -2)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=5] V=[(11, -32), (25, -7), (21, -8), (-9, 29), (-30, 4)]: Lemma 2.1(b),(c) exact at 3 rational x: True; exact in Q[rho]/(rho^2-q) at x=(13, -7): definition == three-point form True
[n=5] V=[(-13, -19), (28, 27), (-6, 40), (-6, -29), (-33, 3)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=5] V=[(-37, -12), (-30, 34), (-23, 19), (19, -32), (35, 29)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=6] V=[(-35, 5), (-16, -22), (-40, 11), (7, -40), (22, -6), (-15, 29)]: Lemma 2.1(b),(c) exact at 3 rational x: True; exact in Q[rho]/(rho^2-q) at x=(-3, 50): definition == three-point form True, Pitot sum_i (-1)^i w_i rho_i = 0: True
[n=6] V=[(26, -3), (13, 28), (-29, 0), (-28, -1), (26, 19), (36, 4)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=6] V=[(-32, 26), (-25, 5), (-13, 24), (2, 24), (-18, -34), (11, -19)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=7] V=[(17, -16), (-9, 8), (18, 38), (5, 34), (-5, 37), (17, -6), (8, 11)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=7] V=[(-25, -27), (-7, 18), (30, -20), (-23, 9), (9, -16), (-20, 40), (-26, 0)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=7] V=[(-21, -17), (-31, -35), (0, 23), (10, -15), (-1, -20), (10, 34), (-6, -32)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=8] V=[(31, -10), (24, 33), (0, -36), (33, -21), (33, 24), (-35, 27), (28, -18), (-35, 33)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=8] V=[(-37, -15), (32, 26), (4, 5), (34, -35), (-19, 9), (27, 4), (31, 35), (1, -37)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=8] V=[(14, -36), (-16, -31), (29, 8), (-27, 28), (-39, 29), (33, -9), (-6, 38), (27, 29)]: Lemma 2.1(b),(c) exact at 3 rational x: True
[n=4] V=[(-21, 21), (-27, -4), (16, 29), (-12, 36)]: Theorem 3.2(a),(c) mod p (2^3 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent; p0 not tangent): True
[n=4] V=[(5, 33), (20, -9), (-25, -17), (-18, 9)]: Theorem 3.2(a),(c) mod p (2^3 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent; p0 not tangent): True
[n=5] V=[(0, -34), (-20, -34), (-15, -10), (-38, -6), (22, 22)]: Theorem 3.2(a),(c) mod p (2^4 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=5] V=[(-31, -33), (3, -18), (-25, 38), (32, 34), (36, 11)]: Theorem 3.2(a),(c) mod p (2^4 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=6] V=[(-26, 0), (-38, -27), (27, 25), (24, 1), (2, -5), (-26, 37)]: Theorem 3.2(a),(c) mod p (2^5 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=6] V=[(8, 31), (22, 33), (8, 16), (9, 29), (-5, -30), (-1, 1)]: Theorem 3.2(a),(c) mod p (2^5 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=7] V=[(-11, 4), (14, -6), (30, -22), (-17, -16), (-5, -14), (32, -11), (10, 24)]: Theorem 3.2(a),(c) mod p (2^6 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=7] V=[(5, 14), (4, 9), (19, 33), (8, 8), (-4, 9), (-20, -28), (35, -38)]: Theorem 3.2(a),(c) mod p (2^6 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=8] V=[(-5, -39), (-26, -38), (-34, 0), (-25, -34), (14, 26), (5, -31), (23, 28), (28, 28)]: Theorem 3.2(a),(c) mod p (2^7 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
[n=8] V=[(-13, 11), (-24, -7), (34, -5), (-8, -31), (32, -25), (11, -1), (-28, 6), (30, 23)]: Theorem 3.2(a),(c) mod p (2^7 distinct p_eps with s!=0; tangent exactly for the class +-eps; random w in K(x) not tangent): True
collision determinant (Theorem 3.2 proof), V=[(0, 0), (1, 0), (1, 1), (0, 1)]: 28 pairs of sign classes; coefficient of rho_j rho_k = +-2 det(v_a-x, v_b-x) and only mixed rho_p rho_q terms: True
collision determinant (Theorem 3.2 proof), V=[(-26, 18), (11, -31), (-18, 22), (9, -9)]: 28 pairs of sign classes; coefficient of rho_j rho_k = +-2 det(v_a-x, v_b-x) and only mixed rho_p rho_q terms: True
proof of Theorem 1.1, V=[(0, 0), (1, 0), (1, 1), (0, 1)]: on P(K(x)) (4 random x), F_P(t k + w1) has degree exactly 8 in t (so beta^6 divides the binary form: order 6 at p0) and its 8 roots are the 8 distinct p_eps(x): True
proof of Theorem 1.1, V=[(0, 0), (8, 1), (3, 3), (1, 9)]: on P(K(x)) (4 random x), F_P(t k + w1) has degree exactly 8 in t (so beta^6 divides the binary form: order 6 at p0) and its 8 roots are the 8 distinct p_eps(x): True
proof of Theorem 1.1, V=[(0, 0), (6, 5), (6, 0), (0, 7)]: on P(K(x)) (4 random x), F_P(t k + w1) has degree exactly 8 in t (so beta^6 divides the binary form: order 6 at p0) and its 8 roots are the 8 distinct p_eps(x): True
proof of Theorem 1.1, V=[(40, 24), (22, -35), (22, 1), (16, 7)]: on P(K(x)) (4 random x), F_P(t k + w1) has degree exactly 8 in t (so beta^6 divides the binary form: order 6 at p0) and its 8 roots are the 8 distinct p_eps(x): True
Remark 3.3: convex V=[(0.0, 0.0), (7.0, 1.0), (6.0, 5.0), (1.0, 4.0)], x = diagonal intersection (3.375, 2.8125): M(x)(r1,r2,-r3,-r4) = ['0.0e+00', '5.6e-17', '0.0e+00', '5.6e-17'] (max abs 5.6e-17)
ALL OK: True (4.5s)
