diff --git a/LeanPool.lean b/LeanPool.lean
index aa0c8e656..3a742ba71 100644
--- a/LeanPool.lean
+++ b/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
diff --git a/LeanPool/Erdos132WeiE2.lean b/LeanPool/Erdos132WeiE2.lean
new file mode 100644
index 000000000..83db2c9ae
--- /dev/null
+++ b/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
+-/
diff --git a/LeanPool/Erdos132WeiE2/Algebra/BezoutGenerated.lean b/LeanPool/Erdos132WeiE2/Algebra/BezoutGenerated.lean
new file mode 100644
index 000000000..3089d4b2c
--- /dev/null
+++ b/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
diff --git a/LeanPool/Erdos132WeiE2/Algebra/Exclusions.lean b/LeanPool/Erdos132WeiE2/Algebra/Exclusions.lean
new file mode 100644
index 000000000..14417f0ab
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Algebra/Exclusions.lean
@@ -0,0 +1,223 @@
+/-
+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.TrigSigns
+import LeanPool.Erdos132WeiE2.Algebra.BezoutGenerated
+import LeanPool.Erdos132WeiE2.Algebra.TanExpressions
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
+
+/-!
+# Algebraic exclusions for the E2 diameter-heptagon pattern
+
+This module converts the possible distance collisions to tangent-coordinate polynomials and
+applies the generated Bézout certificates.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Algebra
+
+/-- The tangent-coordinate numerator of the E2 closure curve. -/
+def closurePolynomial (x y : ℝ) : ℝ :=
+  x ^ 2 * y ^ 2 + x ^ 2 + 4 * x * y ^ 2 - 12 * x + y ^ 2 + 1
+
+/-- The tangent-coordinate numerator forced by the distance collision `RA = Q`. -/
+def pRQ (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
+
+/-- The tangent-coordinate numerator forced by the distance collision `RA = eC`. -/
+def pRC (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
+
+/-- The tangent-coordinate numerator forced by the distance collision `RB = eC`. -/
+def pBC (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
+
+/-- The tangent-coordinate numerator forced by the distance collision `RB = eA`. -/
+def pBA (x y : ℝ) : ℝ :=
+  (x - y) * (x * y + 1) * (x ^ 2 * y + x * y ^ 2 + 3 * x - y)
+
+/-- Certified unit ideal for the collision `(RA, RB) = (Q, eC)`. -/
+lemma exclude_ra_q_rb_ec (x y : ℝ)
+    (hF : x ^ 2 * y ^ 2 + x ^ 2 + 4 * x * y ^ 2 - 12 * x + y ^ 2 + 1 = 0)
+    (hRQ : pRQ x y = 0) (hBC : pBC x y = 0) : False := by
+  have hRQ' : x ^ 4 * y ^ 2 + x ^ 4 + 16 * x ^ 3 * y + 2 * x ^ 2 * y ^ 2 -
+      30 * x ^ 2 - 16 * x * y + y ^ 2 + 1 = 0 := by
+    simpa only [pRQ] using hRQ
+  have hBC' : 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 = 0 := by
+    simpa only [pBC] using hBC
+  have hid := case1_bezout_identity x y
+  rw [hF, hRQ', hBC'] at hid
+  norm_num at hid
+
+/-- Certified unit ideal for the collision `(RA, RB) = (Q, eA)`. -/
+lemma exclude_ra_q_rb_ea (x y : ℝ)
+    (hF : x ^ 2 * y ^ 2 + x ^ 2 + 4 * x * y ^ 2 - 12 * x + y ^ 2 + 1 = 0)
+    (hRQ : pRQ x y = 0) (hBA : pBA x y = 0) : False := by
+  have hRQ' : x ^ 4 * y ^ 2 + x ^ 4 + 16 * x ^ 3 * y + 2 * x ^ 2 * y ^ 2 -
+      30 * x ^ 2 - 16 * x * y + y ^ 2 + 1 = 0 := by
+    simpa only [pRQ] using hRQ
+  have hBA' : (x - y) * (x * y + 1) *
+      (x ^ 2 * y + x * y ^ 2 + 3 * x - y) = 0 := by
+    simpa only [pBA] using hBA
+  have hid := case2_bezout_identity x y
+  rw [hF, hRQ', hBA'] at hid
+  norm_num at hid
+
+/-- Certified unit ideal for the collision `(RA, RB) = (eC, eA)`. -/
+lemma exclude_ra_ec_rb_ea (x y : ℝ)
+    (hF : x ^ 2 * y ^ 2 + x ^ 2 + 4 * x * y ^ 2 - 12 * x + y ^ 2 + 1 = 0)
+    (hRC : pRC x y = 0) (hBA : pBA x y = 0) : False := by
+  have hRC' : 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 = 0 := by
+    simpa only [pRC] using hRC
+  have hBA' : (x - y) * (x * y + 1) *
+      (x ^ 2 * y + x * y ^ 2 + 3 * x - y) = 0 := by
+    simpa only [pBA] using hBA
+  have hid := case3_bezout_identity x y
+  rw [hF, hRC', hBA'] at hid
+  norm_num at hid
+
+lemma tan_dictionary (A B x y : ℝ)
+    (hA : 0 < A) (hApi : A < Real.pi)
+    (hS : 0 < A + B) (hSpi : A + B < Real.pi)
+    (hx : x = Real.tan (A / 4)) (hy : y = Real.tan ((A + B) / 2)) :
+    Real.sin (A / 2) = 2 * x / (1 + x ^ 2) ∧
+      Real.cos (A / 2) = (1 - x ^ 2) / (1 + x ^ 2) ∧
+      Real.sin (A + B) = 2 * y / (1 + y ^ 2) ∧
+      Real.cos (A + B) = (1 - y ^ 2) / (1 + y ^ 2) := by
+  have hcosA : Real.cos (A / 2) ≠ -1 := by
+    have hpos : 0 < Real.cos (A / 2) :=
+      Real.cos_pos_of_mem_Ioo ⟨by linarith [Real.pi_pos], by linarith⟩
+    linarith
+  have hcosS : Real.cos (A + B) ≠ -1 := by
+    have hpos : 0 < Real.cos ((A + B) / 2) :=
+      Real.cos_pos_of_mem_Ioo ⟨by linarith [Real.pi_pos], by linarith⟩
+    have hdouble : Real.cos (A + B) ≠ -1 := by
+      intro heq
+      have hsquare := Real.cos_sq_add_sin_sq ((A + B) / 2)
+      have hdoubleCos := Real.cos_two_mul_eq_one_sub ((A + B) / 2)
+      rw [show 2 * ((A + B) / 2) = A + B by ring, heq] at hdoubleCos
+      nlinarith
+    exact hdouble
+  constructor
+  · rw [Real.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq]
+    rw [show A / 2 / 2 = A / 4 by ring, ← hx]
+  constructor
+  · rw [Real.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq (A / 2) hcosA]
+    rw [show A / 2 / 2 = A / 4 by ring, ← hx]
+  constructor
+  · rw [Real.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, ← hy]
+  · rw [Real.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq (A + B) hcosS, ← hy]
+
+lemma closure_implies_polynomial (A B x y : ℝ)
+    (hA : 0 < A) (hApi : A < Real.pi)
+    (hS : 0 < A + B) (hSpi : A + B < Real.pi)
+    (hx : x = Real.tan (A / 4)) (hy : y = Real.tan ((A + B) / 2))
+    (hclosure : 2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B)) = 1) :
+    closurePolynomial x y = 0 := by
+  obtain ⟨hsinA, _, _, hcosS⟩ := tan_dictionary A B x y hA hApi hS hSpi hx hy
+  have hdx : 1 + x ^ 2 ≠ 0 := by nlinarith [sq_nonneg x]
+  have hdy : 1 + y ^ 2 ≠ 0 := by nlinarith [sq_nonneg y]
+  rw [hsinA, hcosS] at hclosure
+  field_simp [hdx, hdy] at hclosure
+  dsimp only [closurePolynomial]
+  linear_combination -hclosure
+
+lemma ra_eq_q_implies_pRQ (A B x y RA Q : ℝ)
+    (hA : 0 < A) (hApi : A < Real.pi)
+    (hS : 0 < A + B) (hSpi : A + B < Real.pi)
+    (hx : x = Real.tan (A / 4)) (hy : y = Real.tan ((A + B) / 2))
+    (hRA : RA ^ 2 = 4 - 4 * Real.cos A - 2 * Real.cos B +
+      4 * Real.cos (A + B) - 2 * Real.cos (2 * A + B))
+    (hQ : Q ^ 2 = 3 - 2 * Real.cos A - 2 * Real.cos B + 2 * Real.cos (A + B))
+    (heq : RA = Q) : pRQ x y = 0 := by
+  obtain ⟨hsinHalf, hcosHalf, hsinS, hcosS⟩ :=
+    tan_dictionary A B x y hA hApi hS hSpi hx hy
+  have hdx : 1 + x ^ 2 ≠ 0 := by nlinarith [sq_nonneg x]
+  have hdy : 1 + y ^ 2 ≠ 0 := by nlinarith [sq_nonneg y]
+  subst RA
+  rw [cos_B_as_S_sub_A A B] at hRA hQ
+  rw [cos_twoA_add_B_as_S_add_A A B] at hRA
+  rw [cos_A_as_half A, sin_A_as_half A,
+    hsinHalf, hcosHalf, hsinS, hcosS] at hRA hQ
+  field_simp [hdx, hdy] at hRA hQ
+  dsimp only [pRQ]
+  linear_combination hRA - hQ
+
+lemma ra_eq_ec_implies_pRC (A B C x y RA eC : ℝ)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi)
+    (hA : 0 < A) (hApi : A < Real.pi)
+    (hS : 0 < A + B) (hSpi : A + B < Real.pi)
+    (hx : x = Real.tan (A / 4)) (hy : y = Real.tan ((A + B) / 2))
+    (hRA : RA ^ 2 = 4 - 4 * Real.cos A - 2 * Real.cos B +
+      4 * Real.cos (A + B) - 2 * Real.cos (2 * A + B))
+    (heC : eC = 2 * Real.sin (C / 2)) (heq : RA = eC) : pRC x y = 0 := by
+  obtain ⟨hsinHalf, hcosHalf, hsinS, hcosS⟩ :=
+    tan_dictionary A B x y hA hApi hS hSpi hx hy
+  have hdx : 1 + x ^ 2 ≠ 0 := by nlinarith [sq_nonneg x]
+  have hdy : 1 + y ^ 2 ≠ 0 := by nlinarith [sq_nonneg y]
+  have heCsq : eC ^ 2 = 2 - 2 * Real.cos C := by
+    rw [heC, two_sin_half_sq]
+  subst RA
+  rw [heCsq, cos_C_as_sin_halfA_add_S A B C hsum, Real.sin_add,
+    cos_B_as_S_sub_A A B, cos_twoA_add_B_as_S_add_A A B,
+    cos_A_as_half A, sin_A_as_half A,
+    hsinHalf, hcosHalf, hsinS, hcosS] at hRA
+  field_simp [hdx, hdy] at hRA
+  dsimp only [pRC]
+  linear_combination hRA / 2
+
+lemma rb_eq_ec_implies_pBC (A B C x y RB eC : ℝ)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi)
+    (hA : 0 < A) (hApi : A < Real.pi)
+    (hS : 0 < A + B) (hSpi : A + B < Real.pi)
+    (hx : x = Real.tan (A / 4)) (hy : y = Real.tan ((A + B) / 2))
+    (hRB : RB ^ 2 = 4 - 2 * Real.cos A - 4 * Real.cos B +
+      4 * Real.cos (A + B) - 2 * Real.cos (A + 2 * B))
+    (heC : eC = 2 * Real.sin (C / 2)) (heq : RB = eC) : pBC x y = 0 := by
+  obtain ⟨hsinHalf, hcosHalf, hsinS, hcosS⟩ :=
+    tan_dictionary A B x y hA hApi hS hSpi hx hy
+  have hdx : 1 + x ^ 2 ≠ 0 := by nlinarith [sq_nonneg x]
+  have hdy : 1 + y ^ 2 ≠ 0 := by nlinarith [sq_nonneg y]
+  have heCsq : eC ^ 2 = 2 - 2 * Real.cos C := by
+    rw [heC, two_sin_half_sq]
+  subst RB
+  rw [heCsq, cos_C_as_sin_halfA_add_S A B C hsum, Real.sin_add,
+    cos_B_as_S_sub_A A B, cos_A_add_twoB_as_twoS_sub_A A B,
+    cos_A_as_half A, sin_A_as_half A,
+    hsinHalf, hcosHalf, hsinS, hcosS] at hRB
+  field_simp [hdx, hdy] at hRB
+  dsimp only [pBC]
+  linear_combination hRB / 2
+
+lemma rb_eq_ea_implies_pBA (A B x y RB eA : ℝ)
+    (hA : 0 < A) (hApi : A < Real.pi)
+    (hS : 0 < A + B) (hSpi : A + B < Real.pi)
+    (hx : x = Real.tan (A / 4)) (hy : y = Real.tan ((A + B) / 2))
+    (hRB : RB ^ 2 = 4 - 2 * Real.cos A - 4 * Real.cos B +
+      4 * Real.cos (A + B) - 2 * Real.cos (A + 2 * B))
+    (heA : eA = 2 * Real.sin (A / 2)) (heq : RB = eA) : pBA x y = 0 := by
+  obtain ⟨hsinHalf, hcosHalf, hsinS, hcosS⟩ :=
+    tan_dictionary A B x y hA hApi hS hSpi hx hy
+  have hdx : 1 + x ^ 2 ≠ 0 := by nlinarith [sq_nonneg x]
+  have hdy : 1 + y ^ 2 ≠ 0 := by nlinarith [sq_nonneg y]
+  subst RB
+  rw [heA, cos_B_as_S_sub_A A B, cos_A_add_twoB_as_twoS_sub_A A B,
+    cos_A_as_half A, sin_A_as_half A,
+    hsinHalf, hcosHalf, hsinS, hcosS] at hRB
+  field_simp [hdx, hdy] at hRB
+  dsimp only [pBA]
+  linear_combination -hRB / 16
+
+end LeanPool.Erdos132WeiE2.Algebra
diff --git a/LeanPool/Erdos132WeiE2/Algebra/G10.lean b/LeanPool/Erdos132WeiE2/Algebra/G10.lean
new file mode 100644
index 000000000..d494147f3
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Algebra/G10.lean
@@ -0,0 +1,83 @@
+/-
+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.Exclusions
+
+/-!
+# The strict E2 comparison between the C-edge and Q-diagonal
+
+This module derives `eC < Q` from the frozen trigonometric interface.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Algebra
+
+/-- The exact polynomial identity supplied with the amended G10 certificate. -/
+lemma g10_curve_identity (x y : ℝ) :
+    (-x ^ 4 * y ^ 2 - 4 * x ^ 4 * y - x ^ 4 - 4 * x ^ 3 * y ^ 2 +
+        16 * x ^ 3 * y + 4 * x ^ 3 - 2 * x ^ 2 * y ^ 2 + 30 * x ^ 2 -
+        4 * x * y ^ 2 - 16 * x * y + 4 * x - y ^ 2 + 4 * y - 1) =
+      -(x ^ 2 + 1) * closurePolynomial x y +
+        4 * (x ^ 2 - 4 * x + 1) * ((1 - x ^ 2) * y - 2 * x) := by
+  simp only [closurePolynomial]
+  ring
+
+/-- G10 from the amended explicit-real interface. -/
+lemma ec_lt_q_of_interface (A B C eC Q : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C) (hC : C < Real.pi / 3)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi)
+    (hclosure : 2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B)) = 1)
+    (heC : eC = 2 * Real.sin (C / 2))
+    (hQ : Q ^ 2 = 3 - 2 * Real.cos A - 2 * Real.cos B + 2 * Real.cos (A + B))
+    (heCnonneg : 0 ≤ eC) (hQnonneg : 0 ≤ Q) : eC < Q := by
+  have hA : 0 < A := lt_trans hB hBA
+  have hApiThird : A < Real.pi / 3 := lt_trans hAC hC
+  have hApi : A < Real.pi := by linarith [Real.pi_pos]
+  have hSpos : 0 < A + B := by linarith
+  have hSlt := add_lt_two_pi_div_three A B C hB hBA hAC hsum
+  have hsinHalfLt : Real.sin (A / 2) < 1 / 2 := by
+    rw [← Real.sin_pi_div_six]
+    exact Real.sin_lt_sin_of_lt_of_le_pi_div_two
+      (by linarith [Real.pi_pos]) (by linarith [Real.pi_pos]) (by linarith)
+  have hcosSHalf : 0 < Real.cos ((A + B) / 2) :=
+    Real.cos_pos_of_mem_Ioo ⟨by linarith [Real.pi_pos], by linarith [Real.pi_pos]⟩
+  have hsinBHalf : 0 < Real.sin (B / 2) :=
+    Real.sin_pos_of_pos_of_lt_pi (by linarith) (by linarith [Real.pi_pos])
+  have heCsq : eC ^ 2 = 2 - 2 * Real.cos C := by
+    rw [heC, two_sin_half_sq]
+  have hsinSdouble : Real.sin (A + B) =
+      2 * Real.sin ((A + B) / 2) * Real.cos ((A + B) / 2) := by
+    calc
+      Real.sin (A + B) = Real.sin (2 * ((A + B) / 2)) := by congr 1; ring
+      _ = _ := Real.sin_two_mul ((A + B) / 2)
+  have hcosSdouble : Real.cos (A + B) =
+      2 * Real.cos ((A + B) / 2) ^ 2 - 1 := by
+    calc
+      Real.cos (A + B) = Real.cos (2 * ((A + B) / 2)) := by congr 1; ring
+      _ = _ := Real.cos_two_mul ((A + B) / 2)
+  have hsinBsub : Real.sin (B / 2) =
+      Real.sin ((A + B) / 2) * Real.cos (A / 2) -
+        Real.cos ((A + B) / 2) * Real.sin (A / 2) := by
+    calc
+      Real.sin (B / 2) = Real.sin ((A + B) / 2 - A / 2) := by congr 1; ring
+      _ = _ := by rw [Real.sin_sub]
+  have hclosure' := hclosure
+  rw [hcosSdouble] at hclosure'
+  have hdiff : Q ^ 2 - eC ^ 2 =
+      4 * (1 - 2 * Real.sin (A / 2)) * Real.cos ((A + B) / 2) *
+        Real.sin (B / 2) := by
+    rw [hQ, heCsq, cos_C_as_sin_halfA_add_S A B C hsum, Real.sin_add,
+      cos_B_as_S_sub_A A B, cos_A_as_half A, sin_A_as_half A,
+      hsinSdouble, hcosSdouble, hsinBsub]
+    linear_combination hclosure' -
+      8 * Real.cos ((A + B) / 2) ^ 2 * (Real.sin_sq_add_cos_sq (A / 2))
+  have hfactor1 : 0 < 1 - 2 * Real.sin (A / 2) := by linarith
+  have hproduct : 0 <
+      4 * (1 - 2 * Real.sin (A / 2)) * Real.cos ((A + B) / 2) *
+        Real.sin (B / 2) := by
+    exact mul_pos (mul_pos (by positivity) hcosSHalf) hsinBHalf
+  have hsq : eC ^ 2 < Q ^ 2 := by linarith
+  exact lt_of_sq_lt_sq_of_nonneg hsq heCnonneg hQnonneg
+
+end LeanPool.Erdos132WeiE2.Algebra
diff --git a/LeanPool/Erdos132WeiE2/Algebra/Ranges.lean b/LeanPool/Erdos132WeiE2/Algebra/Ranges.lean
new file mode 100644
index 000000000..7315693cf
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Algebra/Ranges.lean
@@ -0,0 +1,67 @@
+/-
+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.Analysis.SpecialFunctions.Trigonometric.Basic
+
+/-!
+# Angle ranges for the E2 parametrization
+
+This module derives the linear angle inequalities used by the E2 algebraic argument.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Algebra
+
+/-- Linear angle consequences of the frozen E2 algebra interface. -/
+lemma angle_ranges (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    A + B < 2 * Real.pi / 3 ∧
+      2 * A + B < Real.pi ∧
+      0 < A + 2 * B ∧
+      A + 2 * B < 2 * A + B ∧
+      3 * A + 2 * B < Real.pi := by
+  have hA : 0 < A := lt_trans hB hBA
+  have hthree : 3 * A + 2 * B < Real.pi := by linarith
+  constructor
+  · linarith [Real.pi_pos]
+  constructor
+  · linarith
+  constructor
+  · linarith
+  constructor
+  · linarith
+  · exact hthree
+
+lemma add_lt_two_pi_div_three (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    A + B < 2 * Real.pi / 3 :=
+  (angle_ranges A B C hB hBA hAC hsum).1
+
+lemma two_mul_add_lt_pi (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    2 * A + B < Real.pi :=
+  (angle_ranges A B C hB hBA hAC hsum).2.1
+
+lemma add_two_mul_pos (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    0 < A + 2 * B :=
+  (angle_ranges A B C hB hBA hAC hsum).2.2.1
+
+lemma add_two_mul_lt_two_mul_add (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    A + 2 * B < 2 * A + B :=
+  (angle_ranges A B C hB hBA hAC hsum).2.2.2.1
+
+lemma three_mul_add_lt_pi (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    3 * A + 2 * B < Real.pi :=
+  (angle_ranges A B C hB hBA hAC hsum).2.2.2.2
+
+end LeanPool.Erdos132WeiE2.Algebra
diff --git a/LeanPool/Erdos132WeiE2/Algebra/TanExpressions.lean b/LeanPool/Erdos132WeiE2/Algebra/TanExpressions.lean
new file mode 100644
index 000000000..f8a6d471d
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Algebra/TanExpressions.lean
@@ -0,0 +1,63 @@
+/-
+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.TrigSigns
+
+/-!
+# Tangent expressions for the E2 parametrization
+
+This module rewrites the relevant angles into the half-angle forms used by the algebraic proof.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Algebra
+
+lemma cos_A_as_half (A : ℝ) :
+    Real.cos A = 2 * Real.cos (A / 2) ^ 2 - 1 := by
+  calc
+    Real.cos A = Real.cos (2 * (A / 2)) := by congr 1; ring
+    _ = _ := Real.cos_two_mul (A / 2)
+
+lemma sin_A_as_half (A : ℝ) :
+    Real.sin A = 2 * Real.sin (A / 2) * Real.cos (A / 2) := by
+  calc
+    Real.sin A = Real.sin (2 * (A / 2)) := by congr 1; ring
+    _ = _ := Real.sin_two_mul (A / 2)
+
+lemma cos_B_as_S_sub_A (A B : ℝ) :
+    Real.cos B = Real.cos (A + B) * Real.cos A + Real.sin (A + B) * Real.sin A := by
+  calc
+    Real.cos B = Real.cos ((A + B) - A) := by congr 1; ring
+    _ = _ := by rw [Real.cos_sub]
+
+lemma cos_twoA_add_B_as_S_add_A (A B : ℝ) :
+    Real.cos (2 * A + B) =
+      Real.cos (A + B) * Real.cos A - Real.sin (A + B) * Real.sin A := by
+  calc
+    Real.cos (2 * A + B) = Real.cos ((A + B) + A) := by congr 1; ring
+    _ = _ := by rw [Real.cos_add]
+
+lemma cos_A_add_twoB_as_twoS_sub_A (A B : ℝ) :
+    Real.cos (A + 2 * B) =
+      (2 * Real.cos (A + B) ^ 2 - 1) * Real.cos A +
+        (2 * Real.sin (A + B) * Real.cos (A + B)) * Real.sin A := by
+  calc
+    Real.cos (A + 2 * B) = Real.cos (2 * (A + B) - A) := by congr 1; ring
+    _ = Real.cos (2 * (A + B)) * Real.cos A +
+        Real.sin (2 * (A + B)) * Real.sin A := by rw [Real.cos_sub]
+    _ = _ := by rw [Real.cos_two_mul, Real.sin_two_mul]
+
+lemma cos_C_as_sin_halfA_add_S (A B C : ℝ)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    Real.cos C = Real.sin (A / 2 + (A + B)) := by
+  have hC : C = Real.pi / 2 - (A / 2 + (A + B)) := by linarith
+  rw [hC, Real.cos_pi_div_two_sub]
+
+lemma two_sin_half_sq (C : ℝ) :
+    (2 * Real.sin (C / 2)) ^ 2 = 2 - 2 * Real.cos C := by
+  have hcos := Real.cos_two_mul_eq_one_sub (C / 2)
+  rw [show 2 * (C / 2) = C by ring] at hcos
+  nlinarith
+
+end LeanPool.Erdos132WeiE2.Algebra
diff --git a/LeanPool/Erdos132WeiE2/Algebra/TrigSigns.lean b/LeanPool/Erdos132WeiE2/Algebra/TrigSigns.lean
new file mode 100644
index 000000000..a5927364e
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Algebra/TrigSigns.lean
@@ -0,0 +1,146 @@
+/-
+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.Ranges
+
+/-!
+# Trigonometric signs for the E2 parametrization
+
+This module proves the trigonometric identities and sign inequalities used in the exclusions.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Algebra
+
+lemma ra_sq_sub_ea_sq_identity (A B : ℝ) :
+    (4 - 4 * Real.cos A - 2 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (2 * A + B)) - (2 * Real.sin (A / 2)) ^ 2 =
+      4 * (Real.sin (A / 2)) ^ 2 * (1 + 2 * Real.cos (A + B)) := by
+  have hcosA : Real.cos A = 1 - 2 * (Real.sin (A / 2)) ^ 2 := by
+    calc
+      Real.cos A = Real.cos (2 * (A / 2)) := by congr 1; ring
+      _ = 1 - 2 * (Real.sin (A / 2)) ^ 2 := Real.cos_two_mul_eq_one_sub (A / 2)
+  have hsinA : Real.sin A = 2 * Real.sin (A / 2) * Real.cos (A / 2) := by
+    calc
+      Real.sin A = Real.sin (2 * (A / 2)) := by congr 1; ring
+      _ = 2 * Real.sin (A / 2) * Real.cos (A / 2) := Real.sin_two_mul (A / 2)
+  have hcosB : Real.cos B =
+      Real.cos (A + B) * Real.cos A + Real.sin (A + B) * Real.sin A := by
+    calc
+      Real.cos B = Real.cos ((A + B) - A) := by congr 1; ring
+      _ = _ := by rw [Real.cos_sub]
+  have hcosTwo : Real.cos (2 * A + B) =
+      Real.cos (A + B) * Real.cos A - Real.sin (A + B) * Real.sin A := by
+    calc
+      Real.cos (2 * A + B) = Real.cos ((A + B) + A) := by congr 1; ring
+      _ = _ := by rw [Real.cos_add]
+  rw [hcosB, hcosTwo, hcosA, hsinA]
+  ring
+
+lemma rb_sq_sub_eb_sq_identity (A B : ℝ) :
+    (4 - 2 * Real.cos A - 4 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (A + 2 * B)) - (2 * Real.sin (B / 2)) ^ 2 =
+      4 * (Real.sin (B / 2)) ^ 2 * (1 + 2 * Real.cos (A + B)) := by
+  have hcosB : Real.cos B = 1 - 2 * (Real.sin (B / 2)) ^ 2 := by
+    calc
+      Real.cos B = Real.cos (2 * (B / 2)) := by congr 1; ring
+      _ = 1 - 2 * (Real.sin (B / 2)) ^ 2 := Real.cos_two_mul_eq_one_sub (B / 2)
+  have hsinB : Real.sin B = 2 * Real.sin (B / 2) * Real.cos (B / 2) := by
+    calc
+      Real.sin B = Real.sin (2 * (B / 2)) := by congr 1; ring
+      _ = 2 * Real.sin (B / 2) * Real.cos (B / 2) := Real.sin_two_mul (B / 2)
+  have hcosA : Real.cos A =
+      Real.cos (A + B) * Real.cos B + Real.sin (A + B) * Real.sin B := by
+    calc
+      Real.cos A = Real.cos ((A + B) - B) := by congr 1; ring
+      _ = _ := by rw [Real.cos_sub]
+  have hcosTwo : Real.cos (A + 2 * B) =
+      Real.cos (A + B) * Real.cos B - Real.sin (A + B) * Real.sin B := by
+    calc
+      Real.cos (A + 2 * B) = Real.cos ((A + B) + B) := by congr 1; ring
+      _ = _ := by rw [Real.cos_add]
+  rw [hcosA, hcosTwo, hcosB, hsinB]
+  ring
+
+lemma ra_sq_sub_rb_sq_identity (A B : ℝ) :
+    (4 - 4 * Real.cos A - 2 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (2 * A + B)) -
+      (4 - 2 * Real.cos A - 4 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (A + 2 * B)) =
+      2 * ((Real.cos B - Real.cos A) +
+        (Real.cos (A + 2 * B) - Real.cos (2 * A + B))) := by
+  ring
+
+lemma one_add_two_cos_pos {A B : ℝ} (hpos : 0 < A + B)
+    (hlt : A + B < 2 * Real.pi / 3) :
+    0 < 1 + 2 * Real.cos (A + B) := by
+  have hangle : A + B < Real.pi - Real.pi / 3 := by linarith
+  have hcos := Real.cos_lt_cos_of_nonneg_of_le_pi
+    (le_of_lt hpos) (show Real.pi - Real.pi / 3 ≤ Real.pi by linarith [Real.pi_pos]) hangle
+  rw [Real.cos_pi_sub, Real.cos_pi_div_three] at hcos
+  linarith
+
+lemma cos_B_gt_cos_A {A B : ℝ} (hB : 0 < B) (hBA : B < A) (hApi : A < Real.pi) :
+    Real.cos A < Real.cos B :=
+  Real.cos_lt_cos_of_nonneg_of_le_pi (le_of_lt hB) (le_of_lt hApi) hBA
+
+lemma cos_add_two_mul_gt_cos_two_mul_add {A B : ℝ}
+    (hpos : 0 < A + 2 * B) (hlt : A + 2 * B < 2 * A + B)
+    (hpi : 2 * A + B < Real.pi) :
+    Real.cos (2 * A + B) < Real.cos (A + 2 * B) :=
+  Real.cos_lt_cos_of_nonneg_of_le_pi (le_of_lt hpos) (le_of_lt hpi) hlt
+
+lemma sin_half_pos {X : ℝ} (hX : 0 < X) (hXpi : X < Real.pi) :
+    0 < Real.sin (X / 2) :=
+  Real.sin_pos_of_pos_of_lt_pi (by linarith) (by linarith [Real.pi_pos])
+
+lemma sin_A_half_pos {A : ℝ} (hA : 0 < A) (hApi : A < Real.pi) :
+    0 < Real.sin (A / 2) := sin_half_pos hA hApi
+
+lemma sin_B_half_pos {B : ℝ} (hB : 0 < B) (hBpi : B < Real.pi) :
+    0 < Real.sin (B / 2) := sin_half_pos hB hBpi
+
+lemma sin_C_half_pos {C : ℝ} (hC : 0 < C) (hCpi : C < Real.pi) :
+    0 < Real.sin (C / 2) := sin_half_pos hC hCpi
+
+lemma ra_sq_gt_ea_sq (RA eA A B : ℝ)
+    (hid : RA ^ 2 - eA ^ 2 =
+      4 * (Real.sin (A / 2)) ^ 2 * (1 + 2 * Real.cos (A + B)))
+    (hsin : 0 < Real.sin (A / 2)) (hcos : 0 < 1 + 2 * Real.cos (A + B)) :
+    eA ^ 2 < RA ^ 2 := by
+  nlinarith [sq_pos_of_pos hsin]
+
+lemma rb_sq_gt_eb_sq (RB eB A B : ℝ)
+    (hid : RB ^ 2 - eB ^ 2 =
+      4 * (Real.sin (B / 2)) ^ 2 * (1 + 2 * Real.cos (A + B)))
+    (hsin : 0 < Real.sin (B / 2)) (hcos : 0 < 1 + 2 * Real.cos (A + B)) :
+    eB ^ 2 < RB ^ 2 := by
+  nlinarith [sq_pos_of_pos hsin]
+
+lemma ra_sq_gt_rb_sq (RA RB A B : ℝ)
+    (hid : RA ^ 2 - RB ^ 2 =
+      2 * ((Real.cos B - Real.cos A) +
+        (Real.cos (A + 2 * B) - Real.cos (2 * A + B))))
+    (hcosBA : Real.cos A < Real.cos B)
+    (hcosAdd : Real.cos (2 * A + B) < Real.cos (A + 2 * B)) :
+    RB ^ 2 < RA ^ 2 := by
+  linarith
+
+lemma lt_of_sq_lt_sq_of_nonneg {a b : ℝ} (hsq : a ^ 2 < b ^ 2)
+    (ha : 0 ≤ a) (hb : 0 ≤ b) : a < b :=
+  (sq_lt_sq₀ ha hb).mp hsq
+
+lemma ra_gt_ea {RA eA : ℝ} (hsq : eA ^ 2 < RA ^ 2)
+    (hRA : 0 ≤ RA) (heA : 0 ≤ eA) : eA < RA :=
+  lt_of_sq_lt_sq_of_nonneg hsq heA hRA
+
+lemma rb_gt_eb {RB eB : ℝ} (hsq : eB ^ 2 < RB ^ 2)
+    (hRB : 0 ≤ RB) (heB : 0 ≤ eB) : eB < RB :=
+  lt_of_sq_lt_sq_of_nonneg hsq heB hRB
+
+lemma ra_gt_rb {RA RB : ℝ} (hsq : RB ^ 2 < RA ^ 2)
+    (hRA : 0 ≤ RA) (hRB : 0 ≤ RB) : RB < RA :=
+  lt_of_sq_lt_sq_of_nonneg hsq hRB hRA
+
+end LeanPool.Erdos132WeiE2.Algebra
diff --git a/LeanPool/Erdos132WeiE2/Counting/Assembly.lean b/LeanPool/Erdos132WeiE2/Counting/Assembly.lean
new file mode 100644
index 000000000..2e1673905
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Counting/Assembly.lean
@@ -0,0 +1,143 @@
+/-
+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.G10
+import LeanPool.Erdos132WeiE2.Counting.Endgame
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+/-!
+# Six-distance assembly for the E2 diameter-heptagon pattern
+
+This module combines the algebraic exclusions and finite counting endgame.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Counting
+
+open LeanPool.Erdos132WeiE2.Algebra
+
+theorem six_distances_of_parametrization
+    (p : Fin 7 → EuclideanSpace ℝ (Fin 2))
+    (h03 : dist (p 0) (p 3) = 1)
+    (hs02 : dist (p 0) (p 2) < 1) (hs05 : dist (p 0) (p 5) < 1)
+    (hBAe : dist (p 1) (p 2) < dist (p 4) (p 5))
+    (hACe : dist (p 4) (p 5) < dist (p 0) (p 1))
+    (A B C : ℝ)
+    (hB : 0 < B) (hBA : B < A) (hAC : A < C) (hCpi : C < Real.pi / 3)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi)
+    (hclosure : 2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B)) = 1)
+    (heC : dist (p 0) (p 1) = 2 * Real.sin (C / 2))
+    (heB : dist (p 1) (p 2) = 2 * Real.sin (B / 2))
+    (heA : dist (p 4) (p 5) = 2 * Real.sin (A / 2))
+    (hQ : (dist (p 0) (p 2)) ^ 2 =
+      3 - 2 * Real.cos A - 2 * Real.cos B + 2 * Real.cos (A + B))
+    (hRA : (dist (p 0) (p 5)) ^ 2 =
+      4 - 4 * Real.cos A - 2 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (2 * A + B))
+    (hRB : (dist (p 1) (p 3)) ^ 2 =
+      4 - 2 * Real.cos A - 4 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (A + 2 * B)) :
+    6 ≤ ((Finset.univ.filter fun q : Fin 7 × Fin 7 => q.1 ≠ q.2).image
+      fun q => dist (p q.1) (p q.2)).card := by
+  let V : Finset ℝ :=
+    (Finset.univ.filter fun q : Fin 7 × Fin 7 => q.1 ≠ q.2).image
+      fun q => dist (p q.1) (p q.2)
+  let eB : ℝ := dist (p 1) (p 2)
+  let eA : ℝ := dist (p 4) (p 5)
+  let eC : ℝ := dist (p 0) (p 1)
+  let Q : ℝ := dist (p 0) (p 2)
+  let RA : ℝ := dist (p 0) (p 5)
+  let RB : ℝ := dist (p 1) (p 3)
+  have heCv : eC = 2 * Real.sin (C / 2) := heC
+  have heBv : eB = 2 * Real.sin (B / 2) := heB
+  have heAv : eA = 2 * Real.sin (A / 2) := heA
+  have hQv : Q ^ 2 =
+      3 - 2 * Real.cos A - 2 * Real.cos B + 2 * Real.cos (A + B) := hQ
+  have hRAv : RA ^ 2 =
+      4 - 4 * Real.cos A - 2 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (2 * A + B) := hRA
+  have hRBv : RB ^ 2 =
+      4 - 2 * Real.cos A - 4 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (A + 2 * B) := hRB
+  have mem_dist (i j : Fin 7) (hij : i ≠ j) : dist (p i) (p j) ∈ V := by
+    refine Finset.mem_image.mpr ⟨(i, j), ?_, rfl⟩
+    simp [hij]
+  have hmemB : eB ∈ V := mem_dist 1 2 (by decide)
+  have hmemA : eA ∈ V := mem_dist 4 5 (by decide)
+  have hmemC : eC ∈ V := mem_dist 0 1 (by decide)
+  have hmemQ : Q ∈ V := mem_dist 0 2 (by decide)
+  have hmemRA : RA ∈ V := mem_dist 0 5 (by decide)
+  have hmemRB : RB ∈ V := mem_dist 1 3 (by decide)
+  have hmem1 : (1 : ℝ) ∈ V := by
+    simpa only [h03] using mem_dist 0 3 (by decide)
+  have hApos : 0 < A := lt_trans hB hBA
+  have hApi : A < Real.pi := by linarith [Real.pi_pos]
+  have hSpos : 0 < A + B := by linarith
+  have hSltTwo := add_lt_two_pi_div_three A B C hB hBA hAC hsum
+  have hSpi : A + B < Real.pi := by linarith [Real.pi_pos]
+  have hTwoAlt := two_mul_add_lt_pi A B C hB hBA hAC hsum
+  have hAddTwoPos := add_two_mul_pos A B C hB hBA hAC hsum
+  have hAddTwoLt := add_two_mul_lt_two_mul_add A B C hB hBA hAC hsum
+  have hfactor : 0 < 1 + 2 * Real.cos (A + B) :=
+    one_add_two_cos_pos hSpos hSltTwo
+  have hsinA : 0 < Real.sin (A / 2) := sin_A_half_pos hApos hApi
+  have hBpi : B < Real.pi := by linarith
+  have hsinB : 0 < Real.sin (B / 2) := sin_B_half_pos hB hBpi
+  have hidRA : RA ^ 2 - eA ^ 2 =
+      4 * Real.sin (A / 2) ^ 2 * (1 + 2 * Real.cos (A + B)) := by
+    rw [hRAv, heAv]
+    exact ra_sq_sub_ea_sq_identity A B
+  have hidRB : RB ^ 2 - eB ^ 2 =
+      4 * Real.sin (B / 2) ^ 2 * (1 + 2 * Real.cos (A + B)) := by
+    rw [hRBv, heBv]
+    exact rb_sq_sub_eb_sq_identity A B
+  have hidRARB : RA ^ 2 - RB ^ 2 =
+      2 * ((Real.cos B - Real.cos A) +
+        (Real.cos (A + 2 * B) - Real.cos (2 * A + B))) := by
+    rw [hRAv, hRBv]
+    exact ra_sq_sub_rb_sq_identity A B
+  have hcosBA : Real.cos A < Real.cos B := cos_B_gt_cos_A hB hBA hApi
+  have hcosAdd : Real.cos (2 * A + B) < Real.cos (A + 2 * B) :=
+    cos_add_two_mul_gt_cos_two_mul_add hAddTwoPos hAddTwoLt hTwoAlt
+  have hRASq : eA ^ 2 < RA ^ 2 := ra_sq_gt_ea_sq RA eA A B hidRA hsinA hfactor
+  have hRBSq : eB ^ 2 < RB ^ 2 := rb_sq_gt_eb_sq RB eB A B hidRB hsinB hfactor
+  have hRARBSq : RB ^ 2 < RA ^ 2 :=
+    ra_sq_gt_rb_sq RA RB A B hidRARB hcosBA hcosAdd
+  have rA1 : eA < RA := ra_gt_ea hRASq dist_nonneg dist_nonneg
+  have rB1 : eB < RB := rb_gt_eb hRBSq dist_nonneg dist_nonneg
+  have rB2 : RB < RA := ra_gt_rb hRARBSq dist_nonneg dist_nonneg
+  have o3 : eC < Q := ec_lt_q_of_interface A B C eC Q hB hBA hAC hCpi hsum
+    hclosure heCv hQv dist_nonneg dist_nonneg
+  let x : ℝ := Real.tan (A / 4)
+  let y : ℝ := Real.tan ((A + B) / 2)
+  have hx : x = Real.tan (A / 4) := rfl
+  have hy : y = Real.tan ((A + B) / 2) := rfl
+  have hF' := closure_implies_polynomial A B x y hApos hApi hSpos hSpi hx hy hclosure
+  have hF : x ^ 2 * y ^ 2 + x ^ 2 + 4 * x * y ^ 2 - 12 * x + y ^ 2 + 1 = 0 := by
+    simpa only [closurePolynomial] using hF'
+  have x1 : ¬(RA = Q ∧ RB = eC) := by
+    rintro ⟨hRAQ, hRBeC⟩
+    have hpRQ := ra_eq_q_implies_pRQ A B x y RA Q hApos hApi hSpos hSpi hx hy
+      hRAv hQv hRAQ
+    have hpBC := rb_eq_ec_implies_pBC A B C x y RB eC hsum hApos hApi hSpos hSpi
+      hx hy hRBv heCv hRBeC
+    exact exclude_ra_q_rb_ec x y hF hpRQ hpBC
+  have x2 : ¬(RA = Q ∧ RB = eA) := by
+    rintro ⟨hRAQ, hRBeA⟩
+    have hpRQ := ra_eq_q_implies_pRQ A B x y RA Q hApos hApi hSpos hSpi hx hy
+      hRAv hQv hRAQ
+    have hpBA := rb_eq_ea_implies_pBA A B x y RB eA hApos hApi hSpos hSpi hx hy
+      hRBv heAv hRBeA
+    exact exclude_ra_q_rb_ea x y hF hpRQ hpBA
+  have x3 : ¬(RA = eC ∧ RB = eA) := by
+    rintro ⟨hRAeC, hRBeA⟩
+    have hpRC := ra_eq_ec_implies_pRC A B C x y RA eC hsum hApos hApi hSpos hSpi
+      hx hy hRAv heCv hRAeC
+    have hpBA := rb_eq_ea_implies_pBA A B x y RB eA hApos hApi hSpos hSpi hx hy
+      hRBv heAv hRBeA
+    exact exclude_ra_ec_rb_ea x y hF hpRC hpBA
+  exact six_le_card_of_values V eB eA eC Q RA RB hmemB hmemA hmemC hmemQ hmem1
+    hmemRA hmemRB hBAe hACe o3 hs02 rA1 hs05 rB1 rB2 x1 x2 x3
+
+end LeanPool.Erdos132WeiE2.Counting
diff --git a/LeanPool/Erdos132WeiE2/Counting/Endgame.lean b/LeanPool/Erdos132WeiE2/Counting/Endgame.lean
new file mode 100644
index 000000000..5a4c0b1ca
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Counting/Endgame.lean
@@ -0,0 +1,113 @@
+/-
+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.Finset.Card
+import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.Linarith
+import Lean.Elab.Tactic.Omega
+
+/-!
+# Finite counting endgame for six distances
+
+This module turns the ordered distance values and exclusion cases into the final cardinality bound.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Counting
+
+lemma six_le_card_of_values (V : Finset ℝ) (eB eA eC Q RA RB : ℝ)
+    (hmemB : eB ∈ V) (hmemA : eA ∈ V) (hmemC : eC ∈ V) (hmemQ : Q ∈ V)
+    (hmem1 : (1 : ℝ) ∈ V) (hmemRA : RA ∈ V) (hmemRB : RB ∈ V)
+    (o1 : eB < eA) (o2 : eA < eC) (o3 : eC < Q) (o4 : Q < 1)
+    (rA1 : eA < RA) (rA2 : RA < 1) (rB1 : eB < RB) (rB2 : RB < RA)
+    (x1 : ¬(RA = Q ∧ RB = eC)) (x2 : ¬(RA = Q ∧ RB = eA))
+    (x3 : ¬(RA = eC ∧ RB = eA)) :
+    6 ≤ V.card := by
+  classical
+  let S : Finset ℝ := {eB, eA, eC, Q, 1}
+  have hBnot : eB ∉ ({eA, eC, Q, (1 : ℝ)} : Finset ℝ) := by
+    simp only [Finset.mem_insert, Finset.mem_singleton, not_or]
+    constructor
+    · linarith
+    constructor
+    · linarith
+    constructor <;> linarith
+  have hAnot : eA ∉ ({eC, Q, (1 : ℝ)} : Finset ℝ) := by
+    simp only [Finset.mem_insert, Finset.mem_singleton, not_or]
+    constructor
+    · linarith
+    constructor <;> linarith
+  have hCnot : eC ∉ ({Q, (1 : ℝ)} : Finset ℝ) := by
+    simp only [Finset.mem_insert, Finset.mem_singleton, not_or]
+    constructor <;> linarith
+  have hQnot : Q ∉ ({(1 : ℝ)} : Finset ℝ) := by
+    simpa only [Finset.mem_singleton] using ne_of_lt o4
+  have hScard : S.card = 5 := by
+    simp [S, hBnot, hAnot, hCnot, hQnot]
+  have hSsub : S ⊆ V := by
+    intro z hz
+    simp only [S, Finset.mem_insert, Finset.mem_singleton] at hz
+    rcases hz with rfl | rfl | rfl | rfl | rfl
+    · exact hmemB
+    · exact hmemA
+    · exact hmemC
+    · exact hmemQ
+    · exact hmem1
+  by_contra hcard
+  have hVcard : V.card < 6 := Nat.lt_of_not_ge hcard
+  have hRAin : RA ∈ S := by
+    by_contra hnot
+    have hinsSub : insert RA S ⊆ V := by
+      intro z hz
+      rw [Finset.mem_insert] at hz
+      rcases hz with rfl | hz
+      · exact hmemRA
+      · exact hSsub hz
+    have hinsCard : (insert RA S).card = 6 := by
+      rw [Finset.card_insert_of_notMem hnot, hScard]
+    have := Finset.card_le_card hinsSub
+    omega
+  have hRBin : RB ∈ S := by
+    by_contra hnot
+    have hinsSub : insert RB S ⊆ V := by
+      intro z hz
+      rw [Finset.mem_insert] at hz
+      rcases hz with rfl | hz
+      · exact hmemRB
+      · exact hSsub hz
+    have hinsCard : (insert RB S).card = 6 := by
+      rw [Finset.card_insert_of_notMem hnot, hScard]
+    have := Finset.card_le_card hinsSub
+    omega
+  have hRAcases : RA = eC ∨ RA = Q := by
+    simp only [S, Finset.mem_insert, Finset.mem_singleton] at hRAin
+    rcases hRAin with h | h | h | h | h
+    · exfalso; linarith
+    · exfalso; linarith
+    · exact Or.inl h
+    · exact Or.inr h
+    · exfalso; linarith
+  rcases hRAcases with hRAeC | hRAQ
+  · have hRBeA : RB = eA := by
+      simp only [S, Finset.mem_insert, Finset.mem_singleton] at hRBin
+      rcases hRBin with h | h | h | h | h
+      · exfalso; linarith
+      · exact h
+      · exfalso; linarith
+      · exfalso; linarith
+      · exfalso; linarith
+    exact x3 ⟨hRAeC, hRBeA⟩
+  · have hRBcases : RB = eA ∨ RB = eC := by
+      simp only [S, Finset.mem_insert, Finset.mem_singleton] at hRBin
+      rcases hRBin with h | h | h | h | h
+      · exfalso; linarith
+      · exact Or.inl h
+      · exact Or.inr h
+      · exfalso; linarith
+      · exfalso; linarith
+    rcases hRBcases with hRBeA | hRBeC
+    · exact x2 ⟨hRAQ, hRBeA⟩
+    · exact x1 ⟨hRAQ, hRBeC⟩
+
+end LeanPool.Erdos132WeiE2.Counting
diff --git a/LeanPool/Erdos132WeiE2/Final.lean b/LeanPool/Erdos132WeiE2/Final.lean
new file mode 100644
index 000000000..7343a9b22
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Final.lean
@@ -0,0 +1,45 @@
+/-
+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.Geometry.Parametrization
+import LeanPool.Erdos132WeiE2.Counting.Assembly
+
+/-!
+# Final E2 six-distance theorem
+
+This module derives the repaired geometric E2 conclusion from the original hypotheses.
+-/
+
+namespace LeanPool.Erdos132WeiE2
+
+/-- The E2 diameter-heptagon pattern realizes at least six distinct pairwise distances.
+
+This is the independently significant repaired E2 step of Wei–Li–Cong–Gao 2014
+(doi:10.11650/tjm.18.2014.4030, Theorem 4, Part III, Case 2); it does not completely solve
+Erdős problem 132. Exact-arithmetic companion: github.com/lyfar/erdos132-wei-certificates. -/
+theorem e2_pattern_six_distances
+    (p : Fin 7 → EuclideanSpace ℝ (Fin 2))
+    (hdiam : ∀ i : Fin 7, dist (p i) (p (i + 3)) = 1)
+    (hshort : ∀ i j : Fin 7, i ≠ j → j ≠ i + 3 → i ≠ j + 3 → dist (p i) (p j) < 1)
+    (hC : dist (p 0) (p 1) = dist (p 3) (p 4))
+    (hB : dist (p 1) (p 2) = dist (p 2) (p 3))
+    (hA₁ : dist (p 4) (p 5) = dist (p 5) (p 6))
+    (hA₂ : dist (p 5) (p 6) = dist (p 6) (p 0))
+    (hBA : dist (p 1) (p 2) < dist (p 4) (p 5))
+    (hAC : dist (p 4) (p 5) < dist (p 0) (p 1)) :
+    6 ≤ ((Finset.univ.filter fun q : Fin 7 × Fin 7 => q.1 ≠ q.2).image
+      fun q => dist (p q.1) (p q.2)).card := by
+  obtain ⟨A, B, C, hpar⟩ :=
+    LeanPool.Erdos132WeiE2.Geometry.e2_angle_parametrization
+      p hdiam hshort hC hB hA₁ hA₂ hBA hAC
+  exact LeanPool.Erdos132WeiE2.Counting.six_distances_of_parametrization
+    p (hdiam 0)
+    (hshort 0 2 (by decide) (by decide) (by decide))
+    (hshort 0 5 (by decide) (by decide) (by decide))
+    hBA hAC A B C hpar.B_pos hpar.B_lt_A hpar.A_lt_C hpar.C_lt_pi_div_three
+    hpar.angle_sum hpar.closure hpar.edgeC hpar.edgeB hpar.edgeA hpar.q_sq hpar.ra_sq hpar.rb_sq
+
+end LeanPool.Erdos132WeiE2
diff --git a/LeanPool/Erdos132WeiE2/Geometry/Basic.lean b/LeanPool/Erdos132WeiE2/Geometry/Basic.lean
new file mode 100644
index 000000000..feec2e079
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Geometry/Basic.lean
@@ -0,0 +1,156 @@
+/-
+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.Analysis.Convex.Segment
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Geometry.Euclidean.Congruence
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Lean.Elab.Tactic.Omega
+
+/-!
+# Basic geometry for the Wei E2 configuration
+
+This file fixes the challenge point type, the diameter-star indexing, and the
+raw geometric hypotheses used by the angle-parametrization route.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Geometry
+
+open EuclideanGeometry
+
+/-- The plane used by the challenge statement. -/
+abbrev Plane := EuclideanSpace ℝ (Fin 2)
+
+/-- The standard real-linear isometry from the complex plane to the challenge plane. -/
+noncomputable def complexPlaneEquiv : ℂ ≃ₗᵢ[ℝ] Plane :=
+  Complex.isometryOfOrthonormal (EuclideanSpace.basisFun (Fin 2) ℝ)
+
+/-- Complex coordinates of a point in the challenge plane. -/
+noncomputable def toComplex (x : Plane) : ℂ := complexPlaneEquiv.symm x
+
+/-- Signed doubled area, transported through the standard Complex isometry. -/
+noncomputable def orientedArea (a b c : Plane) : ℝ :=
+  let u := toComplex b - toComplex a
+  let v := toComplex c - toComplex a
+  u.re * v.im - u.im * v.re
+
+/-- The order in which the seven diameter edges form their cycle. -/
+def walkIndex (i : Fin 7) : Fin 7 := 3 * i
+
+/-- The angle between the two unit diameter edges incident at vertex `i`. -/
+noncomputable def apexAngle (p : Fin 7 → Plane) (i : Fin 7) : ℝ :=
+  ∠ (p (i + 3)) (p i) (p (i + 4))
+
+/-- The geometric and edge-class hypotheses copied from the challenge. -/
+structure E2GeometryHypotheses (p : Fin 7 → Plane) : Prop where
+  hdiam : ∀ i : Fin 7, dist (p i) (p (i + 3)) = 1
+  hshort : ∀ i j : Fin 7, i ≠ j → j ≠ i + 3 → i ≠ j + 3 → dist (p i) (p j) < 1
+  hC : dist (p 0) (p 1) = dist (p 3) (p 4)
+  hB : dist (p 1) (p 2) = dist (p 2) (p 3)
+  hA₁ : dist (p 4) (p 5) = dist (p 5) (p 6)
+  hA₂ : dist (p 5) (p 6) = dist (p 6) (p 0)
+  hBA : dist (p 1) (p 2) < dist (p 4) (p 5)
+  hAC : dist (p 4) (p 5) < dist (p 0) (p 1)
+
+/-- One of the two diameter partners of `i` is not a diameter partner of a
+different index `j`. This is a finite fact about the seven-cycle. -/
+private theorem exists_diameter_partner_avoiding
+    (i j : Fin 7) (hij : i ≠ j) :
+    ∃ k : Fin 7,
+      (k = i + 3 ∨ i = k + 3) ∧ k ≠ j ∧ k ≠ j + 3 ∧ j ≠ k + 3 := by
+  revert hij
+  fin_cases i <;> fin_cases j <;> decide
+
+/-- The challenge hypotheses force all seven labelled points to be distinct. -/
+theorem pairwise_distinct_of_diameter_pattern
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) : Function.Injective p := by
+  intro i j hp
+  by_contra hij
+  obtain ⟨k, hik, hkj, hkj3, hjk3⟩ := exists_diameter_partner_avoiding i j hij
+  have hdik : dist (p i) (p k) = 1 := by
+    rcases hik with hik | hik
+    · simpa [hik] using h.hdiam i
+    · simpa [hik, dist_comm] using h.hdiam k
+  have hdjk : dist (p j) (p k) = 1 := by simpa [hp] using hdik
+  have hshort := h.hshort j k hkj.symm hkj3 hjk3
+  linarith
+
+/-- Every distance is bounded by the common diameter. -/
+theorem dist_le_one_of_diameter_pattern
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i j : Fin 7) :
+    dist (p i) (p j) ≤ 1 := by
+  by_cases hij : i = j
+  · subst j
+    simp
+  by_cases hj : j = i + 3
+  · exact (show dist (p i) (p j) = 1 by simpa [hj] using h.hdiam i).le
+  by_cases hi : i = j + 3
+  · exact (show dist (p i) (p j) = 1 by simpa [hi, dist_comm] using h.hdiam j).le
+  exact (h.hshort i j hij hj hi).le
+
+/-- Distance one occurs exactly on the two orientations of the labelled
+diameter cycle. -/
+theorem dist_eq_one_iff_diameter_related
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i j : Fin 7) :
+    dist (p i) (p j) = 1 ↔ j = i + 3 ∨ i = j + 3 := by
+  constructor
+  · intro hd
+    by_contra hrelated
+    have hij : i ≠ j := by
+      intro hij
+      subst j
+      rw [dist_self] at hd
+      exact zero_ne_one hd
+    have hj : j ≠ i + 3 := fun hj ↦ hrelated (Or.inl hj)
+    have hi : i ≠ j + 3 := fun hi ↦ hrelated (Or.inr hi)
+    have hshort := h.hshort i j hij hj hi
+    linarith
+  · rintro (hj | hi)
+    · simpa [hj] using h.hdiam i
+    · simpa [hi, dist_comm] using h.hdiam j
+
+/-- Every apex triangle is nondegenerate. -/
+theorem apex_not_collinear
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7) :
+    ¬Collinear ℝ ({p (i + 3), p i, p (i + 4)} : Set Plane) := by
+  intro hcollinear
+  have hinjective := pairwise_distinct_of_diameter_pattern h
+  have hleft : p (i + 3) ≠ p i := by
+    intro heq
+    have := hinjective heq
+    omega
+  have hright : p (i + 4) ≠ p i := by
+    intro heq
+    have := hinjective heq
+    omega
+  have hends : p (i + 3) ≠ p (i + 4) := by
+    intro heq
+    have := hinjective heq
+    omega
+  have hleftDist : dist (p (i + 3)) (p i) = 1 := by
+    simpa [dist_comm] using h.hdiam i
+  have hrightDist : dist (p (i + 4)) (p i) = 1 := by
+    have hindex : (i + 4) + 3 = i := by omega
+    simpa [hindex] using h.hdiam (i + 4)
+  have hbase : dist (p (i + 3)) (p (i + 4)) < 1 :=
+    h.hshort (i + 3) (i + 4) (by omega) (by omega) (by omega)
+  rcases
+      (collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi.mp hcollinear) with
+    hbad | hbad | hzero | hpi
+  · exact hleft hbad
+  · exact hright hbad
+  · have hcos := law_cos (p (i + 3)) (p i) (p (i + 4))
+    rw [hleftDist, hrightDist, hzero, Real.cos_zero] at hcos
+    have hdistZero : dist (p (i + 3)) (p (i + 4)) = 0 := by
+      have hnonneg : 0 ≤ dist (p (i + 3)) (p (i + 4)) := dist_nonneg
+      nlinarith
+    exact hends (dist_eq_zero.mp hdistZero)
+  · have hcos := law_cos (p (i + 3)) (p i) (p (i + 4))
+    rw [hleftDist, hrightDist, hpi, Real.cos_pi] at hcos
+    have hnonneg : 0 ≤ dist (p (i + 3)) (p (i + 4)) := dist_nonneg
+    nlinarith
+
+end LeanPool.Erdos132WeiE2.Geometry
diff --git a/LeanPool/Erdos132WeiE2/Geometry/Parametrization.lean b/LeanPool/Erdos132WeiE2/Geometry/Parametrization.lean
new file mode 100644
index 000000000..9d3a38d4e
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Geometry/Parametrization.lean
@@ -0,0 +1,1109 @@
+/-
+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.Geometry.Star
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+import Mathlib.Tactic.Ring
+
+/-!
+# Angle parametrization of the Wei E2 diameter star
+
+This module states the frozen geometry/algebra interface. The proof skeleton
+follows the certificate walk and does not use the broken E2 swap argument.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Geometry
+
+attribute [local instance] Complex.finrank_real_complex_fact
+
+/-- The seven apex angles have the certificate classes `C,A,A,A,C,B,B`. -/
+structure AngleClasses (p : Fin 7 → Plane) (A B C : ℝ) : Prop where
+  angle0 : apexAngle p 0 = C
+  angle1 : apexAngle p 1 = A
+  angle2 : apexAngle p 2 = A
+  angle3 : apexAngle p 3 = A
+  angle4 : apexAngle p 4 = C
+  angle5 : apexAngle p 5 = B
+  angle6 : apexAngle p 6 = B
+
+/-- The edge-length consequences of the three apex-angle classes. -/
+structure EdgeFormulas (p : Fin 7 → Plane) (A B C : ℝ) : Prop where
+  edgeC : dist (p 0) (p 1) = 2 * Real.sin (C / 2)
+  edgeB : dist (p 1) (p 2) = 2 * Real.sin (B / 2)
+  edgeA : dist (p 4) (p 5) = 2 * Real.sin (A / 2)
+
+/-- The required diagonal part of the frozen certificate dictionary (interface v1.2). -/
+structure DistanceDictionary (p : Fin 7 → Plane) (A B : ℝ) : Prop where
+  q_sq :
+    (dist (p 0) (p 2)) ^ 2 =
+      3 - 2 * Real.cos A - 2 * Real.cos B + 2 * Real.cos (A + B)
+  ra_sq :
+    (dist (p 0) (p 5)) ^ 2 =
+      4 - 4 * Real.cos A - 2 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (2 * A + B)
+  rb_sq :
+    (dist (p 1) (p 3)) ^ 2 =
+      4 - 2 * Real.cos A - 4 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (A + 2 * B)
+
+/-- Frozen interface v1.2, with optional class equalities omitted. -/
+structure E2AngleParametrization (p : Fin 7 → Plane) (A B C : ℝ) : Prop where
+  B_pos : 0 < B
+  B_lt_A : B < A
+  A_lt_C : A < C
+  C_lt_pi_div_three : C < Real.pi / 3
+  angle_sum : 2 * C + 3 * A + 2 * B = Real.pi
+  closure : 2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B)) = 1
+  edgeC : dist (p 0) (p 1) = 2 * Real.sin (C / 2)
+  edgeB : dist (p 1) (p 2) = 2 * Real.sin (B / 2)
+  edgeA : dist (p 4) (p 5) = 2 * Real.sin (A / 2)
+  q_sq :
+    (dist (p 0) (p 2)) ^ 2 =
+      3 - 2 * Real.cos A - 2 * Real.cos B + 2 * Real.cos (A + B)
+  ra_sq :
+    (dist (p 0) (p 5)) ^ 2 =
+      4 - 4 * Real.cos A - 2 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (2 * A + B)
+  rb_sq :
+    (dist (p 1) (p 3)) ^ 2 =
+      4 - 2 * Real.cos A - 4 * Real.cos B + 4 * Real.cos (A + B) -
+        2 * Real.cos (A + 2 * B)
+
+/-- Equal base lengths in two unit apex triangles give equal apex angles. -/
+private theorem apexAngle_eq_of_base_dist_eq
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) {i j : Fin 7}
+    (hbase : dist (p (i + 3)) (p (i + 4)) =
+      dist (p (j + 3)) (p (j + 4))) :
+    apexAngle p i = apexAngle p j := by
+  have hleft (k : Fin 7) : dist (p (k + 3)) (p k) = 1 := by
+    simpa [dist_comm] using h.hdiam k
+  have hright (k : Fin 7) : dist (p k) (p (k + 4)) = 1 := by
+    have hd := h.hdiam (k + 4)
+    have hindex : (k + 4) + 3 = k := by omega
+    simpa [hindex, dist_comm] using hd
+  have hcongruent := EuclideanGeometry.side_side_side
+    (show dist (p (i + 3)) (p i) = dist (p (j + 3)) (p j) by
+      rw [hleft i, hleft j])
+    (show dist (p i) (p (i + 4)) = dist (p j) (p (j + 4)) by
+      rw [hright i, hright j])
+    (show dist (p (i + 4)) (p (i + 3)) =
+        dist (p (j + 4)) (p (j + 3)) by
+      simpa [dist_comm] using hbase)
+  simpa [apexAngle] using
+    EuclideanGeometry.angle_eq_of_congruent hcongruent (0 : Fin 3) 1 2
+
+/-- The challenge edge equalities give the certificate angle-class pattern. -/
+theorem apex_angle_classes
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    AngleClasses p (apexAngle p 1) (apexAngle p 5) (apexAngle p 0) := by
+  have h04 : apexAngle p 0 = apexAngle p 4 :=
+    apexAngle_eq_of_base_dist_eq h h.hC.symm
+  have h12 : apexAngle p 1 = apexAngle p 2 :=
+    apexAngle_eq_of_base_dist_eq h h.hA₁
+  have h23 : apexAngle p 2 = apexAngle p 3 :=
+    apexAngle_eq_of_base_dist_eq h h.hA₂
+  have h56 : apexAngle p 5 = apexAngle p 6 :=
+    apexAngle_eq_of_base_dist_eq h h.hB
+  exact
+    { angle0 := rfl
+      angle1 := rfl
+      angle2 := h12.symm
+      angle3 := h23.symm.trans h12.symm
+      angle4 := h04.symm
+      angle5 := rfl
+      angle6 := h56.symm }
+
+private def complexCross (x y : ℂ) : ℝ :=
+  x.re * y.im - x.im * y.re
+
+private theorem complex_oangle_eq_angle_of_cross_pos
+    {x y : ℂ} (hcross : 0 < complexCross x y) :
+    Complex.orientation.oangle x y = InnerProductGeometry.angle x y := by
+  have hx : x ≠ 0 := by
+    intro hx
+    simp [hx, complexCross] at hcross
+  have hy : y ≠ 0 := by
+    intro hy
+    simp [hy, complexCross] at hcross
+  rcases Complex.orientation.oangle_eq_angle_or_eq_neg_angle hx hy with hpos | hneg
+  · exact hpos
+  · have hsin : 0 < Real.Angle.sin (Complex.orientation.oangle x y) := by
+      rw [Complex.oangle, Real.Angle.sin_coe, Complex.sin_arg]
+      have him : ((starRingEnd ℂ) x * y).im = complexCross x y := by
+        simp [complexCross]
+        ring
+      rw [him]
+      exact div_pos hcross (norm_pos_iff.mpr
+        (mul_ne_zero ((map_ne_zero (starRingEnd ℂ)).2 hx) hy))
+    rw [hneg, Real.Angle.sin_neg, Real.Angle.sin_coe] at hsin
+    have hnonneg := Real.sin_nonneg_of_nonneg_of_le_pi
+      (InnerProductGeometry.angle_nonneg x y) (InnerProductGeometry.angle_le_pi x y)
+    linarith
+
+private theorem complex_oangle_eq_neg_angle_of_cross_neg
+    {x y : ℂ} (hcross : complexCross x y < 0) :
+    Complex.orientation.oangle x y = -InnerProductGeometry.angle x y := by
+  have hx : x ≠ 0 := by
+    intro hx
+    simp [hx, complexCross] at hcross
+  have hy : y ≠ 0 := by
+    intro hy
+    simp [hy, complexCross] at hcross
+  rcases Complex.orientation.oangle_eq_angle_or_eq_neg_angle hx hy with hpos | hneg
+  · have hsin : Real.Angle.sin (Complex.orientation.oangle x y) < 0 := by
+      rw [Complex.oangle, Real.Angle.sin_coe, Complex.sin_arg]
+      have him : ((starRingEnd ℂ) x * y).im = complexCross x y := by
+        simp [complexCross]
+        ring
+      rw [him]
+      exact div_neg_of_neg_of_pos hcross (norm_pos_iff.mpr
+        (mul_ne_zero ((map_ne_zero (starRingEnd ℂ)).2 hx) hy))
+    rw [hpos, Real.Angle.sin_coe] at hsin
+    have hnonneg := Real.sin_nonneg_of_nonneg_of_le_pi
+      (InnerProductGeometry.angle_nonneg x y) (InnerProductGeometry.angle_le_pi x y)
+    linarith
+  · exact hneg
+
+private theorem apexAngle_pos
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7) :
+    0 < apexAngle p i := by
+  exact EuclideanGeometry.angle_pos_of_not_collinear (apex_not_collinear h i)
+
+private theorem apexAngle_lt_pi
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7) :
+    apexAngle p i < Real.pi := by
+  exact EuclideanGeometry.angle_lt_pi_of_not_collinear (apex_not_collinear h i)
+
+private theorem apex_base_sq
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7) :
+    (dist (p (i + 3)) (p (i + 4))) ^ 2 = 2 - 2 * Real.cos (apexAngle p i) := by
+  have hleft : dist (p (i + 3)) (p i) = 1 := by
+    simpa [dist_comm] using h.hdiam i
+  have hright : dist (p i) (p (i + 4)) = 1 := by
+    have hd := h.hdiam (i + 4)
+    have hindex : (i + 4) + 3 = i := by omega
+    simpa [hindex, dist_comm] using hd
+  have hcos := EuclideanGeometry.law_cos (p (i + 3)) (p i) (p (i + 4))
+  rw [hleft, dist_comm (p (i + 4)) (p i), hright] at hcos
+  norm_num at hcos
+  simpa [apexAngle, pow_two] using hcos
+
+private theorem apexAngle_lt_of_base_dist_lt
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) {i j : Fin 7}
+    (hbase : dist (p (i + 3)) (p (i + 4)) <
+      dist (p (j + 3)) (p (j + 4))) :
+    apexAngle p i < apexAngle p j := by
+  have hsquare :
+      (dist (p (i + 3)) (p (i + 4))) ^ 2 <
+        (dist (p (j + 3)) (p (j + 4))) ^ 2 :=
+    (sq_lt_sq₀ dist_nonneg dist_nonneg).2 hbase
+  have hcos : Real.cos (apexAngle p j) < Real.cos (apexAngle p i) := by
+    rw [apex_base_sq h i, apex_base_sq h j] at hsquare
+    linarith
+  by_contra hnot
+  have hreverse : apexAngle p j ≤ apexAngle p i := le_of_not_gt hnot
+  have hcosReverse := Real.antitoneOn_cos
+    ⟨(apexAngle_pos h j).le, (apexAngle_lt_pi h j).le⟩
+    ⟨(apexAngle_pos h i).le, (apexAngle_lt_pi h i).le⟩ hreverse
+  linarith
+
+private theorem apexAngle_lt_pi_div_three
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7)
+    (hbase : dist (p (i + 3)) (p (i + 4)) < 1) :
+    apexAngle p i < Real.pi / 3 := by
+  have hsquare : (dist (p (i + 3)) (p (i + 4))) ^ 2 < 1 := by
+    nlinarith [dist_nonneg (x := p (i + 3)) (y := p (i + 4))]
+  have hcos : 1 / 2 < Real.cos (apexAngle p i) := by
+    rw [apex_base_sq h i] at hsquare
+    linarith
+  by_contra hnot
+  have hthirdNonneg : 0 ≤ Real.pi / 3 := by positivity
+  have hthirdLePi : Real.pi / 3 ≤ Real.pi := by nlinarith [Real.pi_pos]
+  have hcosLe := Real.antitoneOn_cos
+    ⟨hthirdNonneg, hthirdLePi⟩
+    ⟨(apexAngle_pos h i).le, (apexAngle_lt_pi h i).le⟩ (le_of_not_gt hnot)
+  rw [Real.cos_pi_div_three] at hcosLe
+  norm_num at hcosLe
+  linarith
+
+private theorem apex_base_lt_one
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7) :
+    dist (p (i + 3)) (p (i + 4)) < 1 := by
+  exact h.hshort (i + 3) (i + 4) (by omega) (by omega) (by omega)
+
+private theorem apex_base_eq_two_mul_sin_half
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i : Fin 7) :
+    dist (p (i + 3)) (p (i + 4)) =
+      2 * Real.sin (apexAngle p i / 2) := by
+  have hhalfNonneg : 0 ≤ apexAngle p i / 2 := by
+    exact div_nonneg (apexAngle_pos h i).le (by norm_num)
+  have hhalfLePi : apexAngle p i / 2 ≤ Real.pi := by
+    linarith [apexAngle_lt_pi h i, Real.pi_pos]
+  have hrightNonneg : 0 ≤ 2 * Real.sin (apexAngle p i / 2) :=
+    mul_nonneg (by norm_num) (Real.sin_nonneg_of_nonneg_of_le_pi hhalfNonneg hhalfLePi)
+  apply (sq_eq_sq₀ dist_nonneg hrightNonneg).mp
+  rw [apex_base_sq h i]
+  have htrig := Real.cos_two_mul (apexAngle p i / 2)
+  have hdouble : 2 * (apexAngle p i / 2) = apexAngle p i := by ring
+  rw [hdouble] at htrig
+  nlinarith [Real.sin_sq_add_cos_sq (apexAngle p i / 2)]
+
+private noncomputable def walkComplexPoint (p : Fin 7 → Plane) (k : Fin 7) : ℂ :=
+  toComplex (p (walkIndex k))
+
+private noncomputable def walkComplexEdge (p : Fin 7 → Plane) (k : Fin 7) : ℂ :=
+  walkComplexPoint p (k + 1) - walkComplexPoint p k
+
+private theorem walkComplexEdge_ne_zero
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    walkComplexEdge p k ≠ 0 := by
+  intro hedge
+  have hz : walkComplexPoint p (k + 1) = walkComplexPoint p k := sub_eq_zero.mp hedge
+  have hp : p (walkIndex (k + 1)) = p (walkIndex k) :=
+    complexPlaneEquiv.symm.injective (by
+      simpa [walkComplexPoint, toComplex] using hz)
+  have hi := pairwise_distinct_of_diameter_pattern h hp
+  have hne : walkIndex (k + 1) ≠ walkIndex k := by
+    fin_cases k <;> decide
+  exact hne hi
+
+private theorem walkComplexEdge_norm
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    ‖walkComplexEdge p k‖ = 1 := by
+  have hstep : walkIndex (k + 1) = walkIndex k + 3 := by
+    simp only [walkIndex]
+    omega
+  have hmap := complexPlaneEquiv.symm.toLinearIsometry.norm_map
+    (p (walkIndex (k + 1)) - p (walkIndex k))
+  have hsource : ‖p (walkIndex (k + 1)) - p (walkIndex k)‖ = 1 := by
+    rw [norm_sub_rev, ← dist_eq_norm, hstep, h.hdiam]
+  calc
+    ‖walkComplexEdge p k‖ =
+        ‖p (walkIndex (k + 1)) - p (walkIndex k)‖ := by
+      simpa [walkComplexEdge, walkComplexPoint, toComplex, map_sub] using hmap
+    _ = 1 := hsource
+
+private theorem walkComplexAngle_eq_apex
+    (p : Fin 7 → Plane) (k : Fin 7) :
+    InnerProductGeometry.angle (-walkComplexEdge p k) (walkComplexEdge p (k + 1)) =
+      apexAngle p (walkIndex (k + 1)) := by
+  have hmap := complexPlaneEquiv.symm.toLinearIsometry.angle_map
+    (p (walkIndex k) - p (walkIndex (k + 1)))
+    (p (walkIndex (k + 2)) - p (walkIndex (k + 1)))
+  have hstep : (k + 1) + 1 = k + 2 := by omega
+  have hprev : walkIndex k = walkIndex (k + 1) + 4 := by
+    simp only [walkIndex]
+    omega
+  have hnext : walkIndex (k + 2) = walkIndex (k + 1) + 3 := by
+    simp only [walkIndex]
+    omega
+  simpa [walkComplexEdge, walkComplexPoint, hstep, neg_sub, hprev, hnext,
+    apexAngle, EuclideanGeometry.angle, toComplex, InnerProductGeometry.angle_comm] using hmap
+
+private theorem walkComplexCross_eq_neg_orientedArea
+    (p : Fin 7 → Plane) (k : Fin 7) :
+    complexCross (-walkComplexEdge p k) (walkComplexEdge p (k + 1)) =
+      -orientedArea (p (walkIndex k)) (p (walkIndex (k + 1)))
+        (p (walkIndex (k + 2))) := by
+  have hstep : (k + 1) + 1 = k + 2 := by omega
+  simp only [walkComplexEdge, walkComplexPoint, hstep, orientedArea, complexCross,
+    Complex.neg_re, Complex.neg_im, Complex.sub_re, Complex.sub_im]
+  ring
+
+private noncomputable def walkComplexTurn (p : Fin 7 → Plane) (k : Fin 7) :
+    Real.Angle :=
+  Complex.orientation.oangle (-walkComplexEdge p k) (walkComplexEdge p (k + 1))
+
+private noncomputable def walkExteriorTurn (p : Fin 7 → Plane) (k : Fin 7) :
+    Real.Angle :=
+  Complex.orientation.oangle (walkComplexEdge p k) (walkComplexEdge p (k + 1))
+
+private theorem walkComplexTurn_eq_exterior_add_pi
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    walkComplexTurn p k = walkExteriorTurn p k + Real.pi := by
+  exact Complex.orientation.oangle_neg_left (walkComplexEdge_ne_zero h k)
+    (walkComplexEdge_ne_zero h (k + 1))
+
+private theorem walkComplexTurn_sum
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    walkComplexTurn p 0 + walkComplexTurn p 1 + walkComplexTurn p 2 +
+      walkComplexTurn p 3 + walkComplexTurn p 4 + walkComplexTurn p 5 +
+        walkComplexTurn p 6 = Real.pi := by
+  have h0 := walkComplexEdge_ne_zero h (0 : Fin 7)
+  have h1 := walkComplexEdge_ne_zero h (1 : Fin 7)
+  have h2 := walkComplexEdge_ne_zero h (2 : Fin 7)
+  have h3 := walkComplexEdge_ne_zero h (3 : Fin 7)
+  have h4 := walkComplexEdge_ne_zero h (4 : Fin 7)
+  have h5 := walkComplexEdge_ne_zero h (5 : Fin 7)
+  have h6 := walkComplexEdge_ne_zero h (6 : Fin 7)
+  have hexterior :
+      walkExteriorTurn p 0 + walkExteriorTurn p 1 + walkExteriorTurn p 2 +
+        walkExteriorTurn p 3 + walkExteriorTurn p 4 + walkExteriorTurn p 5 +
+          walkExteriorTurn p 6 = 0 := by
+    simp only [walkExteriorTurn]
+    calc
+      Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 1) +
+            Complex.orientation.oangle (walkComplexEdge p 1) (walkComplexEdge p 2) +
+          Complex.orientation.oangle (walkComplexEdge p 2) (walkComplexEdge p 3) +
+        Complex.orientation.oangle (walkComplexEdge p 3) (walkComplexEdge p 4) +
+          Complex.orientation.oangle (walkComplexEdge p 4) (walkComplexEdge p 5) +
+        Complex.orientation.oangle (walkComplexEdge p 5) (walkComplexEdge p 6) +
+        Complex.orientation.oangle (walkComplexEdge p 6) (walkComplexEdge p 0) =
+          Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 2) +
+            Complex.orientation.oangle (walkComplexEdge p 2) (walkComplexEdge p 3) +
+          Complex.orientation.oangle (walkComplexEdge p 3) (walkComplexEdge p 4) +
+            Complex.orientation.oangle (walkComplexEdge p 4) (walkComplexEdge p 5) +
+          Complex.orientation.oangle (walkComplexEdge p 5) (walkComplexEdge p 6) +
+          Complex.orientation.oangle (walkComplexEdge p 6) (walkComplexEdge p 0) := by
+            rw [Complex.orientation.oangle_add h0 h1 h2]
+      _ = Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 3) +
+            Complex.orientation.oangle (walkComplexEdge p 3) (walkComplexEdge p 4) +
+          Complex.orientation.oangle (walkComplexEdge p 4) (walkComplexEdge p 5) +
+            Complex.orientation.oangle (walkComplexEdge p 5) (walkComplexEdge p 6) +
+          Complex.orientation.oangle (walkComplexEdge p 6) (walkComplexEdge p 0) := by
+            rw [Complex.orientation.oangle_add h0 h2 h3]
+      _ = Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 4) +
+            Complex.orientation.oangle (walkComplexEdge p 4) (walkComplexEdge p 5) +
+          Complex.orientation.oangle (walkComplexEdge p 5) (walkComplexEdge p 6) +
+          Complex.orientation.oangle (walkComplexEdge p 6) (walkComplexEdge p 0) := by
+            rw [Complex.orientation.oangle_add h0 h3 h4]
+      _ = Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 5) +
+            Complex.orientation.oangle (walkComplexEdge p 5) (walkComplexEdge p 6) +
+          Complex.orientation.oangle (walkComplexEdge p 6) (walkComplexEdge p 0) := by
+            rw [Complex.orientation.oangle_add h0 h4 h5]
+      _ = Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 6) +
+          Complex.orientation.oangle (walkComplexEdge p 6) (walkComplexEdge p 0) := by
+            rw [Complex.orientation.oangle_add h0 h5 h6]
+      _ = 0 := Complex.orientation.oangle_add_oangle_rev _ _
+  have hsevenPi :
+      (Real.pi : Real.Angle) + Real.pi + Real.pi + Real.pi + Real.pi + Real.pi + Real.pi =
+        Real.pi := by
+    calc
+      (Real.pi : Real.Angle) + Real.pi + Real.pi + Real.pi + Real.pi + Real.pi + Real.pi =
+          (Real.pi + Real.pi) + (Real.pi + Real.pi) + (Real.pi + Real.pi) + Real.pi := by
+            abel
+      _ = Real.pi := by simp
+  rw [walkComplexTurn_eq_exterior_add_pi h 0,
+    walkComplexTurn_eq_exterior_add_pi h 1,
+    walkComplexTurn_eq_exterior_add_pi h 2,
+    walkComplexTurn_eq_exterior_add_pi h 3,
+    walkComplexTurn_eq_exterior_add_pi h 4,
+    walkComplexTurn_eq_exterior_add_pi h 5,
+    walkComplexTurn_eq_exterior_add_pi h 6]
+  calc
+    (walkExteriorTurn p 0 + Real.pi) + (walkExteriorTurn p 1 + Real.pi) +
+          (walkExteriorTurn p 2 + Real.pi) + (walkExteriorTurn p 3 + Real.pi) +
+        (walkExteriorTurn p 4 + Real.pi) + (walkExteriorTurn p 5 + Real.pi) +
+        (walkExteriorTurn p 6 + Real.pi) =
+      (walkExteriorTurn p 0 + walkExteriorTurn p 1 + walkExteriorTurn p 2 +
+          walkExteriorTurn p 3 + walkExteriorTurn p 4 + walkExteriorTurn p 5 +
+          walkExteriorTurn p 6) +
+        (Real.pi + Real.pi + Real.pi + Real.pi + Real.pi + Real.pi + Real.pi) := by
+          abel
+    _ = Real.pi := by rw [hexterior, hsevenPi, zero_add]
+
+private theorem walkComplexTurn_cases
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    (∀ k, walkComplexTurn p k =
+      -(apexAngle p (walkIndex (k + 1)) : Real.Angle)) ∨
+    (∀ k, walkComplexTurn p k =
+      (apexAngle p (walkIndex (k + 1)) : Real.Angle)) := by
+  obtain ⟨ε, hε, hturn⟩ := diameter_star_structure h
+  rcases hε with rfl | rfl
+  · left
+    intro k
+    have harea := hturn k
+    have hcross :
+        complexCross (-walkComplexEdge p k) (walkComplexEdge p (k + 1)) < 0 := by
+      rw [walkComplexCross_eq_neg_orientedArea]
+      norm_num at harea ⊢
+      linarith
+    have hoangle := complex_oangle_eq_neg_angle_of_cross_neg hcross
+    rw [walkComplexAngle_eq_apex] at hoangle
+    exact hoangle
+  · right
+    intro k
+    have harea := hturn k
+    have hcross :
+        0 < complexCross (-walkComplexEdge p k) (walkComplexEdge p (k + 1)) := by
+      rw [walkComplexCross_eq_neg_orientedArea]
+      norm_num at harea ⊢
+      linarith
+    have hoangle := complex_oangle_eq_angle_of_cross_pos hcross
+    rw [walkComplexAngle_eq_apex] at hoangle
+    exact hoangle
+
+private theorem walkExteriorTurn_cases
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    (∀ k, walkExteriorTurn p k =
+      -(apexAngle p (walkIndex (k + 1)) : Real.Angle) - Real.pi) ∨
+    (∀ k, walkExteriorTurn p k =
+      (apexAngle p (walkIndex (k + 1)) : Real.Angle) - Real.pi) := by
+  rcases walkComplexTurn_cases h with hneg | hpos
+  · left
+    intro k
+    have hrelation := walkComplexTurn_eq_exterior_add_pi h k
+    rw [hneg k] at hrelation
+    calc
+      walkExteriorTurn p k =
+          (walkExteriorTurn p k + Real.pi) - Real.pi := by
+            rw [add_sub_cancel_right]
+      _ = -(apexAngle p (walkIndex (k + 1)) : Real.Angle) - Real.pi := by
+            rw [← hrelation]
+  · right
+    intro k
+    have hrelation := walkComplexTurn_eq_exterior_add_pi h k
+    rw [hpos k] at hrelation
+    calc
+      walkExteriorTurn p k =
+          (walkExteriorTurn p k + Real.pi) - Real.pi := by
+            rw [add_sub_cancel_right]
+      _ = (apexAngle p (walkIndex (k + 1)) : Real.Angle) - Real.pi := by
+            rw [← hrelation]
+
+private theorem walkExteriorTurn_signed
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    ∃ s : ℝ, (s = -1 ∨ s = 1) ∧
+      ∀ k, walkExteriorTurn p k =
+        ((s * apexAngle p (walkIndex (k + 1)) : ℝ) : Real.Angle) - Real.pi := by
+  rcases walkExteriorTurn_cases h with hneg | hpos
+  · refine ⟨-1, Or.inl rfl, ?_⟩
+    intro k
+    simpa only [neg_one_mul, Real.Angle.coe_neg] using hneg k
+  · refine ⟨1, Or.inr rfl, ?_⟩
+    intro k
+    simpa only [one_mul] using hpos k
+
+private theorem walkComplexEdge_mul_conj_re
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (i j : Fin 7) :
+    (walkComplexEdge p i * starRingEnd ℂ (walkComplexEdge p j)).re =
+      Real.Angle.cos
+        (Complex.orientation.oangle (walkComplexEdge p i) (walkComplexEdge p j)) := by
+  have hinner := Complex.orientation.inner_eq_norm_mul_norm_mul_cos_oangle
+    (walkComplexEdge p i) (walkComplexEdge p j)
+  rw [walkComplexEdge_norm h i, walkComplexEdge_norm h j] at hinner
+  simpa [Complex.inner, mul_comm] using hinner
+
+private theorem angle_signed_turn_two (s x y : ℝ) :
+    (((s * x : ℝ) : Real.Angle) - Real.pi) +
+        (((s * y : ℝ) : Real.Angle) - Real.pi) =
+      ((s * (x + y) : ℝ) : Real.Angle) := by
+  simp only [sub_eq_add_neg, Real.Angle.neg_coe_pi]
+  calc
+    ((s * x : ℝ) : Real.Angle) + Real.pi +
+          (((s * y : ℝ) : Real.Angle) + Real.pi) =
+        (((s * x : ℝ) : Real.Angle) + ((s * y : ℝ) : Real.Angle)) +
+          (Real.pi + Real.pi) := by abel
+    _ = ((s * x + s * y : ℝ) : Real.Angle) := by simp
+    _ = ((s * (x + y) : ℝ) : Real.Angle) := by
+      congr 1
+      ring
+
+private theorem angle_signed_turn_three (s x y z : ℝ) :
+    (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) =
+      ((s * (x + y + z) : ℝ) : Real.Angle) - Real.pi := by
+  have hcoe :
+      ((s * (x + y) : ℝ) : Real.Angle) + ((s * z : ℝ) : Real.Angle) =
+        ((s * (x + y + z) : ℝ) : Real.Angle) := by
+    rw [← Real.Angle.coe_add]
+    congr 1
+    ring
+  calc
+    (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) =
+      ((((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi)) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) := by abel
+    _ = ((s * (x + y) : ℝ) : Real.Angle) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) := by rw [angle_signed_turn_two]
+    _ = (((s * (x + y) : ℝ) : Real.Angle) +
+        ((s * z : ℝ) : Real.Angle)) - Real.pi := by abel
+    _ = ((s * (x + y + z) : ℝ) : Real.Angle) - Real.pi := by rw [hcoe]
+
+private theorem angle_signed_turn_four (s w x y z : ℝ) :
+    (((s * w : ℝ) : Real.Angle) - Real.pi) +
+          (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) =
+      ((s * (w + x + y + z) : ℝ) : Real.Angle) := by
+  calc
+    (((s * w : ℝ) : Real.Angle) - Real.pi) +
+          (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) =
+      ((((s * w : ℝ) : Real.Angle) - Real.pi) +
+          (((s * x : ℝ) : Real.Angle) - Real.pi)) +
+        ((((s * y : ℝ) : Real.Angle) - Real.pi) +
+          (((s * z : ℝ) : Real.Angle) - Real.pi)) := by abel
+    _ = ((s * (w + x) : ℝ) : Real.Angle) +
+        ((s * (y + z) : ℝ) : Real.Angle) := by
+      rw [angle_signed_turn_two, angle_signed_turn_two]
+    _ = ((s * (w + x) + s * (y + z) : ℝ) : Real.Angle) := by
+      rw [Real.Angle.coe_add]
+    _ = ((s * (w + x + y + z) : ℝ) : Real.Angle) := by
+      congr 1
+      ring
+
+private theorem angle_signed_turn_five (s v w x y z : ℝ) :
+    (((s * v : ℝ) : Real.Angle) - Real.pi) +
+          (((s * w : ℝ) : Real.Angle) - Real.pi) +
+          (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) =
+      ((s * (v + w + x + y + z) : ℝ) : Real.Angle) - Real.pi := by
+  have hcoe :
+      ((s * (v + w + x + y) : ℝ) : Real.Angle) +
+          ((s * z : ℝ) : Real.Angle) =
+        ((s * (v + w + x + y + z) : ℝ) : Real.Angle) := by
+    rw [← Real.Angle.coe_add]
+    congr 1
+    ring
+  calc
+    (((s * v : ℝ) : Real.Angle) - Real.pi) +
+          (((s * w : ℝ) : Real.Angle) - Real.pi) +
+          (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) =
+      ((((s * v : ℝ) : Real.Angle) - Real.pi) +
+          (((s * w : ℝ) : Real.Angle) - Real.pi) +
+          (((s * x : ℝ) : Real.Angle) - Real.pi) +
+          (((s * y : ℝ) : Real.Angle) - Real.pi)) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) := by abel
+    _ = ((s * (v + w + x + y) : ℝ) : Real.Angle) +
+        (((s * z : ℝ) : Real.Angle) - Real.pi) := by rw [angle_signed_turn_four]
+    _ = (((s * (v + w + x + y) : ℝ) : Real.Angle) +
+        ((s * z : ℝ) : Real.Angle)) - Real.pi := by abel
+    _ = ((s * (v + w + x + y + z) : ℝ) : Real.Angle) - Real.pi := by rw [hcoe]
+
+private theorem cos_sign_mul (s x : ℝ) (hs : s = -1 ∨ s = 1) :
+    Real.cos (s * x) = Real.cos x := by
+  rcases hs with rfl | rfl
+  · rw [neg_one_mul, Real.cos_neg]
+  · rw [one_mul]
+
+private structure WalkGram (p : Fin 7 → Plane) (A B : ℝ) : Prop where
+  dot01 : (walkComplexEdge p 0 * starRingEnd ℂ (walkComplexEdge p 1)).re = -Real.cos A
+  dot12 : (walkComplexEdge p 1 * starRingEnd ℂ (walkComplexEdge p 2)).re = -Real.cos B
+  dot23 : (walkComplexEdge p 2 * starRingEnd ℂ (walkComplexEdge p 3)).re = -Real.cos A
+  dot34 : (walkComplexEdge p 3 * starRingEnd ℂ (walkComplexEdge p 4)).re = -Real.cos B
+  dot45 : (walkComplexEdge p 4 * starRingEnd ℂ (walkComplexEdge p 5)).re = -Real.cos A
+  dot02 : (walkComplexEdge p 0 * starRingEnd ℂ (walkComplexEdge p 2)).re = Real.cos (A + B)
+  dot13 : (walkComplexEdge p 1 * starRingEnd ℂ (walkComplexEdge p 3)).re = Real.cos (A + B)
+  dot24 : (walkComplexEdge p 2 * starRingEnd ℂ (walkComplexEdge p 4)).re = Real.cos (A + B)
+  dot35 : (walkComplexEdge p 3 * starRingEnd ℂ (walkComplexEdge p 5)).re = Real.cos (A + B)
+  dot03 : (walkComplexEdge p 0 * starRingEnd ℂ (walkComplexEdge p 3)).re = -Real.cos (2 * A + B)
+  dot14 : (walkComplexEdge p 1 * starRingEnd ℂ (walkComplexEdge p 4)).re = -Real.cos (A + 2 * B)
+  dot25 : (walkComplexEdge p 2 * starRingEnd ℂ (walkComplexEdge p 5)).re = -Real.cos (2 * A + B)
+  dot04 : (walkComplexEdge p 0 * starRingEnd ℂ (walkComplexEdge p 4)).re = Real.cos (2 * (A + B))
+  dot15 : (walkComplexEdge p 1 * starRingEnd ℂ (walkComplexEdge p 5)).re = Real.cos (2 * (A + B))
+  dot05 : (walkComplexEdge p 0 * starRingEnd ℂ (walkComplexEdge p 5)).re = -Real.cos (3 * A + 2 * B)
+
+private theorem walk_oangle_02 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 2) =
+      walkExteriorTurn p 0 + walkExteriorTurn p 1 := by
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 0) (walkComplexEdge_ne_zero h 1)
+      (walkComplexEdge_ne_zero h 2)
+
+private theorem walk_oangle_13 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 1) (walkComplexEdge p 3) =
+      walkExteriorTurn p 1 + walkExteriorTurn p 2 := by
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 1) (walkComplexEdge_ne_zero h 2)
+      (walkComplexEdge_ne_zero h 3)
+
+private theorem walk_oangle_24 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 2) (walkComplexEdge p 4) =
+      walkExteriorTurn p 2 + walkExteriorTurn p 3 := by
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 2) (walkComplexEdge_ne_zero h 3)
+      (walkComplexEdge_ne_zero h 4)
+
+private theorem walk_oangle_35 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 3) (walkComplexEdge p 5) =
+      walkExteriorTurn p 3 + walkExteriorTurn p 4 := by
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 3) (walkComplexEdge_ne_zero h 4)
+      (walkComplexEdge_ne_zero h 5)
+
+private theorem walk_oangle_03 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 3) =
+      walkExteriorTurn p 0 + walkExteriorTurn p 1 + walkExteriorTurn p 2 := by
+  rw [← walk_oangle_02 h]
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 0) (walkComplexEdge_ne_zero h 2)
+      (walkComplexEdge_ne_zero h 3)
+
+private theorem walk_oangle_14 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 1) (walkComplexEdge p 4) =
+      walkExteriorTurn p 1 + walkExteriorTurn p 2 + walkExteriorTurn p 3 := by
+  rw [← walk_oangle_13 h]
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 1) (walkComplexEdge_ne_zero h 3)
+      (walkComplexEdge_ne_zero h 4)
+
+private theorem walk_oangle_25 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 2) (walkComplexEdge p 5) =
+      walkExteriorTurn p 2 + walkExteriorTurn p 3 + walkExteriorTurn p 4 := by
+  rw [← walk_oangle_24 h]
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 2) (walkComplexEdge_ne_zero h 4)
+      (walkComplexEdge_ne_zero h 5)
+
+private theorem walk_oangle_04 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 4) =
+      walkExteriorTurn p 0 + walkExteriorTurn p 1 + walkExteriorTurn p 2 +
+        walkExteriorTurn p 3 := by
+  rw [← walk_oangle_03 h]
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 0) (walkComplexEdge_ne_zero h 3)
+      (walkComplexEdge_ne_zero h 4)
+
+private theorem walk_oangle_15 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 1) (walkComplexEdge p 5) =
+      walkExteriorTurn p 1 + walkExteriorTurn p 2 + walkExteriorTurn p 3 +
+        walkExteriorTurn p 4 := by
+  rw [← walk_oangle_14 h]
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 1) (walkComplexEdge_ne_zero h 4)
+      (walkComplexEdge_ne_zero h 5)
+
+private theorem walk_oangle_05 {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    Complex.orientation.oangle (walkComplexEdge p 0) (walkComplexEdge p 5) =
+      walkExteriorTurn p 0 + walkExteriorTurn p 1 + walkExteriorTurn p 2 +
+        walkExteriorTurn p 3 + walkExteriorTurn p 4 := by
+  rw [← walk_oangle_04 h]
+  symm
+  exact Complex.orientation.oangle_add
+    (walkComplexEdge_ne_zero h 0) (walkComplexEdge_ne_zero h 4)
+      (walkComplexEdge_ne_zero h 5)
+
+private theorem walkGram
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p)
+    {A B C : ℝ} (hclasses : AngleClasses p A B C) : WalkGram p A B := by
+  obtain ⟨s, hs, hturn⟩ := walkExteriorTurn_signed h
+  have ht0 : walkExteriorTurn p 0 =
+      ((s * A : ℝ) : Real.Angle) - Real.pi := by
+    have ht := hturn 0
+    norm_num [walkIndex] at ht
+    simpa [hclasses.angle3] using ht
+  have ht1 : walkExteriorTurn p 1 =
+      ((s * B : ℝ) : Real.Angle) - Real.pi := by
+    have ht := hturn 1
+    norm_num [walkIndex] at ht
+    simpa [hclasses.angle6] using ht
+  have ht2 : walkExteriorTurn p 2 =
+      ((s * A : ℝ) : Real.Angle) - Real.pi := by
+    have ht := hturn 2
+    norm_num [walkIndex] at ht
+    simpa [hclasses.angle2] using ht
+  have ht3 : walkExteriorTurn p 3 =
+      ((s * B : ℝ) : Real.Angle) - Real.pi := by
+    have ht := hturn 3
+    norm_num [walkIndex] at ht
+    simpa [hclasses.angle5] using ht
+  have ht4 : walkExteriorTurn p 4 =
+      ((s * A : ℝ) : Real.Angle) - Real.pi := by
+    have ht := hturn 4
+    norm_num [walkIndex] at ht
+    simpa [hclasses.angle1] using ht
+  refine
+    { dot01 := ?_, dot12 := ?_, dot23 := ?_, dot34 := ?_, dot45 := ?_,
+      dot02 := ?_, dot13 := ?_, dot24 := ?_, dot35 := ?_, dot03 := ?_,
+      dot14 := ?_, dot25 := ?_, dot04 := ?_, dot15 := ?_, dot05 := ?_ }
+  · rw [walkComplexEdge_mul_conj_re h]
+    change Real.Angle.cos (walkExteriorTurn p 0) = _
+    rw [ht0, Real.Angle.cos_sub_pi, Real.Angle.cos_coe, cos_sign_mul s A hs]
+  · rw [walkComplexEdge_mul_conj_re h]
+    change Real.Angle.cos (walkExteriorTurn p 1) = _
+    rw [ht1, Real.Angle.cos_sub_pi, Real.Angle.cos_coe, cos_sign_mul s B hs]
+  · rw [walkComplexEdge_mul_conj_re h]
+    change Real.Angle.cos (walkExteriorTurn p 2) = _
+    rw [ht2, Real.Angle.cos_sub_pi, Real.Angle.cos_coe, cos_sign_mul s A hs]
+  · rw [walkComplexEdge_mul_conj_re h]
+    change Real.Angle.cos (walkExteriorTurn p 3) = _
+    rw [ht3, Real.Angle.cos_sub_pi, Real.Angle.cos_coe, cos_sign_mul s B hs]
+  · rw [walkComplexEdge_mul_conj_re h]
+    change Real.Angle.cos (walkExteriorTurn p 4) = _
+    rw [ht4, Real.Angle.cos_sub_pi, Real.Angle.cos_coe, cos_sign_mul s A hs]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_02 h, ht0, ht1,
+      angle_signed_turn_two, Real.Angle.cos_coe, cos_sign_mul s (A + B) hs]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_13 h, ht1, ht2,
+      angle_signed_turn_two, Real.Angle.cos_coe, cos_sign_mul s (B + A) hs, add_comm B A]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_24 h, ht2, ht3,
+      angle_signed_turn_two, Real.Angle.cos_coe, cos_sign_mul s (A + B) hs]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_35 h, ht3, ht4,
+      angle_signed_turn_two, Real.Angle.cos_coe, cos_sign_mul s (B + A) hs, add_comm B A]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_03 h, ht0, ht1, ht2,
+      angle_signed_turn_three, Real.Angle.cos_sub_pi, Real.Angle.cos_coe,
+      cos_sign_mul s (A + B + A) hs, show A + B + A = 2 * A + B by ring]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_14 h, ht1, ht2, ht3,
+      angle_signed_turn_three, Real.Angle.cos_sub_pi, Real.Angle.cos_coe,
+      cos_sign_mul s (B + A + B) hs, show B + A + B = A + 2 * B by ring]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_25 h, ht2, ht3, ht4,
+      angle_signed_turn_three, Real.Angle.cos_sub_pi, Real.Angle.cos_coe,
+      cos_sign_mul s (A + B + A) hs, show A + B + A = 2 * A + B by ring]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_04 h, ht0, ht1, ht2, ht3,
+      angle_signed_turn_four, Real.Angle.cos_coe,
+      cos_sign_mul s (A + B + A + B) hs,
+      show A + B + A + B = 2 * (A + B) by ring]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_15 h, ht1, ht2, ht3, ht4,
+      angle_signed_turn_four, Real.Angle.cos_coe,
+      cos_sign_mul s (B + A + B + A) hs,
+      show B + A + B + A = 2 * (A + B) by ring]
+  · rw [walkComplexEdge_mul_conj_re h, walk_oangle_05 h, ht0, ht1, ht2, ht3, ht4,
+      angle_signed_turn_five, Real.Angle.cos_sub_pi, Real.Angle.cos_coe,
+      cos_sign_mul s (A + B + A + B + A) hs,
+      show A + B + A + B + A = 3 * A + 2 * B by ring]
+
+private theorem complex_normSq_add_three (a b c : ℂ) :
+    Complex.normSq (a + b + c) = Complex.normSq a + Complex.normSq b +
+      Complex.normSq c + 2 * (a * starRingEnd ℂ b).re +
+        2 * (a * starRingEnd ℂ c).re + 2 * (b * starRingEnd ℂ c).re := by
+  simp [Complex.normSq_apply, Complex.mul_re]
+  ring
+
+private theorem complex_normSq_add_four (a b c d : ℂ) :
+    Complex.normSq (a + b + c + d) =
+      Complex.normSq a + Complex.normSq b + Complex.normSq c + Complex.normSq d +
+        2 * (a * starRingEnd ℂ b).re + 2 * (a * starRingEnd ℂ c).re +
+        2 * (a * starRingEnd ℂ d).re + 2 * (b * starRingEnd ℂ c).re +
+        2 * (b * starRingEnd ℂ d).re + 2 * (c * starRingEnd ℂ d).re := by
+  simp [Complex.normSq_apply, Complex.mul_re]
+  ring
+
+private theorem complex_normSq_add_six (a b c d e f : ℂ) :
+    Complex.normSq (a + b + c + d + e + f) =
+      Complex.normSq a + Complex.normSq b + Complex.normSq c + Complex.normSq d +
+        Complex.normSq e + Complex.normSq f +
+        2 * (a * starRingEnd ℂ b).re + 2 * (a * starRingEnd ℂ c).re +
+        2 * (a * starRingEnd ℂ d).re + 2 * (a * starRingEnd ℂ e).re +
+        2 * (a * starRingEnd ℂ f).re + 2 * (b * starRingEnd ℂ c).re +
+        2 * (b * starRingEnd ℂ d).re + 2 * (b * starRingEnd ℂ e).re +
+        2 * (b * starRingEnd ℂ f).re + 2 * (c * starRingEnd ℂ d).re +
+        2 * (c * starRingEnd ℂ e).re + 2 * (c * starRingEnd ℂ f).re +
+        2 * (d * starRingEnd ℂ e).re + 2 * (d * starRingEnd ℂ f).re +
+        2 * (e * starRingEnd ℂ f).re := by
+  simp [Complex.normSq_apply, Complex.mul_re]
+  ring
+
+private theorem walkComplexEdge_normSq
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    Complex.normSq (walkComplexEdge p k) = 1 := by
+  rw [Complex.normSq_eq_norm_sq, walkComplexEdge_norm h k]
+  norm_num
+
+private theorem walkComplexPoint_dist
+    (p : Fin 7 → Plane) (i j : Fin 7) :
+    dist (p (walkIndex i)) (p (walkIndex j)) =
+      ‖walkComplexPoint p i - walkComplexPoint p j‖ := by
+  have hmap := complexPlaneEquiv.symm.toLinearIsometry.dist_map
+    (p (walkIndex i)) (p (walkIndex j))
+  rw [dist_eq_norm] at hmap
+  simpa [walkComplexPoint, toComplex] using hmap.symm
+
+private theorem walk_sum_0_3 (p : Fin 7 → Plane) :
+    walkComplexPoint p 3 - walkComplexPoint p 0 =
+      walkComplexEdge p 0 + walkComplexEdge p 1 + walkComplexEdge p 2 := by
+  simp [walkComplexEdge]
+
+private theorem walk_sum_0_4 (p : Fin 7 → Plane) :
+    walkComplexPoint p 4 - walkComplexPoint p 0 =
+      walkComplexEdge p 0 + walkComplexEdge p 1 + walkComplexEdge p 2 +
+        walkComplexEdge p 3 := by
+  simp [walkComplexEdge]
+
+private theorem walk_sum_1_5 (p : Fin 7 → Plane) :
+    walkComplexPoint p 5 - walkComplexPoint p 1 =
+      walkComplexEdge p 1 + walkComplexEdge p 2 + walkComplexEdge p 3 +
+        walkComplexEdge p 4 := by
+  simp [walkComplexEdge]
+
+private theorem walk_sum_0_6 (p : Fin 7 → Plane) :
+    walkComplexPoint p 6 - walkComplexPoint p 0 =
+      walkComplexEdge p 0 + walkComplexEdge p 1 + walkComplexEdge p 2 +
+        walkComplexEdge p 3 + walkComplexEdge p 4 + walkComplexEdge p 5 := by
+  simp [walkComplexEdge]
+
+private theorem walk_norm_trig_identity (A B : ℝ) :
+    6 - 6 * Real.cos A - 4 * Real.cos B + 8 * Real.cos (A + B) -
+          4 * Real.cos (2 * A + B) - 2 * Real.cos (A + 2 * B) +
+        4 * Real.cos (2 * (A + B)) - 2 * Real.cos (3 * A + 2 * B) =
+      (2 - 2 * Real.cos A) *
+        (3 + 4 * Real.cos (A + B) + 2 * Real.cos (2 * (A + B))) := by
+  rw [show 2 * A + B = (A + B) + A by ring, Real.cos_add]
+  rw [show A + 2 * B = (A + B) + B by ring, Real.cos_add]
+  rw [show 3 * A + 2 * B = 2 * (A + B) + A by ring, Real.cos_add]
+  rw [Real.cos_add (A + B) B, Real.cos_add (2 * (A + B)) A]
+  rw [Real.cos_two_mul (A + B), Real.sin_two_mul (A + B),
+    Real.cos_add A B, Real.sin_add A B]
+  linear_combination
+    (4 * Real.cos A * Real.cos B ^ 2 -
+        4 * Real.cos B * Real.sin A * Real.sin B + 4 * Real.cos B) *
+      (Real.sin_sq_add_cos_sq A) +
+    (2 * Real.cos A) * (Real.sin_sq_add_cos_sq B)
+
+private theorem two_mul_sin_half_sq (A : ℝ) :
+    (2 * Real.sin (A / 2)) ^ 2 = 2 - 2 * Real.cos A := by
+  have hcos := Real.cos_two_mul (A / 2)
+  rw [show 2 * (A / 2) = A by ring] at hcos
+  nlinarith [Real.sin_sq_add_cos_sq (A / 2)]
+
+private theorem one_add_two_cos_sq (S : ℝ) :
+    (1 + 2 * Real.cos S) ^ 2 =
+      3 + 4 * Real.cos S + 2 * Real.cos (2 * S) := by
+  rw [Real.cos_two_mul]
+  nlinarith [Real.sin_sq_add_cos_sq S]
+
+/-- The star structure and edge order determine the three ordered angle classes. -/
+theorem ordered_angle_classes
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    ∃ A B C : ℝ,
+      0 < B ∧ B < A ∧ A < C ∧ C < Real.pi / 3 ∧ AngleClasses p A B C := by
+  refine ⟨apexAngle p 1, apexAngle p 5, apexAngle p 0, apexAngle_pos h 5, ?_, ?_, ?_,
+    apex_angle_classes h⟩
+  · exact apexAngle_lt_of_base_dist_lt h h.hBA
+  · apply apexAngle_lt_of_base_dist_lt h
+    simpa using h.hAC.trans_eq h.hC
+  · apply apexAngle_lt_pi_div_three h 0
+    exact h.hshort 3 4 (by decide) (by decide) (by decide)
+
+/-- The consistently oriented star walk gives the certificate angle sum. -/
+theorem star_angle_sum
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p)
+    {A B C : ℝ} (hclasses : AngleClasses p A B C) :
+    2 * C + 3 * A + 2 * B = Real.pi := by
+  have hw0 : walkIndex ((0 : Fin 7) + 1) = 3 := by decide
+  have hw1 : walkIndex ((1 : Fin 7) + 1) = 6 := by decide
+  have hw2 : walkIndex ((2 : Fin 7) + 1) = 2 := by decide
+  have hw3 : walkIndex ((3 : Fin 7) + 1) = 5 := by decide
+  have hw4 : walkIndex ((4 : Fin 7) + 1) = 1 := by decide
+  have hw5 : walkIndex ((5 : Fin 7) + 1) = 4 := by decide
+  have hw6 : walkIndex ((6 : Fin 7) + 1) = 0 := by decide
+  have hmod : ((2 * C + 3 * A + 2 * B : ℝ) : Real.Angle) = Real.pi := by
+    rcases walkComplexTurn_cases h with hturnNeg | hturnPos
+    · have hsum := walkComplexTurn_sum h
+      rw [hturnNeg 0, hturnNeg 1, hturnNeg 2, hturnNeg 3, hturnNeg 4,
+        hturnNeg 5, hturnNeg 6] at hsum
+      rw [hw0, hw1, hw2, hw3, hw4, hw5, hw6, hclasses.angle0,
+        hclasses.angle1, hclasses.angle2, hclasses.angle3, hclasses.angle4,
+        hclasses.angle5, hclasses.angle6] at hsum
+      have hnegative :
+          -((A + B + A + B + A + C + C : ℝ) : Real.Angle) = Real.pi := by
+        calc
+          -((A + B + A + B + A + C + C : ℝ) : Real.Angle) =
+              -((A : Real.Angle) + B + A + B + A + C + C) := by
+                simp only [Real.Angle.coe_add]
+          _ = -(A : Real.Angle) - B - A - B - A - C - C := by abel
+          _ =
+              -A + -B + -A + -B + -A + -C + -C := by abel
+          _ = Real.pi := hsum
+      have hnegated := congrArg (fun θ : Real.Angle ↦ -θ) hnegative
+      have hpositive :
+          ((A + B + A + B + A + C + C : ℝ) : Real.Angle) = Real.pi := by
+        simpa using hnegated
+      have hreal : 2 * C + 3 * A + 2 * B = A + B + A + B + A + C + C := by ring
+      rw [hreal]
+      exact hpositive
+    · have hsum := walkComplexTurn_sum h
+      rw [hturnPos 0, hturnPos 1, hturnPos 2, hturnPos 3, hturnPos 4,
+        hturnPos 5, hturnPos 6] at hsum
+      rw [hw0, hw1, hw2, hw3, hw4, hw5, hw6, hclasses.angle0,
+        hclasses.angle1, hclasses.angle2, hclasses.angle3, hclasses.angle4,
+        hclasses.angle5, hclasses.angle6] at hsum
+      have hpositive :
+          ((A + B + A + B + A + C + C : ℝ) : Real.Angle) = Real.pi := by
+        simpa only [Real.Angle.coe_add] using hsum
+      have hreal : 2 * C + 3 * A + 2 * B = A + B + A + B + A + C + C := by ring
+      rw [hreal]
+      exact hpositive
+  have hBpos : 0 < B := by rw [← hclasses.angle5]; exact apexAngle_pos h 5
+  have hApos : 0 < A := by rw [← hclasses.angle1]; exact apexAngle_pos h 1
+  have hCpos : 0 < C := by rw [← hclasses.angle0]; exact apexAngle_pos h 0
+  have hBthird : B < Real.pi / 3 := by
+    rw [← hclasses.angle5]
+    exact apexAngle_lt_pi_div_three h 5 (apex_base_lt_one h 5)
+  have hAthird : A < Real.pi / 3 := by
+    rw [← hclasses.angle1]
+    exact apexAngle_lt_pi_div_three h 1 (apex_base_lt_one h 1)
+  have hCthird : C < Real.pi / 3 := by
+    rw [← hclasses.angle0]
+    exact apexAngle_lt_pi_div_three h 0 (apex_base_lt_one h 0)
+  have hsumPos : 0 < 2 * C + 3 * A + 2 * B := by positivity
+  have hsumUpper : 2 * C + 3 * A + 2 * B < 7 * Real.pi / 3 := by linarith
+  obtain ⟨n, hn⟩ := Real.Angle.angle_eq_iff_two_pi_dvd_sub.mp hmod
+  have hnzero : n = 0 := by
+    by_contra hnzero
+    rcases lt_or_gt_of_ne hnzero with hnneg | hnpos
+    · have hnle : (n : ℝ) ≤ -1 := by exact_mod_cast (show n ≤ -1 by omega)
+      nlinarith [Real.pi_pos]
+    · have hnle : (1 : ℝ) ≤ n := by exact_mod_cast (show 1 ≤ n by omega)
+      nlinarith [Real.pi_pos]
+  subst n
+  norm_num at hn
+  linarith
+
+/-- Unit isosceles apex triangles give the three edge formulas. -/
+theorem edge_formulas
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p)
+    {A B C : ℝ} (hclasses : AngleClasses p A B C) :
+    EdgeFormulas p A B C := by
+  constructor
+  · simpa [hclasses.angle4] using apex_base_eq_two_mul_sin_half h 4
+  · simpa [hclasses.angle5] using apex_base_eq_two_mul_sin_half h 5
+  · simpa [hclasses.angle1] using apex_base_eq_two_mul_sin_half h 1
+
+/-- Closing the normalized Complex walk gives the scalar closure identity. -/
+theorem star_scalar_closure
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p)
+    {A B C : ℝ} (hclasses : AngleClasses p A B C)
+    (hsum : 2 * C + 3 * A + 2 * B = Real.pi) :
+    2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B)) = 1 := by
+  have hgram := walkGram h hclasses
+  have hdiam04 : dist (p 0) (p 4) = 1 := by
+    have hd := h.hdiam 4
+    simpa [dist_comm] using hd
+  have hpoint : dist (p 0) (p 4) =
+      ‖walkComplexPoint p 0 - walkComplexPoint p 6‖ := by
+    simpa [walkIndex] using walkComplexPoint_dist p 0 6
+  have hwalkNorm :
+      ‖walkComplexEdge p 0 + walkComplexEdge p 1 + walkComplexEdge p 2 +
+          walkComplexEdge p 3 + walkComplexEdge p 4 + walkComplexEdge p 5‖ = 1 := by
+    rw [← walk_sum_0_6, norm_sub_rev, ← hpoint]
+    exact hdiam04
+  have hwalkNormSq :
+      Complex.normSq
+        (walkComplexEdge p 0 + walkComplexEdge p 1 + walkComplexEdge p 2 +
+          walkComplexEdge p 3 + walkComplexEdge p 4 + walkComplexEdge p 5) = 1 := by
+    rw [Complex.normSq_eq_norm_sq, hwalkNorm]
+    norm_num
+  rw [complex_normSq_add_six, walkComplexEdge_normSq h 0,
+    walkComplexEdge_normSq h 1, walkComplexEdge_normSq h 2,
+    walkComplexEdge_normSq h 3, walkComplexEdge_normSq h 4,
+    walkComplexEdge_normSq h 5, hgram.dot01, hgram.dot02, hgram.dot03,
+    hgram.dot04, hgram.dot05, hgram.dot12, hgram.dot13, hgram.dot14,
+    hgram.dot15, hgram.dot23, hgram.dot24, hgram.dot25, hgram.dot34,
+    hgram.dot35, hgram.dot45] at hwalkNormSq
+  have htrigProduct :
+      (2 - 2 * Real.cos A) *
+        (3 + 4 * Real.cos (A + B) + 2 * Real.cos (2 * (A + B))) = 1 := by
+    rw [← walk_norm_trig_identity]
+    nlinarith [hwalkNormSq]
+  rw [← two_mul_sin_half_sq, ← one_add_two_cos_sq] at htrigProduct
+  have hsquare :
+      (2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B))) ^ 2 = 1 := by
+    simpa [mul_pow] using htrigProduct
+  have hApos : 0 < A := by
+    rw [← hclasses.angle1]
+    exact apexAngle_pos h 1
+  have hBpos : 0 < B := by
+    rw [← hclasses.angle5]
+    exact apexAngle_pos h 5
+  have hCpos : 0 < C := by
+    rw [← hclasses.angle0]
+    exact apexAngle_pos h 0
+  have hsinpos : 0 < Real.sin (A / 2) := by
+    apply Real.sin_pos_of_pos_of_lt_pi
+    · linarith
+    · have hAlt : A < Real.pi := by
+        rw [← hclasses.angle1]
+        exact apexAngle_lt_pi h 1
+      linarith [Real.pi_pos]
+  have hsumlt : A + B < Real.pi / 2 := by linarith
+  have hcospos : 0 < Real.cos (A + B) := by
+    apply Real.cos_pos_of_mem_Ioo
+    constructor <;> linarith [Real.pi_pos]
+  have hproductpos :
+      0 < 2 * Real.sin (A / 2) * (1 + 2 * Real.cos (A + B)) := by positivity
+  nlinarith
+
+/-- Norm expansion of the normalized certificate walk gives required G6, G8, and G9. -/
+theorem distance_dictionary
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p)
+    {A B C : ℝ} (hclasses : AngleClasses p A B C) :
+    DistanceDictionary p A B := by
+  have hgram := walkGram h hclasses
+  have hqdist : dist (p 0) (p 2) =
+      ‖walkComplexPoint p 0 - walkComplexPoint p 3‖ := by
+    simpa [walkIndex] using walkComplexPoint_dist p 0 3
+  have hradist : dist (p 0) (p 5) =
+      ‖walkComplexPoint p 0 - walkComplexPoint p 4‖ := by
+    simpa [walkIndex] using walkComplexPoint_dist p 0 4
+  have hrbdist : dist (p 1) (p 3) =
+      ‖walkComplexPoint p 5 - walkComplexPoint p 1‖ := by
+    simpa [walkIndex] using walkComplexPoint_dist p 5 1
+  constructor
+  · rw [hqdist, norm_sub_rev, walk_sum_0_3, Complex.sq_norm,
+      complex_normSq_add_three, walkComplexEdge_normSq h 0,
+      walkComplexEdge_normSq h 1, walkComplexEdge_normSq h 2,
+      hgram.dot01, hgram.dot02, hgram.dot12]
+    ring
+  · rw [hradist, norm_sub_rev, walk_sum_0_4, Complex.sq_norm,
+      complex_normSq_add_four, walkComplexEdge_normSq h 0,
+      walkComplexEdge_normSq h 1, walkComplexEdge_normSq h 2,
+      walkComplexEdge_normSq h 3, hgram.dot01, hgram.dot02, hgram.dot03,
+      hgram.dot12, hgram.dot13, hgram.dot23]
+    ring
+  · rw [hrbdist, walk_sum_1_5, Complex.sq_norm, complex_normSq_add_four,
+      walkComplexEdge_normSq h 1, walkComplexEdge_normSq h 2,
+      walkComplexEdge_normSq h 3, walkComplexEdge_normSq h 4,
+      hgram.dot12, hgram.dot13, hgram.dot14, hgram.dot23, hgram.dot24,
+      hgram.dot34]
+    ring
+
+/-- Geometry half of the frozen E2 solution interface. -/
+theorem e2_angle_parametrization
+    (p : Fin 7 → EuclideanSpace ℝ (Fin 2))
+    (hdiam : ∀ i : Fin 7, dist (p i) (p (i + 3)) = 1)
+    (hshort : ∀ i j : Fin 7, i ≠ j → j ≠ i + 3 → i ≠ j + 3 → dist (p i) (p j) < 1)
+    (hC : dist (p 0) (p 1) = dist (p 3) (p 4))
+    (hB : dist (p 1) (p 2) = dist (p 2) (p 3))
+    (hA₁ : dist (p 4) (p 5) = dist (p 5) (p 6))
+    (hA₂ : dist (p 5) (p 6) = dist (p 6) (p 0))
+    (hBA : dist (p 1) (p 2) < dist (p 4) (p 5))
+    (hAC : dist (p 4) (p 5) < dist (p 0) (p 1)) :
+    ∃ A B C : ℝ, E2AngleParametrization p A B C := by
+  let h : E2GeometryHypotheses p :=
+    { hdiam := hdiam
+      hshort := hshort
+      hC := hC
+      hB := hB
+      hA₁ := hA₁
+      hA₂ := hA₂
+      hBA := hBA
+      hAC := hAC }
+  obtain ⟨A, B, C, hBpos, hBAngle, hACAngle, hCthird, hclasses⟩ :=
+    ordered_angle_classes h
+  have hsum := star_angle_sum h hclasses
+  have hclosure := star_scalar_closure h hclasses hsum
+  have hedges := edge_formulas h hclasses
+  have hdictionary := distance_dictionary h hclasses
+  exact ⟨A, B, C,
+    { B_pos := hBpos
+      B_lt_A := hBAngle
+      A_lt_C := hACAngle
+      C_lt_pi_div_three := hCthird
+      angle_sum := hsum
+      closure := hclosure
+      edgeC := hedges.edgeC
+      edgeB := hedges.edgeB
+      edgeA := hedges.edgeA
+      q_sq := hdictionary.q_sq
+      ra_sq := hdictionary.ra_sq
+      rb_sq := hdictionary.rb_sq }⟩
+
+end LeanPool.Erdos132WeiE2.Geometry
diff --git a/LeanPool/Erdos132WeiE2/Geometry/Star.lean b/LeanPool/Erdos132WeiE2/Geometry/Star.lean
new file mode 100644
index 000000000..712754606
--- /dev/null
+++ b/LeanPool/Erdos132WeiE2/Geometry/Star.lean
@@ -0,0 +1,684 @@
+/-
+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.Geometry.Basic
+import Mathlib.Analysis.Convex.Independent
+import Mathlib.Analysis.Convex.Radon
+import Mathlib.Analysis.Convex.Strict.Extreme
+import Mathlib.Analysis.Convex.StrictConvexBetween
+import Mathlib.Analysis.InnerProductSpace.Convex
+
+/-!
+# The diameter star
+
+The main target of this file is the standard orientation of the seven-cycle
+formed by the unit diameter segments.
+-/
+
+namespace LeanPool.Erdos132WeiE2.Geometry
+
+open Metric
+
+/-- Two open line segments have a common point. -/
+def OpenSegmentsMeet (a b c d : Plane) : Prop :=
+  ∃ x, x ∈ openSegment ℝ a b ∧ x ∈ openSegment ℝ c d
+
+private theorem orientedArea_affine_combo
+    (a b c d : Plane) (r s : ℝ) (hrs : r + s = 1) :
+    orientedArea a b (r • c + s • d) =
+      r * orientedArea a b c + s * orientedArea a b d := by
+  have hre :
+      (toComplex (r • c + s • d) - toComplex a).re =
+        r * (toComplex c - toComplex a).re +
+          s * (toComplex d - toComplex a).re := by
+    simp only [toComplex, map_add, map_smul, Complex.add_re, Complex.smul_re,
+      Complex.sub_re]
+    linear_combination (complexPlaneEquiv.symm a).re * hrs
+  have him :
+      (toComplex (r • c + s • d) - toComplex a).im =
+        r * (toComplex c - toComplex a).im +
+          s * (toComplex d - toComplex a).im := by
+    simp only [toComplex, map_add, map_smul, Complex.add_im, Complex.smul_im,
+      Complex.sub_im]
+    linear_combination (complexPlaneEquiv.symm a).im * hrs
+  simp only [orientedArea]
+  rw [hre, him]
+  ring
+
+/-- A noncollinear triple has nonzero signed area in the chosen coordinates. -/
+private theorem orientedArea_ne_zero_of_not_collinear
+    {a b c : Plane} (hcol : ¬Collinear ℝ ({a, b, c} : Set Plane)) :
+    orientedArea a b c ≠ 0 := by
+  intro harea
+  apply hcol
+  rw [collinear_iff_exists_forall_eq_smul_vadd]
+  have hab : a ≠ b := by
+    intro hab
+    subst b
+    exact hcol (by simpa [Set.pair_comm] using collinear_pair ℝ a c)
+  let u : ℂ := toComplex b - toComplex a
+  let v : ℂ := toComplex c - toComplex a
+  have hu : u ≠ 0 := by
+    intro hu
+    have : toComplex b = toComplex a := sub_eq_zero.mp hu
+    have hba : b = a := complexPlaneEquiv.symm.injective (by
+      simpa [toComplex] using this)
+    exact hab hba.symm
+  have hcross : u.re * v.im - u.im * v.re = 0 := by
+    simpa [orientedArea, u, v] using harea
+  obtain ⟨r, hvr⟩ : ∃ r : ℝ, v = r • u := by
+    by_cases hure : u.re = 0
+    · have huim : u.im ≠ 0 := by
+        intro huim
+        apply hu
+        apply Complex.ext <;> simp_all
+      refine ⟨v.im / u.im, ?_⟩
+      apply Complex.ext
+      · simp only [Complex.smul_re]
+        have hvre : v.re = 0 := by
+          rw [hure, zero_mul, zero_sub] at hcross
+          have hproduct : u.im * v.re = 0 := by linarith
+          exact (mul_eq_zero.mp hproduct).resolve_left huim
+        simp [hure, hvre]
+      · simp only [Complex.smul_im]
+        change v.im = (v.im / u.im) * u.im
+        exact (div_mul_cancel₀ v.im huim).symm
+    · refine ⟨v.re / u.re, ?_⟩
+      apply Complex.ext
+      · simp only [Complex.smul_re]
+        change v.re = (v.re / u.re) * u.re
+        exact (div_mul_cancel₀ v.re hure).symm
+      · simp only [Complex.smul_im]
+        change v.im = (v.re / u.re) * u.im
+        field_simp
+        nlinarith
+  have hplane : c - a = r • (b - a) := by
+    apply complexPlaneEquiv.symm.injective
+    simpa [u, v, toComplex] using hvr
+  refine ⟨a, b - a, ?_⟩
+  intro x hx
+  simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx
+  rcases hx with rfl | rfl | rfl
+  · exact ⟨0, by simp⟩
+  · exact ⟨1, by simp⟩
+  · exact ⟨r, by simpa [vadd_eq_add] using (sub_eq_iff_eq_add.mp hplane)⟩
+
+/-- A proper segment crossing gives alternating signed areas once one area
+in each line direction is known to be nonzero. -/
+theorem alternating_oriented_areas_of_open_segments_meet
+    {a b c d : Plane} (hmeet : OpenSegmentsMeet a b c d)
+    (habc : orientedArea a b c ≠ 0) (hcda : orientedArea c d a ≠ 0) :
+    orientedArea a b c * orientedArea a b d < 0 ∧
+      orientedArea c d a * orientedArea c d b < 0 := by
+  obtain ⟨x, hxab, hxcd⟩ := hmeet
+  obtain ⟨r, s, hr, hs, hrs, hxAB⟩ := hxab
+  obtain ⟨u, v, hu, hv, huv, hxCD⟩ := hxcd
+  have hareaAB : orientedArea a b x = 0 := by
+    rw [← hxAB, orientedArea_affine_combo a b a b r s hrs]
+    simp only [orientedArea, sub_self, Complex.zero_re, Complex.zero_im, mul_zero]
+    ring
+  have hrelationAB :
+      u * orientedArea a b c + v * orientedArea a b d = 0 := by
+    rw [← hxCD, orientedArea_affine_combo a b c d u v huv] at hareaAB
+    exact hareaAB
+  have hareaCD : orientedArea c d x = 0 := by
+    rw [← hxCD, orientedArea_affine_combo c d c d u v huv]
+    simp only [orientedArea, sub_self, Complex.zero_re, Complex.zero_im, mul_zero]
+    ring
+  have hrelationCD :
+      r * orientedArea c d a + s * orientedArea c d b = 0 := by
+    rw [← hxAB, orientedArea_affine_combo c d a b r s hrs] at hareaCD
+    exact hareaCD
+  constructor
+  · have hscaled :
+        u * (orientedArea a b c) ^ 2 +
+          v * (orientedArea a b c * orientedArea a b d) = 0 := by
+      linear_combination orientedArea a b c * hrelationAB
+    have hpositive := mul_pos hu (sq_pos_of_ne_zero habc)
+    nlinarith
+  · have hscaled :
+        r * (orientedArea c d a) ^ 2 +
+          s * (orientedArea c d a * orientedArea c d b) = 0 := by
+      linear_combination orientedArea c d a * hrelationCD
+    have hpositive := mul_pos hr (sq_pos_of_ne_zero hcda)
+    nlinarith
+
+/-- With the endpoint order induced by two crossed edges, the two consecutive
+turns have the same strict sign. -/
+private theorem consecutive_turn_product_pos_of_open_segments_meet
+    {a b c d : Plane} (hmeet : OpenSegmentsMeet a b c d)
+    (habc : orientedArea a b c ≠ 0) (hcda : orientedArea c d a ≠ 0) :
+    0 < orientedArea a b c * orientedArea b c d := by
+  have hsigns :=
+    alternating_oriented_areas_of_open_segments_meet hmeet habc hcda
+  have hcyclicABC : orientedArea b c a = orientedArea a b c := by
+    simp only [orientedArea, Complex.sub_re, Complex.sub_im]
+    ring
+  have hcyclicBCD : orientedArea c d b = orientedArea b c d := by
+    simp only [orientedArea, Complex.sub_re, Complex.sub_im]
+    ring
+  have hbcd : orientedArea b c d ≠ 0 := by
+    intro hbcd
+    have hcdb : orientedArea c d b = 0 := by simpa [hcyclicBCD] using hbcd
+    rw [hcdb, mul_zero] at hsigns
+    linarith [hsigns.2]
+  obtain ⟨x, hxab, hxcd⟩ := hmeet
+  obtain ⟨r, s, hr, _hs, hrs, hxAB⟩ := hxab
+  obtain ⟨u, v, _hu, hv, huv, hxCD⟩ := hxcd
+  have hareaAB :
+      orientedArea b c x = r * orientedArea a b c := by
+    rw [← hxAB, orientedArea_affine_combo b c a b r s hrs, hcyclicABC]
+    simp only [orientedArea, sub_self, Complex.zero_re, Complex.zero_im,
+      mul_zero, add_zero]
+  have hareaCD :
+      orientedArea b c x = v * orientedArea b c d := by
+    rw [← hxCD, orientedArea_affine_combo b c c d u v huv]
+    simp only [orientedArea]
+    ring
+  have hrelation :
+      r * orientedArea a b c = v * orientedArea b c d := hareaAB.symm.trans hareaCD
+  have hscaled :
+      r * (orientedArea a b c) ^ 2 =
+        v * (orientedArea a b c * orientedArea b c d) := by
+    linear_combination orientedArea a b c * hrelation
+  have hpositive := mul_pos hr (sq_pos_of_ne_zero habc)
+  have hproduct_ne := mul_ne_zero habc hbcd
+  have hproduct_nonneg :
+      0 ≤ orientedArea a b c * orientedArea b c d := by
+    nlinarith
+  exact lt_of_le_of_ne hproduct_nonneg hproduct_ne.symm
+
+/-- The four endpoints of two diameter pairs are in convex position. -/
+private theorem diameter_endpoints_convexIndependent
+    {a b c d : Plane}
+    (hab : dist a b = 1) (hcd : dist c d = 1)
+    (hac : dist a c ≤ 1) (had : dist a d ≤ 1)
+    (hbc : dist b c ≤ 1) (hbd : dist b d ≤ 1)
+    (hacne : a ≠ c) (hadne : a ≠ d) (hbcne : b ≠ c) (hbdne : b ≠ d) :
+    ConvexIndependent ℝ ![a, b, c, d] := by
+  let f : Fin 4 → Plane := ![a, b, c, d]
+  let center : Fin 4 → Plane := ![b, a, d, c]
+  have habne : a ≠ b := by
+    intro h
+    have hzero : dist a b = 0 := dist_eq_zero.mpr h
+    linarith
+  have hcdne : c ≠ d := by
+    intro h
+    have hzero : dist c d = 0 := dist_eq_zero.mpr h
+    linarith
+  have hf : Function.Injective f := by
+    intro i j hij
+    fin_cases i <;> fin_cases j <;> simp_all [f]
+  have hall (i j : Fin 4) : dist (center i) (f j) ≤ 1 := by
+    fin_cases i <;> fin_cases j <;>
+      simp_all [center, f, dist_comm]
+  have hsphere (i : Fin 4) : dist (center i) (f i) = 1 := by
+    fin_cases i <;> simp_all [center, f, dist_comm]
+  intro s i hi
+  have hsubset : convexHull ℝ (f '' s) ⊆ closedBall (center i) 1 := by
+    apply convexHull_min
+    · rintro y ⟨j, hj, rfl⟩
+      exact mem_closedBall.mpr (by simpa [dist_comm] using hall i j)
+    · exact convex_closedBall _ _
+  have hboundary : f i ∈ sphere (center i) 1 := by
+    exact mem_sphere.mpr (by simpa [dist_comm] using hsphere i)
+  have hextremeBall : f i ∈ (closedBall (center i) 1).extremePoints ℝ :=
+    StrictConvexSpace.sphere_subset_extremePoints_closedBall
+      (center i) one_ne_zero hboundary
+  have hextremeHull : f i ∈ (convexHull ℝ (f '' s)).extremePoints ℝ :=
+    inter_extremePoints_subset_extremePoints_of_subset hsubset ⟨hi, hextremeBall⟩
+  obtain ⟨j, hjs, hji⟩ := extremePoints_convexHull_subset hextremeHull
+  simpa [hf hji] using hjs
+
+/-- A proper point on one side of a noncollinear triangle gives a strict
+triangle inequality through that point. -/
+private theorem strict_triangle_through_open_segment
+    {a b c x : Plane} (hx : x ∈ openSegment ℝ a c)
+    (hncol : ¬Collinear ℝ ({a, b, c} : Set Plane)) :
+    dist a b < dist a x + dist x b := by
+  rw [dist_lt_dist_add_dist_iff]
+  intro habx
+  have hxne : x ≠ a := by
+    intro h
+    subst x
+    have hac : a = c := (left_mem_openSegment_iff (𝕜 := ℝ)).mp hx
+    subst c
+    apply hncol
+    simpa [Set.pair_comm] using collinear_pair ℝ a b
+  have hxlineAB : x ∈ line[ℝ, a, b] := habx.mem_affineSpan
+  have hxlineAC : x ∈ line[ℝ, a, c] :=
+    (mem_segment_iff_wbtw.mp (openSegment_subset_segment ℝ a c hx)).mem_affineSpan
+  have hlineAB : line[ℝ, a, x] = line[ℝ, a, b] :=
+    affineSpan_pair_eq_of_right_mem_of_ne hxlineAB hxne
+  have hlineAC : line[ℝ, a, x] = line[ℝ, a, c] :=
+    affineSpan_pair_eq_of_right_mem_of_ne hxlineAC hxne
+  have hbline : b ∈ line[ℝ, a, c] := by
+    rw [← hlineAC, hlineAB]
+    exact right_mem_affineSpan_pair ℝ a b
+  apply hncol
+  simpa [Set.insert_comm] using collinear_insert_of_mem_affineSpan_pair hbline
+
+/-- If one pairing crosses properly, its two side lengths have strictly
+smaller sum than the crossed diagonal lengths. -/
+private theorem side_sum_lt_of_open_segments_meet
+    {a b c d : Plane}
+    (habc : ¬Collinear ℝ ({a, b, c} : Set Plane))
+    (hcda : ¬Collinear ℝ ({c, d, a} : Set Plane))
+    (hmeet : OpenSegmentsMeet a c b d) :
+    dist a b + dist c d < dist a c + dist b d := by
+  obtain ⟨x, hxac, hxbd⟩ := hmeet
+  have hab := strict_triangle_through_open_segment hxac habc
+  have hcd := strict_triangle_through_open_segment
+    (by simpa [openSegment_symm] using hxac) hcda
+  have hac : dist a x + dist x c = dist a c :=
+    dist_add_dist_eq_iff.mpr
+      (mem_segment_iff_wbtw.mp (openSegment_subset_segment ℝ a c hxac))
+  have hbd : dist b x + dist x d = dist b d :=
+    dist_add_dist_eq_iff.mpr
+      (mem_segment_iff_wbtw.mp (openSegment_subset_segment ℝ b d hxbd))
+  calc
+    dist a b + dist c d <
+        (dist a x + dist x b) + (dist c x + dist x d) := add_lt_add hab hcd
+    _ = (dist a x + dist x c) + (dist b x + dist x d) := by
+      rw [dist_comm x b, dist_comm c x]
+      ring
+    _ = dist a c + dist b d := by rw [hac, hbd]
+
+/-- Proper intersection depends only on the two unordered endpoint pairs. -/
+private theorem openSegmentsMeet_congr_pairs
+    {a b c d a' b' c' d' : Plane}
+    (hab : ({a, b} : Set Plane) = {a', b'})
+    (hcd : ({c, d} : Set Plane) = {c', d'})
+    (hmeet : OpenSegmentsMeet a b c d) : OpenSegmentsMeet a' b' c' d' := by
+  rcases Set.pair_eq_pair_iff.mp hab with hab | hab <;>
+    rcases Set.pair_eq_pair_iff.mp hcd with hcd | hcd <;>
+      simpa [OpenSegmentsMeet, hab.1, hab.2, hcd.1, hcd.2,
+        openSegment_symm, and_comm] using hmeet
+
+private theorem openSegmentsMeet_swap_pairs
+    {a b c d : Plane} (hmeet : OpenSegmentsMeet a b c d) :
+    OpenSegmentsMeet c d a b := by
+  simpa [OpenSegmentsMeet, and_comm] using hmeet
+
+/-- The three unordered two-two partitions of four labels. -/
+private theorem fin_four_partition_cases
+    (i j k l : Fin 4) (hji : j ≠ i)
+    (hcomp : ({k, l} : Set (Fin 4)) = ({i, j} : Set (Fin 4))ᶜ) :
+    ((({i, j} : Set (Fin 4)) = {0, 1} ∧ ({k, l} : Set (Fin 4)) = {2, 3}) ∨
+      (({i, j} : Set (Fin 4)) = {2, 3} ∧ ({k, l} : Set (Fin 4)) = {0, 1})) ∨
+    ((({i, j} : Set (Fin 4)) = {0, 2} ∧ ({k, l} : Set (Fin 4)) = {1, 3}) ∨
+      (({i, j} : Set (Fin 4)) = {1, 3} ∧ ({k, l} : Set (Fin 4)) = {0, 2})) ∨
+    (({i, j} : Set (Fin 4)) = {0, 3} ∧ ({k, l} : Set (Fin 4)) = {1, 2}) ∨
+      (({i, j} : Set (Fin 4)) = {1, 2} ∧ ({k, l} : Set (Fin 4)) = {0, 3}) := by
+  fin_cases i
+  · fin_cases j
+    · exact (hji rfl).elim
+    · exact Or.inl (Or.inl ⟨rfl, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩)
+    · exact Or.inr (Or.inl (Or.inl ⟨rfl, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+    · exact Or.inr (Or.inr (Or.inl ⟨by simp, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+  · fin_cases j
+    · exact Or.inl (Or.inl ⟨by exact Set.pair_comm _ _, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩)
+    · exact (hji rfl).elim
+    · exact Or.inr (Or.inr (Or.inr ⟨rfl, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+    · exact Or.inr (Or.inl (Or.inr ⟨by simp, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+  · fin_cases j
+    · exact Or.inr (Or.inl (Or.inl ⟨by exact Set.pair_comm _ _, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+    · exact Or.inr (Or.inr (Or.inr ⟨by exact Set.pair_comm _ _, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+    · exact (hji rfl).elim
+    · exact Or.inl (Or.inr ⟨by simp, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩)
+  · fin_cases j
+    · exact Or.inr (Or.inr (Or.inl ⟨by exact Set.pair_comm _ _, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+    · exact Or.inr (Or.inl (Or.inr ⟨by exact Set.pair_comm _ _, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩))
+    · exact Or.inl (Or.inr ⟨by exact Set.pair_comm _ _, hcomp.trans (by
+        ext m
+        fin_cases m <;> decide)⟩)
+    · exact (hji rfl).elim
+
+private theorem classify_fin_four_pairing
+    (f : Fin 4 → Plane) (i j k l : Fin 4) (hji : j ≠ i)
+    (hcomp : ({k, l} : Set (Fin 4)) = ({i, j} : Set (Fin 4))ᶜ)
+    (hmeet : OpenSegmentsMeet (f i) (f j) (f k) (f l)) :
+    OpenSegmentsMeet (f 0) (f 1) (f 2) (f 3) ∨
+      OpenSegmentsMeet (f 0) (f 2) (f 1) (f 3) ∨
+        OpenSegmentsMeet (f 0) (f 3) (f 1) (f 2) := by
+  rcases fin_four_partition_cases i j k l hji hcomp with h12 | hrest
+  · rcases h12 with h | h
+    · exact Or.inl (openSegmentsMeet_congr_pairs
+        (by simpa [Set.image_pair] using congrArg (f '' ·) h.1)
+        (by simpa [Set.image_pair] using congrArg (f '' ·) h.2) hmeet)
+    · exact Or.inl (openSegmentsMeet_congr_pairs
+        (by simpa [Set.image_pair] using congrArg (f '' ·) h.2)
+        (by simpa [Set.image_pair] using congrArg (f '' ·) h.1)
+        (openSegmentsMeet_swap_pairs hmeet))
+  · rcases hrest with h34 | hrest
+    · rcases h34 with h | h
+      · exact Or.inr (Or.inl (openSegmentsMeet_congr_pairs
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.1)
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.2) hmeet))
+      · exact Or.inr (Or.inl (openSegmentsMeet_congr_pairs
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.2)
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.1)
+          (openSegmentsMeet_swap_pairs hmeet)))
+    · rcases hrest with h | h
+      · exact Or.inr (Or.inr (openSegmentsMeet_congr_pairs
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.1)
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.2) hmeet))
+      · exact Or.inr (Or.inr (openSegmentsMeet_congr_pairs
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.2)
+          (by simpa [Set.image_pair] using congrArg (f '' ·) h.1)
+          (openSegmentsMeet_swap_pairs hmeet)))
+
+/-- Radon's theorem gives one of the three pairings as the proper diagonals
+of four convex-independent planar points. -/
+private theorem one_pairing_open_segments_meet
+    {a b c d : Plane} (hconv : ConvexIndependent ℝ ![a, b, c, d]) :
+    OpenSegmentsMeet a b c d ∨ OpenSegmentsMeet a c b d ∨
+      OpenSegmentsMeet a d b c := by
+  let f : Fin 4 → Plane := ![a, b, c, d]
+  have hf : ConvexIndependent ℝ f := by simpa [f] using hconv
+  have hdep : ¬AffineIndependent ℝ f := by
+    rw [← finrank_vectorSpan_le_iff_not_affineIndependent ℝ f (by decide : 4 = 2 + 2)]
+    exact (Submodule.finrank_le _).trans_eq (by simp [Plane])
+  obtain ⟨I, x, hxI, hxIc⟩ := Convex.radon_partition hdep
+  have hInonempty : I.Nonempty := by
+    have : (f '' I).Nonempty := convexHull_nonempty_iff.mp ⟨x, hxI⟩
+    exact Set.image_nonempty.mp this
+  have hIcNonempty : Iᶜ.Nonempty := by
+    have : (f '' Iᶜ).Nonempty := convexHull_nonempty_iff.mp ⟨x, hxIc⟩
+    exact Set.image_nonempty.mp this
+  have hother (S : Set (Fin 4))
+      (hxS : x ∈ convexHull ℝ (f '' S))
+      (hxSc : x ∈ convexHull ℝ (f '' Sᶜ)) :
+      ∀ i ∈ S, ∃ j ∈ S, j ≠ i := by
+    intro i hi
+    by_contra hnone
+    push Not at hnone
+    have hSeq : S = {i} := by
+      ext j
+      constructor
+      · intro hj
+        exact Set.mem_singleton_iff.mpr (hnone j hj)
+      · intro hj
+        have hji : j = i := by simpa using hj
+        simpa [hji] using hi
+    have hxi : x = f i := by
+      simpa [hSeq] using hxS
+    have hiSc : i ∈ Sᶜ := hf Sᶜ i (by simpa [← hxi] using hxSc)
+    exact (by simpa using hiSc : i ∉ S) hi
+  obtain ⟨i, hi⟩ := hInonempty
+  obtain ⟨j, hj, hji⟩ := hother I hxI hxIc i hi
+  obtain ⟨k, hk⟩ := hIcNonempty
+  obtain ⟨l, hl, hlk⟩ := hother Iᶜ hxIc (by simpa using hxI) k hk
+  let IF : Finset (Fin 4) := I.toFinite.toFinset
+  have hiIF : i ∈ IF := by simpa [IF] using hi
+  have hjIF : j ∈ IF := by simpa [IF] using hj
+  have hkIFc : k ∈ IFᶜ := by simpa [IF] using hk
+  have hlIFc : l ∈ IFᶜ := by simpa [IF] using hl
+  have hIFcard : IF.card = 2 := by
+    have hleft : 2 ≤ IF.card := by
+      rw [show 2 ≤ IF.card ↔ 1 < IF.card by omega, Finset.one_lt_card_iff]
+      exact ⟨i, j, hiIF, hjIF, hji.symm⟩
+    have hright : 2 ≤ IFᶜ.card := by
+      rw [show 2 ≤ IFᶜ.card ↔ 1 < IFᶜ.card by omega, Finset.one_lt_card_iff]
+      exact ⟨k, l, hkIFc, hlIFc, hlk.symm⟩
+    have htotal : IF.card + IFᶜ.card = 4 := by simp
+    omega
+  have hIFccard : IFᶜ.card = 2 := by
+    have htotal : IF.card + IFᶜ.card = 4 := by simp
+    omega
+  have hIFeq : IF = {i, j} := by
+    have hij : i ≠ j := hji.symm
+    have hpaircard : ({i, j} : Finset (Fin 4)).card = 2 := by simp [hij]
+    have hsubset : ({i, j} : Finset (Fin 4)) ⊆ IF := by
+      intro m hm
+      simp only [Finset.mem_insert, Finset.mem_singleton] at hm
+      rcases hm with rfl | rfl <;> assumption
+    have hcardle : IF.card ≤ ({i, j} : Finset (Fin 4)).card := by
+      rw [hIFcard, hpaircard]
+    exact (Finset.eq_of_subset_of_card_le hsubset hcardle).symm
+  have hIFceq : IFᶜ = {k, l} := by
+    have hkl : k ≠ l := hlk.symm
+    have hpaircard : ({k, l} : Finset (Fin 4)).card = 2 := by simp [hkl]
+    have hsubset : ({k, l} : Finset (Fin 4)) ⊆ IFᶜ := by
+      intro m hm
+      simp only [Finset.mem_insert, Finset.mem_singleton] at hm
+      rcases hm with rfl | rfl <;> assumption
+    have hcardle : IFᶜ.card ≤ ({k, l} : Finset (Fin 4)).card := by
+      rw [hIFccard, hpaircard]
+    exact (Finset.eq_of_subset_of_card_le hsubset hcardle).symm
+  have hIeq : I = {i, j} := by
+    ext m
+    calc
+      m ∈ I ↔ m ∈ IF := by simp [IF]
+      _ ↔ m ∈ ({i, j} : Finset (Fin 4)) := by rw [hIFeq]
+      _ ↔ m ∈ ({i, j} : Set (Fin 4)) := by simp
+  have hIceq : Iᶜ = {k, l} := by
+    ext m
+    calc
+      m ∈ Iᶜ ↔ m ∈ IFᶜ := by simp [IF]
+      _ ↔ m ∈ ({k, l} : Finset (Fin 4)) := by rw [hIFceq]
+      _ ↔ m ∈ ({k, l} : Set (Fin 4)) := by simp
+  have hxne (m : Fin 4) : f m ≠ x := by
+    intro hmx
+    by_cases hm : m ∈ I
+    · have : m ∈ Iᶜ := hf Iᶜ m (by simpa [hmx] using hxIc)
+      exact this hm
+    · have : m ∈ I := hf I m (by simpa [hmx] using hxI)
+      exact hm this
+  have hmeet : OpenSegmentsMeet (f i) (f j) (f k) (f l) := by
+    refine ⟨x, ?_, ?_⟩
+    · apply mem_openSegment_of_ne_left_right (hxne i) (hxne j)
+      simpa [hIeq, Set.image_pair, convexHull_pair] using hxI
+    · apply mem_openSegment_of_ne_left_right (hxne k) (hxne l)
+      simpa [hIceq, Set.image_pair, convexHull_pair] using hxIc
+  have hcomp : ({k, l} : Set (Fin 4)) = ({i, j} : Set (Fin 4))ᶜ := by
+    rw [← hIceq, hIeq]
+  simpa [f] using classify_fin_four_pairing f i j k l hji hcomp hmeet
+
+/-- Three different members of a convex-independent family are not collinear. -/
+private theorem convexIndependent_not_collinear
+    {ι : Type*} {f : ι → Plane} (hconv : ConvexIndependent ℝ f)
+    {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) :
+    ¬Collinear ℝ ({f i, f j, f k} : Set Plane) := by
+  intro hcol
+  rcases hcol.wbtw_or_wbtw_or_wbtw with h | h | h
+  · have hjmem : j ∈ ({i, k} : Set ι) := hconv {i, k} j (by
+      simpa [Set.image_pair, convexHull_pair] using h.mem_segment)
+    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hjmem
+    exact hjmem.elim (fun h ↦ hij h.symm) hjk
+  · have hkmem : k ∈ ({j, i} : Set ι) := hconv {j, i} k (by
+      simpa [Set.image_pair, convexHull_pair] using h.mem_segment)
+    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hkmem
+    exact hkmem.elim (fun h ↦ hjk h.symm) (fun h ↦ hik h.symm)
+  · have himem : i ∈ ({k, j} : Set ι) := hconv {k, j} i (by
+      simpa [Set.image_pair, convexHull_pair] using h.mem_segment)
+    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at himem
+    exact himem.elim hik (fun h ↦ hij h)
+
+/-- Two disjoint diameter pairs in a four-point set of diameter one cross properly. -/
+theorem four_point_diameter_segments_meet
+    {a b c d : Plane}
+    (hab : dist a b = 1) (hcd : dist c d = 1)
+    (hac : dist a c ≤ 1) (had : dist a d ≤ 1)
+    (hbc : dist b c ≤ 1) (hbd : dist b d ≤ 1)
+    (hacne : a ≠ c) (hadne : a ≠ d) (hbcne : b ≠ c) (hbdne : b ≠ d) :
+    OpenSegmentsMeet a b c d := by
+  have hconv := diameter_endpoints_convexIndependent hab hcd hac had hbc hbd
+    hacne hadne hbcne hbdne
+  have hpairing := one_pairing_open_segments_meet hconv
+  rcases hpairing with hcross | hcross | hcross
+  · exact hcross
+  · have habc : ¬Collinear ℝ ({a, b, c} : Set Plane) := by
+      simpa using convexIndependent_not_collinear hconv
+        (i := (0 : Fin 4)) (j := 1) (k := 2) (by decide) (by decide) (by decide)
+    have hcda : ¬Collinear ℝ ({c, d, a} : Set Plane) := by
+      simpa using convexIndependent_not_collinear hconv
+        (i := (2 : Fin 4)) (j := 3) (k := 0) (by decide) (by decide) (by decide)
+    have hlt := side_sum_lt_of_open_segments_meet habc hcda hcross
+    rw [hab, hcd] at hlt
+    linarith
+  · have habd : ¬Collinear ℝ ({a, b, d} : Set Plane) := by
+      simpa using convexIndependent_not_collinear hconv
+        (i := (0 : Fin 4)) (j := 1) (k := 3) (by decide) (by decide) (by decide)
+    have hdca : ¬Collinear ℝ ({d, c, a} : Set Plane) := by
+      simpa using convexIndependent_not_collinear hconv
+        (i := (3 : Fin 4)) (j := 2) (k := 0) (by decide) (by decide) (by decide)
+    have hlt := side_sum_lt_of_open_segments_meet habd hdca hcross
+    rw [hab, dist_comm d c, hcd] at hlt
+    linarith
+
+/-- All nonincident edges of the labelled diameter cycle cross properly. -/
+theorem all_diameter_edges_cross
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) :
+    ∀ i j : Fin 7,
+      i ≠ j → i ≠ j + 3 → i + 3 ≠ j → i + 3 ≠ j + 3 →
+        OpenSegmentsMeet (p i) (p (i + 3)) (p j) (p (j + 3)) := by
+  intro i j hij hij3 hi3j hi3j3
+  have hinjective := pairwise_distinct_of_diameter_pattern h
+  apply four_point_diameter_segments_meet
+  · exact h.hdiam i
+  · exact h.hdiam j
+  · exact dist_le_one_of_diameter_pattern h i j
+  · exact dist_le_one_of_diameter_pattern h i (j + 3)
+  · exact dist_le_one_of_diameter_pattern h (i + 3) j
+  · exact dist_le_one_of_diameter_pattern h (i + 3) (j + 3)
+  · exact hinjective.ne hij
+  · exact hinjective.ne hij3
+  · exact hinjective.ne hi3j
+  · exact hinjective.ne hi3j3
+
+/-- Four successive vertices of the diameter walk form the convex quadrilateral
+whose opposite diameter edges cross. -/
+private theorem walk_four_convexIndependent
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    ConvexIndependent ℝ
+      ![p (walkIndex k), p (walkIndex (k + 1)),
+        p (walkIndex (k + 2)), p (walkIndex (k + 3))] := by
+  apply diameter_endpoints_convexIndependent
+  · have hd := h.hdiam (walkIndex k)
+    fin_cases k <;> simpa [walkIndex] using hd
+  · have hd := h.hdiam (walkIndex (k + 2))
+    fin_cases k <;> simpa [walkIndex] using hd
+  · exact dist_le_one_of_diameter_pattern h _ _
+  · exact dist_le_one_of_diameter_pattern h _ _
+  · exact dist_le_one_of_diameter_pattern h _ _
+  · exact dist_le_one_of_diameter_pattern h _ _
+  · exact (pairwise_distinct_of_diameter_pattern h).ne (by
+      fin_cases k <;> decide)
+  · exact (pairwise_distinct_of_diameter_pattern h).ne (by
+      fin_cases k <;> decide)
+  · exact (pairwise_distinct_of_diameter_pattern h).ne (by
+      fin_cases k <;> decide)
+  · exact (pairwise_distinct_of_diameter_pattern h).ne (by
+      fin_cases k <;> decide)
+
+private theorem walk_turn_ne_zero
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    orientedArea (p (walkIndex k)) (p (walkIndex (k + 1)))
+      (p (walkIndex (k + 2))) ≠ 0 := by
+  apply orientedArea_ne_zero_of_not_collinear
+  simpa using convexIndependent_not_collinear (walk_four_convexIndependent h k)
+    (i := (0 : Fin 4)) (j := 1) (k := 2) (by decide) (by decide) (by decide)
+
+private theorem walk_cross_area_ne_zero
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    orientedArea (p (walkIndex (k + 2))) (p (walkIndex (k + 3)))
+      (p (walkIndex k)) ≠ 0 := by
+  apply orientedArea_ne_zero_of_not_collinear
+  simpa using convexIndependent_not_collinear (walk_four_convexIndependent h k)
+    (i := (2 : Fin 4)) (j := 3) (k := 0) (by decide) (by decide) (by decide)
+
+private theorem walk_edges_two_apart_cross
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    OpenSegmentsMeet
+      (p (walkIndex k)) (p (walkIndex (k + 1)))
+      (p (walkIndex (k + 2))) (p (walkIndex (k + 3))) := by
+  have hcross := all_diameter_edges_cross h (walkIndex k) (walkIndex (k + 2))
+    (by fin_cases k <;> decide) (by fin_cases k <;> decide)
+    (by fin_cases k <;> decide) (by fin_cases k <;> decide)
+  fin_cases k <;> simpa [walkIndex] using hcross
+
+private theorem consecutive_walk_turn_product_pos
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) (k : Fin 7) :
+    0 < orientedArea (p (walkIndex k)) (p (walkIndex (k + 1)))
+        (p (walkIndex (k + 2))) *
+      orientedArea (p (walkIndex (k + 1))) (p (walkIndex (k + 2)))
+        (p (walkIndex (k + 3))) := by
+  exact consecutive_turn_product_pos_of_open_segments_meet
+    (walk_edges_two_apart_cross h k) (walk_turn_ne_zero h k)
+    (walk_cross_area_ne_zero h k)
+
+/-- Along the diameter-cycle walk, every turn has one common orientation. -/
+def SameTurnStar (p : Fin 7 → Plane) : Prop :=
+  ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧
+    ∀ k : Fin 7,
+      0 < ε * orientedArea
+        (p (walkIndex k)) (p (walkIndex (k + 1))) (p (walkIndex (k + 2)))
+
+/-- The seven unit diameters have the standard star orientation, up to reflection. -/
+theorem diameter_star_structure
+    {p : Fin 7 → Plane} (h : E2GeometryHypotheses p) : SameTurnStar p := by
+  let turn : Fin 7 → ℝ := fun k ↦
+    orientedArea (p (walkIndex k)) (p (walkIndex (k + 1)))
+      (p (walkIndex (k + 2)))
+  have hstep (k : Fin 7) : 0 < turn k * turn (k + 1) := by
+    have hs := consecutive_walk_turn_product_pos h k
+    fin_cases k <;> simpa [turn] using hs
+  have hne : turn 0 ≠ 0 := by simpa [turn] using walk_turn_ne_zero h 0
+  have next_negative {x y : ℝ} (hx : x < 0) (hxy : 0 < x * y) : y < 0 := by
+    rcases mul_pos_iff.mp hxy with hpos | hneg
+    · linarith [hpos.1]
+    · exact hneg.2
+  have next_positive {x y : ℝ} (hx : 0 < x) (hxy : 0 < x * y) : 0 < y := by
+    rcases mul_pos_iff.mp hxy with hpos | hneg
+    · exact hpos.2
+    · linarith [hneg.1]
+  rcases lt_or_gt_of_ne hne with hnegative | hpositive
+  · have h1 : turn 1 < 0 := next_negative hnegative (by simpa using hstep 0)
+    have h2 : turn 2 < 0 := next_negative h1 (by simpa using hstep 1)
+    have h3 : turn 3 < 0 := next_negative h2 (by simpa using hstep 2)
+    have h4 : turn 4 < 0 := next_negative h3 (by simpa using hstep 3)
+    have h5 : turn 5 < 0 := next_negative h4 (by simpa using hstep 4)
+    have h6 : turn 6 < 0 := next_negative h5 (by simpa using hstep 5)
+    refine ⟨-1, Or.inr rfl, ?_⟩
+    intro k
+    have hk : turn k < 0 := by
+      fin_cases k <;> assumption
+    simpa [turn] using (show 0 < (-1 : ℝ) * turn k by linarith)
+  · have h1 : 0 < turn 1 := next_positive hpositive (by simpa using hstep 0)
+    have h2 : 0 < turn 2 := next_positive h1 (by simpa using hstep 1)
+    have h3 : 0 < turn 3 := next_positive h2 (by simpa using hstep 2)
+    have h4 : 0 < turn 4 := next_positive h3 (by simpa using hstep 3)
+    have h5 : 0 < turn 5 := next_positive h4 (by simpa using hstep 4)
+    have h6 : 0 < turn 6 := next_positive h5 (by simpa using hstep 5)
+    refine ⟨1, Or.inl rfl, ?_⟩
+    intro k
+    have hk : 0 < turn k := by
+      fin_cases k <;> assumption
+    simpa [turn] using hk
+
+end LeanPool.Erdos132WeiE2.Geometry
diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml
index 563c654dd..fe96e3d82 100644
--- a/LeanPool/projects.yml
+++ b/LeanPool/projects.yml
@@ -7255,3 +7255,59 @@ projects:
       - "11T06"
       - "11T71"
       - "94A60"
+  - slug: erdos132-wei-e2
+    title: Six distances from the E2 diameter-heptagon pattern
+    summary: >-
+      Formalizes the repaired E2 case in the diameter-seven-cycle analysis of
+      Wei, Li, Cong, and Gao. Seven planar points whose unit-distance diameter
+      graph is the step-three 7-cycle and whose boundary edges have ordered
+      classes B < A < C realize at least six distinct pairwise distances. The
+      proof extracts an angle parametrization from the geometry, derives exact
+      trigonometric and polynomial identities, excludes every five-value
+      collapse, and finishes by finite counting. This is the independently
+      significant repaired E2 step; it does not completely solve Erdős problem 132.
+    branch: discrete geometry
+    entry_module: LeanPool.Erdos132WeiE2
+    authors:
+      - Egor Lyfar
+    source:
+      title: Distance sets with diameter graph being cycle
+      authors:
+        - Xianglin Wei
+        - Guogang Li
+        - Yue Cong
+        - Feixing Gao
+      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
+      github_repo: lyfar/erdos132-wei-certificates
+    license: Apache-2.0
+    status: verified
+    provenance: AI
+    main_declarations:
+      - LeanPool.Erdos132WeiE2.e2_pattern_six_distances
+    main_results:
+      - declaration: LeanPool.Erdos132WeiE2.e2_pattern_six_distances
+        informal: >-
+          Seven planar points whose unit-distance diameter graph is the step-three 7-cycle, with
+          boundary edge classes ordered B < A < C, realize at least six distinct pairwise distances —
+          the repaired E2 step of Wei, Li, Cong, and Gao (2014), from the original geometric hypotheses.
+      - declaration: LeanPool.Erdos132WeiE2.Geometry.e2_angle_parametrization
+        informal: >-
+          The E2 geometric hypotheses yield ordered real parameters B < A < C satisfying
+          the angle-sum, closure, edge-length, and diagonal identities used by the
+          six-distance argument.
+      - declaration: LeanPool.Erdos132WeiE2.Counting.six_distances_of_parametrization
+        informal: >-
+          Any seven planar points with a unit 0–3 diagonal, short 0–2 and 0–5 diagonals,
+          boundary distances ordered 1–2 < 4–5 < 0–1, and parameters
+          0 < B < A < C < π/3 satisfying the E2 angle sum, closure equation,
+          three edge formulas, and three squared-diagonal formulas realize at least six
+          distinct pairwise distances.
+    tags:
+      - discrete-geometry
+      - distance-sets
+      - diameter-graph
+      - erdos-problems
+    msc:
+      - "52C10"
+      - "05C62"