Published inputs for the conditional fourteen-point theorem

Exactly two external interfaces remain. They record the published cardinality bound for planar sets with at most six distances and the Szöllősi--Östergård classification of thirteen-point six-distance sets. The Hopf--Pannwitz low-multiplicity diameter consequence is proved in HopfPannwitz.lean.

The cardinality interface packages the known planar maxima through six distances. Its exact six-distance case is Wei's theorem g(6) = 13; the smaller cases and their sources are summarized in Table 1 of the Szöllősi--Östergård paper. The classification interface is Theorem 16 of that paper and returns only a genuine Euclidean distance-scaling similarity to one of the three explicit coordinate templates.

inductive LeanPool.Erdos132N14.ThirteenPointSixDistanceClassification {ι : Type} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) : Prop

The three outcomes of the published maximum six-distance classification.

• regular13 {ι : Type} [LinearOrder ι] {P : Configuration ι} {S : Finset ι} : ∀ (a : SimilarTo P S regularTridecagon.point), ThirteenPointSixDistanceClassification P S
• dodecagonWithCenter {ι : Type} [LinearOrder ι] {P : Configuration ι} {S : Finset ι} : ∀ (a : SimilarTo P S Erdos132N14.dodecagonWithCenter.point), ThirteenPointSixDistanceClassification P S
• hexagramWithCenter {ι : Type} [LinearOrder ι] {P : Configuration ι} {S : Finset ι} : ∀ (a : SimilarTo P S Erdos132N14.hexagramWithCenter.point), ThirteenPointSixDistanceClassification P S

def LeanPool.Erdos132N14.PublishedAtMostSixDistanceCardinalityBound : Prop

Published planar few-distance input: a set determining at most six distances has at most thirteen points. This combines the known maxima through five distances with Wei's exact six-distance theorem g(6) = 13.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Erdos132N14.SzollosiOstergardThirteenPointSixDistanceClassification : Prop

Published Szöllősi--Östergård input: every thirteen-point planar six-distance set is similar to one of the three explicit templates.

Equations

• One or more equations did not get rendered due to their size.