Project: Six distances from the E2 diameter-heptagon pattern

LeanPool.lean

@@ -1061,6 +1061,19 @@ import LeanPool.Erdos132ThreeChain.PowerThree
 import LeanPool.Erdos132ThreeChain.Statement
 import LeanPool.Erdos132ThreeChain.Support
 import LeanPool.Erdos132ThreeChain.Witnesses
+import LeanPool.Erdos132WeiE2
+import LeanPool.Erdos132WeiE2.Algebra.BezoutGenerated
+import LeanPool.Erdos132WeiE2.Algebra.Exclusions
+import LeanPool.Erdos132WeiE2.Algebra.G10
+import LeanPool.Erdos132WeiE2.Algebra.Ranges
+import LeanPool.Erdos132WeiE2.Algebra.TanExpressions
+import LeanPool.Erdos132WeiE2.Algebra.TrigSigns
+import LeanPool.Erdos132WeiE2.Counting.Assembly
+import LeanPool.Erdos132WeiE2.Counting.Endgame
+import LeanPool.Erdos132WeiE2.Final
+import LeanPool.Erdos132WeiE2.Geometry.Basic
+import LeanPool.Erdos132WeiE2.Geometry.Parametrization
+import LeanPool.Erdos132WeiE2.Geometry.Star
 import LeanPool.Erdos137
 import LeanPool.Erdos137.AxiomAudit
 import LeanPool.Erdos137.Base

LeanPool/Erdos132WeiE2.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Egor Lyfar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egor Lyfar
+-/
+
+import LeanPool.Erdos132WeiE2.Algebra.BezoutGenerated
+import LeanPool.Erdos132WeiE2.Algebra.Exclusions
+import LeanPool.Erdos132WeiE2.Algebra.G10
+import LeanPool.Erdos132WeiE2.Algebra.Ranges
+import LeanPool.Erdos132WeiE2.Algebra.TanExpressions
+import LeanPool.Erdos132WeiE2.Algebra.TrigSigns
+import LeanPool.Erdos132WeiE2.Counting.Assembly
+import LeanPool.Erdos132WeiE2.Counting.Endgame
+import LeanPool.Erdos132WeiE2.Final
+import LeanPool.Erdos132WeiE2.Geometry.Basic
+import LeanPool.Erdos132WeiE2.Geometry.Parametrization
+import LeanPool.Erdos132WeiE2.Geometry.Star
+
+/-!
+# Six distances from the E2 diameter-heptagon pattern
+
+Source: doi:10.11650/tjm.18.2014.4030, url:https://projecteuclid.org/journals/taiwanese-journal-of-mathematics/volume-18/issue-6/DISTANCE-SETS-WITH-DIAMETER-GRAPH-BEING-CYCLE/10.11650/tjm.18.2014.4030.pdf
+Authors: Egor Lyfar
+Status: verified
+Main declarations: `LeanPool.Erdos132WeiE2.e2_pattern_six_distances`
+Tags: discrete-geometry, distance-sets, diameter-graph, erdos-problems
+MSC: 52C10, 05C62
+-/

LeanPool/Erdos132WeiE2/Algebra/BezoutGenerated.lean

@@ -0,0 +1,325 @@
+/-
+Copyright (c) 2026 Egor Lyfar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egor Lyfar
+-/
+import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Generated E2 Bézout cofactors
+
+Generated from `cofactors.json`; do not hand-edit.
+Pinned input and generators: `theorem4-2014/bezout-lean/`
+in `github.com/lyfar/erdos132-wei-certificates` @ `34bc87ff0`.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Algebra
+
+/-- Generated from `cofactors.json`; do not hand-edit. -/
+noncomputable def case1C0 (x y : ℝ) : ℝ :=
+  ((1235 : ℝ) / 4096) * x ^ 6 * y +
+    ((-1235 : ℝ) / 4096) * x ^ 6 +
+    ((1235 : ℝ) / 1024) * x ^ 5 * y ^ 2 +
+    ((-2461 : ℝ) / 1024) * x ^ 5 * y +
+    ((775 : ℝ) / 256) * x ^ 5 +
+    ((-43 : ℝ) / 1024) * x ^ 4 * y ^ 3 +
+    ((-14913 : ℝ) / 1024) * x ^ 4 * y ^ 2 +
+    ((-15107 : ℝ) / 4096) * x ^ 4 * y +
+    ((6235 : ℝ) / 4096) * x ^ 4 +
+    ((-1129 : ℝ) / 2048) * x ^ 3 * y ^ 4 +
+    ((18887 : ℝ) / 2048) * x ^ 3 * y ^ 3 +
+    ((110393 : ℝ) / 2048) * x ^ 3 * y ^ 2 +
+    ((-34649 : ℝ) / 2048) * x ^ 3 * y +
+    ((-88659 : ℝ) / 1024) * x ^ 3 +
+    ((863 : ℝ) / 4096) * x ^ 2 * y ^ 5 +
+    ((-1423 : ℝ) / 4096) * x ^ 2 * y ^ 4 +
+    ((11815 : ℝ) / 1024) * x ^ 2 * y ^ 3 +
+    ((-21667 : ℝ) / 1024) * x ^ 2 * y ^ 2 +
+    ((-129665 : ℝ) / 2048) * x ^ 2 * y +
+    ((356649 : ℝ) / 2048) * x ^ 2 +
+    ((-1129 : ℝ) / 2048) * x * y ^ 4 +
+    ((-7405 : ℝ) / 2048) * x * y ^ 3 +
+    ((-81881 : ℝ) / 2048) * x * y ^ 2 +
+    ((48189 : ℝ) / 2048) * x * y +
+    ((3139 : ℝ) / 1024) * x +
+    ((863 : ℝ) / 4096) * y ^ 5 +
+    ((5481 : ℝ) / 4096) * y ^ 4 +
+    ((527 : ℝ) / 256) * y ^ 3 +
+    ((-1829 : ℝ) / 256) * y ^ 2 +
+    ((-5865 : ℝ) / 1024) * y +
+    ((-5855 : ℝ) / 1024) * 1
+
+/-- Bézout case 1 cofactor `C1` for `(F, P_RQ, P_BC)`, from `cofactors.json`. -/
+noncomputable def case1C1 (x y : ℝ) : ℝ :=
+  ((-1235 : ℝ) / 4096) * x ^ 4 * y +
+    ((1235 : ℝ) / 4096) * x ^ 4 +
+    ((231 : ℝ) / 64) * x ^ 3 * y +
+    ((-2785 : ℝ) / 512) * x ^ 3 +
+    ((-20967 : ℝ) / 2048) * x ^ 2 * y +
+    ((60771 : ℝ) / 2048) * x ^ 2 +
+    ((-4581 : ℝ) / 2048) * x * y ^ 4 +
+    ((-23317 : ℝ) / 2048) * x * y ^ 3 +
+    ((44385 : ℝ) / 2048) * x * y ^ 2 +
+    ((63723 : ℝ) / 2048) * x * y +
+    ((-60759 : ℝ) / 1024) * x +
+    ((863 : ℝ) / 4096) * y ^ 5 +
+    ((-4875 : ℝ) / 4096) * y ^ 4 +
+    ((-3363 : ℝ) / 512) * y ^ 3 +
+    ((119 : ℝ) / 512) * y ^ 2 +
+    ((9047 : ℝ) / 2048) * y +
+    ((15531 : ℝ) / 2048) * 1
+
+/-- Bézout case 1 cofactor `C2` for `(F, P_RQ, P_BC)`, from `cofactors.json`. -/
+noncomputable def case1C2 (x y : ℝ) : ℝ :=
+  ((-1235 : ℝ) / 1024) * x ^ 3 +
+    ((43 : ℝ) / 1024) * x ^ 2 * y +
+    ((12357 : ℝ) / 1024) * x ^ 2 +
+    ((2855 : ℝ) / 1024) * x * y ^ 2 +
+    ((-3409 : ℝ) / 1024) * x * y +
+    ((-14413 : ℝ) / 1024) * x +
+    ((-863 : ℝ) / 2048) * y ^ 3 +
+    ((-2029 : ℝ) / 2048) * y ^ 2 +
+    ((-863 : ℝ) / 2048) * y +
+    ((-1773 : ℝ) / 2048) * 1
+
+lemma case1_bezout_identity (x y : ℝ) :
+    case1C0 x y * (
+          x ^ 2 * y ^ 2 +
+          x ^ 2 +
+          4 * x * y ^ 2 -
+          12 * x +
+          y ^ 2 +
+          1
+        ) +
+      case1C1 x y * (
+          x ^ 4 * y ^ 2 +
+          x ^ 4 +
+          16 * x ^ 3 * y +
+          2 * x ^ 2 * y ^ 2 -
+          30 * x ^ 2 -
+          16 * x * y +
+          y ^ 2 +
+          1
+        ) +
+      case1C2 x y * (
+          x ^ 4 * y ^ 4 +
+          2 * x ^ 4 * y ^ 3 -
+          6 * x ^ 4 * y ^ 2 +
+          2 * x ^ 4 * y +
+          x ^ 4 +
+          2 * x ^ 3 * y ^ 4 -
+          32 * x ^ 3 * y -
+          2 * x ^ 3 +
+          2 * x ^ 2 * y ^ 4 +
+          20 * x ^ 2 * y ^ 2 -
+          30 * x ^ 2 +
+          2 * x * y ^ 4 +
+          32 * x * y -
+          2 * x +
+          y ^ 4 -
+          2 * y ^ 3 -
+          6 * y ^ 2 -
+          2 * y +
+          1
+        ) = 1 := by
+  norm_num [case1C0, case1C1, case1C2]
+  ring
+
+/-- Bézout case 2 cofactor `C0` for `(F, P_RQ, P_BA)`, from `cofactors.json`. -/
+noncomputable def case2C0 (x y : ℝ) : ℝ :=
+  ((6167 : ℝ) / 20480) * x ^ 6 * y +
+    ((-6167 : ℝ) / 20480) * x ^ 6 +
+    ((-173 : ℝ) / 48) * x ^ 5 * y +
+    ((3871 : ℝ) / 1280) * x ^ 5 +
+    ((662687 : ℝ) / 61440) * x ^ 4 * y +
+    ((243929 : ℝ) / 61440) * x ^ 4 +
+    ((9287 : ℝ) / 5120) * x ^ 3 * y ^ 4 +
+    ((7385 : ℝ) / 1536) * x ^ 3 * y ^ 3 +
+    ((13611 : ℝ) / 1280) * x ^ 3 * y ^ 2 +
+    ((-19813 : ℝ) / 320) * x ^ 3 * y +
+    ((-113253 : ℝ) / 1024) * x ^ 3 +
+    ((-12953 : ℝ) / 61440) * x ^ 2 * y ^ 5 +
+    ((-28297 : ℝ) / 4096) * x ^ 2 * y ^ 4 +
+    ((50857 : ℝ) / 6144) * x ^ 2 * y ^ 3 +
+    ((-1258921 : ℝ) / 30720) * x ^ 2 * y ^ 2 +
+    ((31635 : ℝ) / 2048) * x ^ 2 * y +
+    ((2056069 : ℝ) / 10240) * x ^ 2 +
+    ((12953 : ℝ) / 15360) * x * y ^ 5 +
+    ((3647 : ℝ) / 960) * x * y ^ 4 +
+    ((971 : ℝ) / 1920) * x * y ^ 3 +
+    ((100603 : ℝ) / 7680) * x * y ^ 2 +
+    ((611021 : ℝ) / 15360) * x * y +
+    ((767 : ℝ) / 160) * x +
+    ((-12953 : ℝ) / 61440) * y ^ 5 +
+    ((7107 : ℝ) / 20480) * y ^ 4 +
+    ((-35507 : ℝ) / 30720) * y ^ 3 +
+    ((-81683 : ℝ) / 10240) * y ^ 2 +
+    ((-8299 : ℝ) / 960) * y +
+    ((-21769 : ℝ) / 3840) * 1
+
+/-- Bézout case 2 cofactor `C1` for `(F, P_RQ, P_BA)`, from `cofactors.json`. -/
+noncomputable def case2C1 (x y : ℝ) : ℝ :=
+  ((-6167 : ℝ) / 20480) * x ^ 4 * y +
+    ((6167 : ℝ) / 20480) * x ^ 4 +
+    ((36859 : ℝ) / 15360) * x ^ 3 * y +
+    ((-6797 : ℝ) / 1024) * x ^ 3 +
+    ((131747 : ℝ) / 30720) * x ^ 2 * y +
+    ((1279649 : ℝ) / 30720) * x ^ 2 +
+    ((-9287 : ℝ) / 5120) * x * y ^ 4 +
+    ((-7385 : ℝ) / 1536) * x * y ^ 3 +
+    ((81707 : ℝ) / 3840) * x * y ^ 2 +
+    ((-139037 : ℝ) / 15360) * x * y +
+    ((-23303 : ℝ) / 320) * x +
+    ((12953 : ℝ) / 61440) * y ^ 5 +
+    ((-7107 : ℝ) / 20480) * y ^ 4 +
+    ((-68117 : ℝ) / 30720) * y ^ 3 +
+    ((1121 : ℝ) / 30720) * y ^ 2 +
+    ((8299 : ℝ) / 960) * y +
+    ((25609 : ℝ) / 3840) * 1
+
+/-- Bézout case 2 cofactor `C2` for `(F, P_RQ, P_BA)`, from `cofactors.json`. -/
+noncomputable def case2C2 (x y : ℝ) : ℝ :=
+  ((6167 : ℝ) / 640) * x ^ 3 +
+    ((-137 : ℝ) / 384) * x ^ 2 * y +
+    ((-185123 : ℝ) / 1920) * x ^ 2 +
+    ((-42769 : ℝ) / 1920) * x * y ^ 2 +
+    ((51127 : ℝ) / 1920) * x * y +
+    ((14389 : ℝ) / 128) * x +
+    ((12953 : ℝ) / 3840) * y ^ 3 +
+    ((30491 : ℝ) / 3840) * y ^ 2 +
+    ((12953 : ℝ) / 3840) * y +
+    ((26651 : ℝ) / 3840) * 1
+
+lemma case2_bezout_identity (x y : ℝ) :
+    case2C0 x y * (
+          x ^ 2 * y ^ 2 +
+          x ^ 2 +
+          4 * x * y ^ 2 -
+          12 * x +
+          y ^ 2 +
+          1
+        ) +
+      case2C1 x y * (
+          x ^ 4 * y ^ 2 +
+          x ^ 4 +
+          16 * x ^ 3 * y +
+          2 * x ^ 2 * y ^ 2 -
+          30 * x ^ 2 -
+          16 * x * y +
+          y ^ 2 +
+          1
+        ) +
+      case2C2 x y * (
+          (x -
+          y) * (x * y +
+          1) * (x ^ 2 * y +
+          x * y ^ 2 +
+          3 * x -
+          y)
+        ) = 1 := by
+  norm_num [case2C0, case2C1, case2C2]
+  ring
+
+/-- Bézout case 3 cofactor `C0` for `(F, P_RC, P_BA)`, from `cofactors.json`. -/
+noncomputable def case3C0 (x y : ℝ) : ℝ :=
+  ((82203 : ℝ) / 28672) * x ^ 6 * y +
+    ((81293 : ℝ) / 43008) * x ^ 5 * y +
+    ((109251 : ℝ) / 7168) * x ^ 5 +
+    ((82203 : ℝ) / 14336) * x ^ 4 * y ^ 2 +
+    ((-12899101 : ℝ) / 86016) * x ^ 4 * y +
+    ((-2670559 : ℝ) / 43008) * x ^ 4 +
+    ((959 : ℝ) / 256) * x ^ 3 * y ^ 4 +
+    ((34795 : ℝ) / 3072) * x ^ 3 * y ^ 3 +
+    ((226609 : ℝ) / 5376) * x ^ 3 * y ^ 2 +
+    ((761095 : ℝ) / 10752) * x ^ 3 * y +
+    ((-2369657 : ℝ) / 5376) * x ^ 3 +
+    ((-178105 : ℝ) / 86016) * x ^ 2 * y ^ 5 +
+    ((-489031 : ℝ) / 43008) * x ^ 2 * y ^ 4 +
+    ((4129109 : ℝ) / 43008) * x ^ 2 * y ^ 3 +
+    ((-1511365 : ℝ) / 21504) * x ^ 2 * y ^ 2 +
+    ((746971 : ℝ) / 2048) * x ^ 2 * y +
+    ((6261755 : ℝ) / 14336) * x ^ 2 +
+    ((178105 : ℝ) / 43008) * x * y ^ 5 +
+    ((-35869 : ℝ) / 2688) * x * y ^ 4 +
+    ((103837 : ℝ) / 2688) * x * y ^ 3 +
+    ((-45713 : ℝ) / 768) * x * y ^ 2 +
+    ((-3437587 : ℝ) / 10752) * x * y +
+    ((2177191 : ℝ) / 21504) * x +
+    ((-178105 : ℝ) / 86016) * y ^ 5 +
+    ((189403 : ℝ) / 43008) * y ^ 4 +
+    ((64487 : ℝ) / 14336) * y ^ 3 +
+    ((106197 : ℝ) / 2048) * y ^ 2 +
+    ((-1644313 : ℝ) / 21504) * y +
+    ((-165611 : ℝ) / 21504) * 1
+
+/-- Bézout case 3 cofactor `C1` for `(F, P_RC, P_BA)`, from `cofactors.json`. -/
+noncomputable def case3C1 (x y : ℝ) : ℝ :=
+  ((-82203 : ℝ) / 28672) * x ^ 4 * y +
+    ((26363 : ℝ) / 768) * x ^ 3 * y +
+    ((-109251 : ℝ) / 7168) * x ^ 3 +
+    ((199189 : ℝ) / 6144) * x ^ 2 * y +
+    ((37883 : ℝ) / 192) * x ^ 2 +
+    ((-959 : ℝ) / 256) * x * y ^ 4 +
+    ((-123071 : ℝ) / 2688) * x * y ^ 3 +
+    ((225011 : ℝ) / 10752) * x * y ^ 2 +
+    ((-536941 : ℝ) / 5376) * x * y +
+    ((-1263431 : ℝ) / 7168) * x +
+    ((178105 : ℝ) / 86016) * y ^ 5 +
+    ((-269 : ℝ) / 1024) * y ^ 4 +
+    ((-928477 : ℝ) / 43008) * y ^ 3 +
+    ((-331283 : ℝ) / 10752) * y ^ 2 +
+    ((2018543 : ℝ) / 21504) * y +
+    ((187115 : ℝ) / 21504) * 1
+
+/-- Bézout case 3 cofactor `C2` for `(F, P_RC, P_BA)`, from `cofactors.json`. -/
+noncomputable def case3C2 (x y : ℝ) : ℝ :=
+  ((82203 : ℝ) / 14336) * x ^ 4 +
+    ((-300705 : ℝ) / 7168) * x ^ 3 * y +
+    ((-26363 : ℝ) / 384) * x ^ 3 +
+    ((19799 : ℝ) / 448) * x ^ 2 * y +
+    ((-7649 : ℝ) / 168) * x ^ 2 +
+    ((-339217 : ℝ) / 5376) * x * y ^ 2 +
+    ((6969181 : ℝ) / 21504) * x * y +
+    ((1291001 : ℝ) / 5376) * x +
+    ((178105 : ℝ) / 10752) * y ^ 3 +
+    ((-91877 : ℝ) / 1344) * y ^ 2 +
+    ((-665927 : ℝ) / 10752) * y +
+    ((7126159 : ℝ) / 43008) * 1
+
+lemma case3_bezout_identity (x y : ℝ) :
+    case3C0 x y * (
+          x ^ 2 * y ^ 2 +
+          x ^ 2 +
+          4 * x * y ^ 2 -
+          12 * x +
+          y ^ 2 +
+          1
+        ) +
+      case3C1 x y * (
+          x ^ 4 * y ^ 2 +
+          2 * x ^ 4 * y +
+          x ^ 4 +
+          2 * x ^ 3 * y ^ 2 -
+          2 * x ^ 3 +
+          2 * x ^ 2 * y ^ 2 -
+          30 * x ^ 2 +
+          2 * x * y ^ 2 -
+          2 * x +
+          y ^ 2 -
+          2 * y +
+          1
+        ) +
+      case3C2 x y * (
+          (x -
+          y) * (x * y +
+          1) * (x ^ 2 * y +
+          x * y ^ 2 +
+          3 * x -
+          y)
+        ) = 1 := by
+  norm_num [case3C0, case3C1, case3C2]
+  ring
+
+end LeanPool.Erdos132WeiE2.Algebra