Pair budget and endpoint deletion at fourteen points

Starting from failure of the two-low-multiplicity conclusion, this module derives the exact multiplicity profile (1, 15, 15, 15, 15, 15, 15). It then deletes one endpoint of the unique pair in the first class and proves that the realized-distance set is exactly the old set with that class erased.

def LeanPool.Erdos132N14.Erdos132ForFourteen (P : Configuration (Fin 14)) : Prop

The fourteen-point assertion in the first clause of Erdős Problem 132.

Equations

• LeanPool.Erdos132N14.Erdos132ForFourteen P = (2 ≤ (P.lowMultiplicityDistances Finset.univ 14).card)

theorem LeanPool.Erdos132N14.pairs_univ_fin_fourteen_card : (pairs Finset.univ).card = 91

structure LeanPool.Erdos132N14.FourteenFailureExactProfile (P : Configuration (Fin 14)) : Type

Exact information forced by a hypothetical failure at fourteen points.

• rareDistance : ℝ

  The unique low-multiplicity realized distance.

• rareDistance_mem : self.rareDistance ∈ P.realizedDistances Finset.univ
• realizedDistance_card : (P.realizedDistances Finset.univ).card = 7
• rareMultiplicity : P.distanceMultiplicity Finset.univ self.rareDistance = 1
• otherMultiplicity (d : ℝ) : d ∈ P.realizedDistances Finset.univ → d ≠ self.rareDistance → P.distanceMultiplicity Finset.univ d = 15
• rarePair : Fin 14 × Fin 14

  The unique increasing pair realizing the rare distance.

• rarePairFiber : {e ∈ pairs Finset.univ | P.pairDistance e = self.rareDistance} = {self.rarePair}

theorem LeanPool.Erdos132N14.fourteen_failure_exact_profile (hopfPannwitz : HopfPannwitzLowMultiplicityDistance14) (publishedCardinality : PublishedAtMostSixDistanceCardinalityBound) (P : Configuration (Fin 14)) (hfailure : ¬Erdos132ForFourteen P) : Nonempty (FourteenFailureExactProfile P)

def LeanPool.Erdos132N14.FourteenFailureExactProfile.deletedVertex {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : Fin 14

The deleted endpoint of the unique rare pair.

Equations

• profile.deletedVertex = profile.rarePair.1

def LeanPool.Erdos132N14.FourteenFailureExactProfile.retainedEndpoint {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : Fin 14

The other endpoint of the unique rare pair.

Equations

• profile.retainedEndpoint = profile.rarePair.2

def LeanPool.Erdos132N14.FourteenFailureExactProfile.remaining {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : Finset (Fin 14)

The thirteen labels left after endpoint deletion.

Equations

• profile.remaining = Finset.univ.erase profile.deletedVertex

theorem LeanPool.Erdos132N14.FourteenFailureExactProfile.rarePair_mem {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : profile.rarePair ∈ pairs Finset.univ

theorem LeanPool.Erdos132N14.FourteenFailureExactProfile.rarePair_distance {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : P.pairDistance profile.rarePair = profile.rareDistance

theorem LeanPool.Erdos132N14.FourteenFailureExactProfile.retainedEndpoint_mem_remaining {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : profile.retainedEndpoint ∈ profile.remaining

theorem LeanPool.Erdos132N14.FourteenFailureExactProfile.remaining_card {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : profile.remaining.card = 13

theorem LeanPool.Erdos132N14.FourteenFailureExactProfile.erase_endpoint_realizedDistances_eq_erase {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : P.realizedDistances profile.remaining = (P.realizedDistances Finset.univ).erase profile.rareDistance

Deleting the endpoint removes exactly the unique rare distance class.

theorem LeanPool.Erdos132N14.FourteenFailureExactProfile.remaining_realizedDistance_card {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : (P.realizedDistances profile.remaining).card = 6