Challenge: six distances from the E2 diameter-heptagon pattern

Challenge.lean

@@ -1,3 +1,4 @@
 import Challenge.Mazur
 import Challenge.McKay
 import Challenge.Odlyzko
+import Challenge.WeiLiCongGao

Challenge/WeiLiCongGao.lean

@@ -0,0 +1,55 @@
+/-
+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
+
+/-!
+# Six distances from the E2 diameter-heptagon pattern
+
+Source: doi:10.11650/tjm.18.2014.4030, url:https://github.com/lyfar/erdos132-wei-certificates
+Proposed by: Egor Lyfar
+Open declarations: `Challenge.WeiLiCongGao.e2_pattern_six_distances`
+Tags: discrete-geometry, distance-sets, diameter-graph, erdos-132
+MSC: 52C10, 05C62
+Estimated size: ~4000 lines of Lean
+
+Informal statement:
+* `Challenge.WeiLiCongGao.e2_pattern_six_distances` — Take seven points in the plane, indexed by i =
+  0..6, with all pairwise distances at most 1, such that the distance between points i and i+3 (mod
+  7) is exactly 1 for every i, and every other pair is at strictly smaller distance. Suppose the
+  seven boundary edges d(i, i+1 mod 7) satisfy e0 = e3, e1 = e2, e4 = e5 = e6, and e1 < e4 < e0.
+  Then the number of distinct values among the pairwise distances of the seven points is at least
+  six.
+-/
+
+namespace Challenge.WeiLiCongGao
+
+/-- **The repaired E2 step of Wei–Li–Cong–Gao (2014), Theorem 4.** Seven planar points whose
+diameter graph is exactly the 7-cycle `{i, i+3}` of unit diameters, with boundary-edge pattern
+`(C, B, B, C, A, A, A)` and `B < A < C`, realize at least six distinct pairwise distances.
+
+The published proof of Theorem 4 handles this configuration by a value-swap appeal ("the proof is
+similar"); an exact line audit found that on this pattern the intended strict comparison is an
+exact equality, so the published argument does not close the case. A computational repair —
+reducing the seven undetermined diagonals to three algebraic classes and excluding every
+five-distance label assignment by unit Gröbner ideals over `ℚ` — establishes the statement; this
+challenge asks for the Lean proof. The bound is sharp: the configuration family generically
+realizes seven distinct distances and drops to exactly six at three isolated configurations, never
+to five. -/
+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 := sorry
+
+end Challenge.WeiLiCongGao

Challenge/challenges.yml

@@ -157,3 +157,64 @@ challenges:
     msc:
       - "20C15"
       - "20D20"
+  - slug: diameter-heptagon-e2-six-distances
+    title: Six distances from the E2 diameter-heptagon pattern
+    summary: >-
+      Seven planar points of diameter 1 whose diameter graph is exactly the
+      7-cycle {i, i+3 mod 7}, with boundary-edge pattern (C, B, B, C, A, A, A)
+      and B < A < C, realize at least six distinct pairwise distances. This is
+      the repaired E2 step of Theorem 4 of Wei-Li-Cong-Gao (2014), the result
+      the classification of 11-point 5-distance sets (Wei, Ars Combin. 102,
+      2011) depends on at m = 7 — a chain a line audit found to carry five
+      omitted proofs. The published proof handles E2 by a value-swap appeal
+      ("the proof is similar"); the audit found that on this pattern the
+      intended strict comparison is an exact equality on a reachable
+      configuration, so the published argument does not close the case. An
+      exact computational repair — the seven undetermined diagonals collapse
+      into three algebraic classes, one forced between the C-edge and the
+      diameter, and every five-distance label assignment dies by a unit
+      Gröbner ideal over the rationals — establishes the statement
+      (certificates and audit: https://github.com/lyfar/erdos132-wei-certificates).
+      The bound is sharp: the configuration family generically realizes seven
+      distinct distances and drops to exactly six at three isolated
+      configurations, never five. A Lean proof would put the repaired step of
+      the E11(5) classification — which Marchetto's n = 11 and n = 12 results
+      for Erdős #132 cite directly — on formal ground. The line estimate
+      covers the diameter-graph structure theory (odd cycles of unit
+      diameters, absent from Mathlib), the one-parameter reduction, and three
+      polynomial-identity certificates.
+    branch: discrete geometry
+    entry_module: Challenge.WeiLiCongGao
+    proposers:
+      - Egor Lyfar
+    source:
+      title: Distance sets with diameter graph being cycle
+      authors:
+        - Xianglin Wei
+        - Zhengyu Li
+        - Meiqin Cong
+        - Yan Gao
+      doi: "10.11650/tjm.18.2014.4030"
+      url: https://github.com/lyfar/erdos132-wei-certificates
+    license: Apache-2.0
+    provenance: AI
+    status: open
+    estimated_lines: 4000
+    statements:
+      - declaration: Challenge.WeiLiCongGao.e2_pattern_six_distances
+        informal: >-
+          Take seven points in the plane, indexed by i = 0..6, with all
+          pairwise distances at most 1, such that the distance between points
+          i and i+3 (mod 7) is exactly 1 for every i, and every other pair is
+          at strictly smaller distance. Suppose the seven boundary edges
+          d(i, i+1 mod 7) satisfy e0 = e3, e1 = e2, e4 = e5 = e6, and
+          e1 < e4 < e0. Then the number of distinct values among the pairwise
+          distances of the seven points is at least six.
+    tags:
+      - discrete-geometry
+      - distance-sets
+      - diameter-graph
+      - erdos-132
+    msc:
+      - "52C10"
+      - "05C62"