Conditional fourteen-point theorem for Erdős Problem 132

This file eliminates the three classified thirteen-point branches after the internal diameter descent. The two exceptional templates contradict the fifteen-pair ceiling. In the regular branch, insertion counts give one rare distance and two copies of each regular chord; the explicit coordinate moments then contradict planar Cauchy--Schwarz.

The result is conditional on the two interfaces in PublishedInputs.lean. The planar diameter bound is proved internally. It does not settle Erdős Problem 132 in general.

theorem LeanPool.Erdos132N14.sum_of_one_rare_and_double_chords (f : Fin 13 → ℝ) (weight : ℝ → ℝ) (rare : ℝ) (hcover : ∀ (i : Fin 13), f i ∈ insert rare (Finset.image regularTridecagonChord Finset.univ)) (hrareNotChord : ∀ (k : Fin 6), rare ≠ regularTridecagonChord k) (hrareCard : {i : Fin 13 | f i = rare}.card = 1) (hchordCard : ∀ (k : Fin 6), {i : Fin 13 | f i = regularTridecagonChord k}.card = 2) : ∑ i : Fin 13, weight (f i) = weight rare + 2 * ∑ k : Fin 6, weight (regularTridecagonChord k)

theorem LeanPool.Erdos132N14.regular_scaled_chords_eq_realized {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (h : SimilarTo P profile.remaining regularTridecagon.point) : Finset.image (fun (k : Fin 6) => h.similarity.ratio * regularTridecagonChord k) Finset.univ = P.realizedDistances profile.remaining

theorem LeanPool.Erdos132N14.regular_remaining_chord_multiplicity {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (h : SimilarTo P profile.remaining regularTridecagon.point) (k : Fin 6) : P.distanceMultiplicity profile.remaining (h.similarity.ratio * regularTridecagonChord k) = 13

theorem LeanPool.Erdos132N14.classified_template_with_large_class_impossible {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (Q : Configuration (Fin 13)) (hlarge : 24 ≤ Q.distanceMultiplicity Finset.univ 1) (h : SimilarTo P profile.remaining Q.point) : False

theorem LeanPool.Erdos132N14.regular_chord_insertion_multiplicity {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (h : SimilarTo P profile.remaining regularTridecagon.point) (k : Fin 6) : P.insertionMultiplicity profile.deletedVertex profile.remaining (h.similarity.ratio * regularTridecagonChord k) = 2

theorem LeanPool.Erdos132N14.rare_insertion_multiplicity {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) : P.insertionMultiplicity profile.deletedVertex profile.remaining profile.rareDistance = 1

def LeanPool.Erdos132N14.normalizedDeletedPoint {P : Configuration (Fin 14)} {S : Finset (Fin 14)} {template : Fin 13 → ℂ} (h : SimilarTo P S template) (v : Fin 14) : ℂ

The deleted point pulled back through a classified similarity.

Equations

• LeanPool.Erdos132N14.normalizedDeletedPoint h v = h.similarity.toEquiv.symm (P.point v)

theorem LeanPool.Erdos132N14.deleted_distance_eq_scaled {P : Configuration (Fin 14)} {S : Finset (Fin 14)} {template : Fin 13 → ℂ} (h : SimilarTo P S template) (v : Fin 14) (i : Fin 13) : dist (P.point v) (P.point ↑(h.reindex i)) = h.similarity.ratio * dist (normalizedDeletedPoint h v) (template i)

theorem LeanPool.Erdos132N14.normalized_distance_filter_card {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (h : SimilarTo P profile.remaining regularTridecagon.point) (d : ℝ) : {i : Fin 13 | dist (normalizedDeletedPoint h profile.deletedVertex) (regularTridecagon.point i) = d}.card = P.insertionMultiplicity profile.deletedVertex profile.remaining (h.similarity.ratio * d)

structure LeanPool.Erdos132N14.Regular13ExtensionProfile (v : ℂ) : Type

Moment data forced by the internally derived insertion edge counts.

• rareDistance : ℝ

  The rare insertion distance after similarity normalization.

• rareIndex : Fin 13

  The regular vertex joined to the deleted point by the rare edge.

• rareDistance_pos : 0 < self.rareDistance
• rareDistance_sq : Complex.normSq (v - regularTridecagonPoint self.rareIndex) = self.rareDistance ^ 2
• second_sum : ∑ i : Fin 13, Complex.normSq (v - regularTridecagonPoint i) = self.rareDistance ^ 2 + 26
• fourth_sum : ∑ i : Fin 13, Complex.normSq (v - regularTridecagonPoint i) ^ 2 = (self.rareDistance ^ 2) ^ 2 + 78

theorem LeanPool.Erdos132N14.regular13_extension_profile_of_failure {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (h : SimilarTo P profile.remaining regularTridecagon.point) : Nonempty (Regular13ExtensionProfile (normalizedDeletedPoint h profile.deletedVertex))

theorem LeanPool.Erdos132N14.regular13_extension_moment_certificate (r2 D2 ip : ℝ) (hDpos : 0 < D2) (hSecond : 13 * (r2 + 1) = D2 + 26) (hFourth : 13 * (r2 ^ 2 + 4 * r2 + 1) = D2 ^ 2 + 78) (hPair : D2 = r2 + 1 - 2 * ip) (hCauchy : ip ^ 2 ≤ r2) : False

theorem LeanPool.Erdos132N14.regular13_extension_impossible {P : Configuration (Fin 14)} (profile : FourteenFailureExactProfile P) (h : SimilarTo P profile.remaining regularTridecagon.point) : False

theorem LeanPool.Erdos132N14.erdos132_for_fourteen_of_published_inputs (publishedCardinality : PublishedAtMostSixDistanceCardinalityBound) (classification : SzollosiOstergardThirteenPointSixDistanceClassification) (P : Configuration (Fin 14)) : Erdos132ForFourteen P

Conditional end-to-end fourteen-point case of Erdős Problem 132. The two arguments are precisely the remaining named published interfaces; the planar diameter bound, counting, deletion, classified-case elimination, and moment steps are proved internally.