Exact rational regression witnesses

Kernel-reduced checks for the three configurations used during the convex k = 3 campaign. Keeping them at the basic layer lets global counterexample regressions use them without importing the closure stack.

def LeanPool.Erdos132ConvexK3.Witnesses.heptagon : Fin 7 → Point ℚ

Attempt 2's exact integer heptagon, in positive cyclic order.

Equations

• LeanPool.Erdos132ConvexK3.Witnesses.heptagon = ![(0, 0), (72, 0), (45, 68), (40, 75), (36, 77), (32, 75), (27, 68)]

theorem LeanPool.Erdos132ConvexK3.Witnesses.heptagon_strict_convex : CyclicStrictConvex heptagon

theorem LeanPool.Erdos132ConvexK3.Witnesses.heptagon_top_three : HasTopThreeDistanceClasses heptagon 7225 6649 5353

theorem LeanPool.Erdos132ConvexK3.Witnesses.heptagon_double_ladder : sqDist (heptagon 0) (heptagon 6) = 5353 ∧ sqDist (heptagon 0) (heptagon 5) = 6649 ∧ sqDist (heptagon 0) (heptagon 4) = 7225 ∧ sqDist (heptagon 1) (heptagon 2) = 5353 ∧ sqDist (heptagon 1) (heptagon 3) = 6649 ∧ sqDist (heptagon 1) (heptagon 4) = 7225

theorem LeanPool.Erdos132ConvexK3.Witnesses.heptagon_x_degree : vertexDegree heptagon 7225 6649 5353 0 = 5

def LeanPool.Erdos132ConvexK3.Witnesses.ninePoint : Fin 9 → Point ℚ

Attempt 3's exact nine-point low-altitude insertion witness.

Equations

• LeanPool.Erdos132ConvexK3.Witnesses.ninePoint = ![(0, 0), (180, -1), (370, -1), (570, 0), (309, 862), (300, 875), (285, 880), (270, 875), (261, 862)]

theorem LeanPool.Erdos132ConvexK3.Witnesses.ninePoint_strict_convex : CyclicStrictConvex ninePoint

theorem LeanPool.Erdos132ConvexK3.Witnesses.ninePoint_top_three : HasTopThreeDistanceClasses ninePoint 855625 838525 811165

theorem LeanPool.Erdos132ConvexK3.Witnesses.ninePoint_insertions_isolated : vertexDegree ninePoint 855625 838525 811165 1 = 0 ∧ vertexDegree ninePoint 855625 838525 811165 2 = 0

def LeanPool.Erdos132ConvexK3.Witnesses.rationalHexagon : Fin 6 → Point ℚ

A second exact rational hexagon, in positive cyclic order.

Equations

• LeanPool.Erdos132ConvexK3.Witnesses.rationalHexagon = ![(0, -20), (24171 / 50380, -(12571661 / 629750)), (48331 / 50380, -(12546661 / 629750)), (1208 / 229, -(4480 / 229)), (1, 0), (-1, 0)]

theorem LeanPool.Erdos132ConvexK3.Witnesses.rationalHexagon_strict_convex : CyclicStrictConvex rationalHexagon

theorem LeanPool.Erdos132ConvexK3.Witnesses.rationalHexagon_top_three : HasTopThreeDistanceClasses rationalHexagon (96661 / 229) 401 (2776265163521 / 6927250000)

theorem LeanPool.Erdos132ConvexK3.Witnesses.rationalHexagon_key_edges : sqDist (rationalHexagon 3) (rationalHexagon 5) = 96661 / 229 ∧ sqDist (rationalHexagon 0) (rationalHexagon 5) = 401 ∧ sqDist (rationalHexagon 3) (rationalHexagon 4) = 401 ∧ sqDist (rationalHexagon 0) (rationalHexagon 4) = 401 ∧ sqDist (rationalHexagon 2) (rationalHexagon 5) = 2776265163521 / 6927250000

theorem LeanPool.Erdos132ConvexK3.Witnesses.rationalHexagon_lower_degrees : vertexDegree rationalHexagon (96661 / 229) 401 (2776265163521 / 6927250000) 1 = 0 ∧ vertexDegree rationalHexagon (96661 / 229) 401 (2776265163521 / 6927250000) 2 = 1