Import Erdos97ConvexOctagon with a regenerable staged LRAT certificate

LeanPool.lean

@@ -795,6 +795,95 @@ import LeanPool.Erdos403
 import LeanPool.Erdos403.Basic
 import LeanPool.Erdos403.FactBase
 import LeanPool.Erdos403.Sharp
+import LeanPool.Erdos97ConvexOctagon
+import LeanPool.Erdos97ConvexOctagon.Basic
+import LeanPool.Erdos97ConvexOctagon.CayleyMenger
+import LeanPool.Erdos97ConvexOctagon.Certificates
+import LeanPool.Erdos97ConvexOctagon.Classification
+import LeanPool.Erdos97ConvexOctagon.CoverageBranches
+import LeanPool.Erdos97ConvexOctagon.CoverageData
+import LeanPool.Erdos97ConvexOctagon.CoverageData00
+import LeanPool.Erdos97ConvexOctagon.CoverageData01
+import LeanPool.Erdos97ConvexOctagon.CoverageData02
+import LeanPool.Erdos97ConvexOctagon.CoverageData03
+import LeanPool.Erdos97ConvexOctagon.CoverageData04
+import LeanPool.Erdos97ConvexOctagon.CoverageData05
+import LeanPool.Erdos97ConvexOctagon.CoverageData06
+import LeanPool.Erdos97ConvexOctagon.CoverageData07
+import LeanPool.Erdos97ConvexOctagon.CoverageData08
+import LeanPool.Erdos97ConvexOctagon.CoverageData09
+import LeanPool.Erdos97ConvexOctagon.CoverageData10
+import LeanPool.Erdos97ConvexOctagon.CoverageData11
+import LeanPool.Erdos97ConvexOctagon.CoverageData12
+import LeanPool.Erdos97ConvexOctagon.CoverageData13
+import LeanPool.Erdos97ConvexOctagon.CoverageData14
+import LeanPool.Erdos97ConvexOctagon.CoverageData15
+import LeanPool.Erdos97ConvexOctagon.CoverageData16
+import LeanPool.Erdos97ConvexOctagon.CoverageData17
+import LeanPool.Erdos97ConvexOctagon.CoverageData18
+import LeanPool.Erdos97ConvexOctagon.CoverageData19
+import LeanPool.Erdos97ConvexOctagon.CoverageData20
+import LeanPool.Erdos97ConvexOctagon.CoverageData21
+import LeanPool.Erdos97ConvexOctagon.CoverageData22
+import LeanPool.Erdos97ConvexOctagon.CoverageData23
+import LeanPool.Erdos97ConvexOctagon.CoverageData24
+import LeanPool.Erdos97ConvexOctagon.CoverageData25
+import LeanPool.Erdos97ConvexOctagon.CoverageData26
+import LeanPool.Erdos97ConvexOctagon.CoverageData27
+import LeanPool.Erdos97ConvexOctagon.CoverageData28
+import LeanPool.Erdos97ConvexOctagon.CoverageData29
+import LeanPool.Erdos97ConvexOctagon.CoverageData30
+import LeanPool.Erdos97ConvexOctagon.CoverageData31
+import LeanPool.Erdos97ConvexOctagon.CoverageDataTypes
+import LeanPool.Erdos97ConvexOctagon.CoverageFormula
+import LeanPool.Erdos97ConvexOctagon.CycleStrip
+import LeanPool.Erdos97ConvexOctagon.EquidistantFour
+import LeanPool.Erdos97ConvexOctagon.FiniteModel
+import LeanPool.Erdos97ConvexOctagon.GeometryReduction
+import LeanPool.Erdos97ConvexOctagon.Gram
+import LeanPool.Erdos97ConvexOctagon.Incidence
+import LeanPool.Erdos97ConvexOctagon.LRAT.Elab
+import LeanPool.Erdos97ConvexOctagon.LRAT.Format
+import LeanPool.Erdos97ConvexOctagon.LRAT.Semantics
+import LeanPool.Erdos97ConvexOctagon.Main
+import LeanPool.Erdos97ConvexOctagon.MasterCertificate
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData0
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData1
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData2
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData3
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData4
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData5
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData6
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData7
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateData8
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateManifest
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateStage00
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateStage01
+import LeanPool.Erdos97ConvexOctagon.MasterCertificateStage02
+import LeanPool.Erdos97ConvexOctagon.MasterFormula
+import LeanPool.Erdos97ConvexOctagon.MasterFormulaData
+import LeanPool.Erdos97ConvexOctagon.Obstructions
+import LeanPool.Erdos97ConvexOctagon.Pentagon
+import LeanPool.Erdos97ConvexOctagon.Radius
+import LeanPool.Erdos97ConvexOctagon.Regenerate
+import LeanPool.Erdos97ConvexOctagon.Relabelling
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra00
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra01
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra02
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra03
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra04
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra05
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra06
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra07
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra08
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra09
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra10
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra11
+import LeanPool.Erdos97ConvexOctagon.ResidualAlgebra12
+import LeanPool.Erdos97ConvexOctagon.ResidualObstructions
+import LeanPool.Erdos97ConvexOctagon.ResidualRepresentatives
+import LeanPool.Erdos97ConvexOctagon.RhombusFan
+import LeanPool.Erdos97ConvexOctagon.RowSymmetry
 import LeanPool.ErdosMoser
 import LeanPool.ErdosMoser.Basic
 import LeanPool.ErdosMoser.Bounds

LeanPool/Erdos97ConvexOctagon.lean

@@ -0,0 +1,18 @@
+/-
+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.Erdos97ConvexOctagon.Main
+
+/-!
+# The Convex-Octagon Case of Erdős Problem 97
+
+Source: doi:10.1080/00029890.1946.11991674, url:https://www.erdosproblems.com/97
+Authors: Egor Lyfar
+Status: verified
+Main declarations: `Erdos97Octagon.erdos97_convex_octagon`
+Tags: discrete-geometry, distance-geometry, erdos-problems, convexity
+MSC: 51K05, 52A10
+-/

LeanPool/Erdos97ConvexOctagon/Basic.lean

@@ -0,0 +1,22 @@
+/-
+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.InnerProductSpace.PiL2
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.LinearAlgebra.Dimension.Finite
+import Mathlib.LinearAlgebra.LinearIndependent.Defs
+
+/-! # Erdős 97 convex-octagon formalization: Basic -/
+
+namespace Erdos97Octagon
+
+open scoped InnerProductSpace
+open Module
+
+/-- The Euclidean plane, represented as `EuclideanSpace ℝ (Fin 2)`. -/
+abbrev Plane := EuclideanSpace ℝ (Fin 2)
+
+end Erdos97Octagon

LeanPool/Erdos97ConvexOctagon/CayleyMenger.lean

@@ -0,0 +1,84 @@
+/-
+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.Erdos97ConvexOctagon.Gram
+
+/-! # Erdős 97 convex-octagon formalization: Cayley Menger -/
+
+namespace Erdos97Octagon
+
+open scoped InnerProductSpace
+
+/-- Squared Euclidean distance. -/
+noncomputable def sqDist (a b : Plane) : ℝ := dist a b ^ 2
+
+/-- The four-point Cayley--Menger polynomial in its six squared distances. -/
+def cm4 (A B C D E F : ℝ) : ℝ :=
+  -2 * A ^ 2 * F - 2 * A * B * D + 2 * A * B * E + 2 * A * B * F +
+    2 * A * C * D - 2 * A * C * E + 2 * A * C * F + 2 * A * D * F +
+    2 * A * E * F - 2 * A * F ^ 2 - 2 * B ^ 2 * E + 2 * B * C * D +
+    2 * B * C * E - 2 * B * C * F + 2 * B * D * E - 2 * B * E ^ 2 +
+    2 * B * E * F - 2 * C ^ 2 * D - 2 * C * D ^ 2 + 2 * C * D * E +
+    2 * C * D * F - 2 * D * E * F
+
+/-- Polarisation expresses an inner product through three squared distances. -/
+theorem inner_sub_sub_eq
+    (a b c : Plane) :
+    ⟪b - a, c - a⟫_ℝ = (sqDist a b + sqDist a c - sqDist b c) / 2 := by
+  have hsub : (b - a) - (c - a) = b - c := by abel
+  have h := norm_sub_sq_real (b - a) (c - a)
+  rw [hsub, ← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm] at h
+  simp only [sqDist]
+  rw [dist_comm b a, dist_comm c a] at h
+  nlinarith
+
+/-- Four planar points have vanishing Cayley--Menger determinant. -/
+theorem cm4_sqDist_eq_zero (a b c d : Plane) :
+    cm4 (sqDist a b) (sqDist a c) (sqDist a d)
+      (sqDist b c) (sqDist b d) (sqDist c d) = 0 := by
+  have h := gram_det_eq_zero ![b - a, c - a, d - a]
+  rw [gram3_expand] at h
+  have n1 : ⟪b - a, b - a⟫_ℝ = sqDist a b := by
+    rw [real_inner_self_eq_norm_sq, ← dist_eq_norm]
+    simp only [sqDist, dist_comm b a]
+  have n2 : ⟪c - a, c - a⟫_ℝ = sqDist a c := by
+    rw [real_inner_self_eq_norm_sq, ← dist_eq_norm]
+    simp only [sqDist, dist_comm c a]
+  have n3 : ⟪d - a, d - a⟫_ℝ = sqDist a d := by
+    rw [real_inner_self_eq_norm_sq, ← dist_eq_norm]
+    simp only [sqDist, dist_comm d a]
+  have i12 := inner_sub_sub_eq a b c
+  have i13 := inner_sub_sub_eq a b d
+  have i23 := inner_sub_sub_eq a c d
+  have i21 : ⟪c - a, b - a⟫_ℝ =
+      (sqDist a b + sqDist a c - sqDist b c) / 2 := by
+    rw [real_inner_comm]
+    exact i12
+  have i31 : ⟪d - a, b - a⟫_ℝ =
+      (sqDist a b + sqDist a d - sqDist b d) / 2 := by
+    rw [real_inner_comm]
+    exact i13
+  have i32 : ⟪d - a, c - a⟫_ℝ =
+      (sqDist a c + sqDist a d - sqDist c d) / 2 := by
+    rw [real_inner_comm]
+    exact i23
+  rw [n1, n2, n3, i12, i13, i23, i21, i31, i32] at h
+  dsimp [cm4]
+  ring_nf at h ⊢
+  linarith
+
+/-- The Cayley--Menger identity remains zero after dividing all squared
+distances by one common nonzero scale. -/
+theorem cm4_normalized_eq_zero
+    (a b c d : Plane) {s : ℝ} (hs : s ≠ 0) :
+    cm4 (sqDist a b / s) (sqDist a c / s) (sqDist a d / s)
+      (sqDist b c / s) (sqDist b d / s) (sqDist c d / s) = 0 := by
+  have h := cm4_sqDist_eq_zero a b c d
+  dsimp [cm4] at h ⊢
+  field_simp [hs]
+  nlinarith
+
+end Erdos97Octagon