The three classified thirteen-point templates

The regular tridecagon is constructed from the canonical primitive thirteenth root of unity. Its centroid, second harmonic, isotropy, chord classes, and distance moments are derived from those coordinates. The centered dodecagon and centered regular hexagram are also given by explicit complex coordinates; their high-multiplicity classes are checked inside Lean.

noncomputable def LeanPool.Erdos132N14.regularThirteenRoot : ℂ

The canonical primitive thirteenth root of unity.

Equations

• LeanPool.Erdos132N14.regularThirteenRoot = Complex.exp (2 * ↑Real.pi * Complex.I / 13)

theorem LeanPool.Erdos132N14.regularThirteenRoot_isPrimitive : IsPrimitiveRoot regularThirteenRoot 13

theorem LeanPool.Erdos132N14.norm_regularThirteenRoot : ‖regularThirteenRoot‖ = 1

noncomputable def LeanPool.Erdos132N14.regularTridecagonPoint (i : Fin 13) : ℂ

Unit-circumradius regular-tridecagon coordinates.

Equations

• LeanPool.Erdos132N14.regularTridecagonPoint i = LeanPool.Erdos132N14.regularThirteenRoot ^ ↑i

theorem LeanPool.Erdos132N14.regularTridecagonPoint_injective : Function.Injective regularTridecagonPoint

noncomputable def LeanPool.Erdos132N14.regularTridecagon : Configuration (Fin 13)

The regular tridecagon as a labelled planar configuration.

Equations

• LeanPool.Erdos132N14.regularTridecagon = { point := LeanPool.Erdos132N14.regularTridecagonPoint, injective := LeanPool.Erdos132N14.regularTridecagonPoint_injective }

theorem LeanPool.Erdos132N14.norm_regularTridecagonPoint (i : Fin 13) : ‖regularTridecagonPoint i‖ = 1

theorem LeanPool.Erdos132N14.normSq_regularTridecagonPoint (i : Fin 13) : Complex.normSq (regularTridecagonPoint i) = 1

theorem LeanPool.Erdos132N14.sum_regularTridecagonPoint : ∑ i : Fin 13, regularTridecagonPoint i = 0

The regular tridecagon is centered at the origin.

theorem LeanPool.Erdos132N14.sum_regularTridecagonPoint_sq : ∑ i : Fin 13, regularTridecagonPoint i ^ 2 = 0

Its second complex harmonic also vanishes.

def LeanPool.Erdos132N14.planeDot (x y : ℂ) : ℝ

The real Euclidean scalar product on complex coordinates.

Equations

• LeanPool.Erdos132N14.planeDot x y = x.re * y.re + x.im * y.im

theorem LeanPool.Erdos132N14.normSq_sub (x y : ℂ) : Complex.normSq (x - y) = Complex.normSq x + Complex.normSq y - 2 * planeDot x y

theorem LeanPool.Erdos132N14.regularTridecagon_isotropy (v : ℂ) : ∑ i : Fin 13, planeDot v (regularTridecagonPoint i) ^ 2 = 13 / 2 * Complex.normSq v

The regular tridecagon is a unit tight frame with frame constant 13 / 2.

theorem LeanPool.Erdos132N14.regularTridecagon_second_moment (v : ℂ) : ∑ i : Fin 13, Complex.normSq (v - regularTridecagonPoint i) = 13 * (Complex.normSq v + 1)

Sum of squared distances from an arbitrary point to the unit tridecagon.

theorem LeanPool.Erdos132N14.regularTridecagon_fourth_moment (v : ℂ) : ∑ i : Fin 13, Complex.normSq (v - regularTridecagonPoint i) ^ 2 = 13 * (Complex.normSq v ^ 2 + 4 * Complex.normSq v + 1)

Sum of fourth powers of distances from an arbitrary point to the tridecagon.

theorem LeanPool.Erdos132N14.normSq_regularThirteenRoot_pow (n : ℕ) : Complex.normSq (regularThirteenRoot ^ n) = 1

noncomputable def LeanPool.Erdos132N14.regularTridecagonChord (k : Fin 6) : ℝ

The six chord lengths, indexed by cyclic gaps 1, ..., 6.

Equations

• LeanPool.Erdos132N14.regularTridecagonChord k = dist 1 (LeanPool.Erdos132N14.regularThirteenRoot ^ (↑k + 1))

theorem LeanPool.Erdos132N14.regularTridecagonChord_injective : Function.Injective regularTridecagonChord

theorem LeanPool.Erdos132N14.normSq_one_root_pow_eq_of_sum_eq_thirteen {a b : ℕ} (hsum : a + b = 13) : Complex.normSq (1 - regularThirteenRoot ^ a) = Complex.normSq (1 - regularThirteenRoot ^ b)

theorem LeanPool.Erdos132N14.regularTridecagon_chord_second_sum : 2 * ∑ k : Fin 6, regularTridecagonChord k ^ 2 = 26

Twice the sum of the six squared chord lengths.

theorem LeanPool.Erdos132N14.regularTridecagon_chord_fourth_sum : 2 * ∑ k : Fin 6, (regularTridecagonChord k ^ 2) ^ 2 = 78

Twice the sum of the squares of the six squared chord lengths.

theorem LeanPool.Erdos132N14.regularTridecagon_chord_multiplicity (k : Fin 6) : regularTridecagon.distanceMultiplicity Finset.univ (regularTridecagonChord k) = 13

Every one of the six regular-tridecagon chord lengths occurs on exactly thirteen unordered vertex pairs.

noncomputable def LeanPool.Erdos132N14.dodecagonWithCenterPoint (i : Fin 13) : ℂ

Explicit coordinates for the regular dodecagon and its center.

Equations

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

theorem LeanPool.Erdos132N14.dodecagonWithCenterPoint_injective : Function.Injective dodecagonWithCenterPoint

noncomputable def LeanPool.Erdos132N14.dodecagonWithCenter : Configuration (Fin 13)

The centered regular dodecagon template in the published classification.

Equations

• LeanPool.Erdos132N14.dodecagonWithCenter = { point := LeanPool.Erdos132N14.dodecagonWithCenterPoint, injective := LeanPool.Erdos132N14.dodecagonWithCenterPoint_injective }

noncomputable def LeanPool.Erdos132N14.hexagramWithCenterPoint (i : Fin 13) : ℂ

Explicit coordinates for the twelve vertices of a regular hexagram and its center. The outer radius is √3 and the inner radius is 1.

Equations

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

theorem LeanPool.Erdos132N14.hexagramWithCenterPoint_injective : Function.Injective hexagramWithCenterPoint

noncomputable def LeanPool.Erdos132N14.hexagramWithCenter : Configuration (Fin 13)

The centered regular-hexagram template in the published classification.

Equations

• LeanPool.Erdos132N14.hexagramWithCenter = { point := LeanPool.Erdos132N14.hexagramWithCenterPoint, injective := LeanPool.Erdos132N14.hexagramWithCenterPoint_injective }

theorem LeanPool.Erdos132N14.dodecagonWithCenter_unit_distance_multiplicity : dodecagonWithCenter.distanceMultiplicity Finset.univ 1 = 24

The centered dodecagon has exactly twenty-four unit-distance pairs.

def LeanPool.Erdos132N14.hexagramUnitPair (k : Fin 24) : Fin 13 × Fin 13

Enumeration of twenty-four unit pairs in the centered hexagram.

Equations

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

theorem LeanPool.Erdos132N14.hexagramUnitPair_injective : Function.Injective hexagramUnitPair

theorem LeanPool.Erdos132N14.hexagramUnitPair_mem_pairs (k : Fin 24) : hexagramUnitPair k ∈ pairs Finset.univ

theorem LeanPool.Erdos132N14.hexagramUnitPair_distance (k : Fin 24) : hexagramWithCenter.pairDistance (hexagramUnitPair k) = 1

theorem LeanPool.Erdos132N14.hexagramWithCenter_unit_distance_multiplicity : 24 ≤ hexagramWithCenter.distanceMultiplicity Finset.univ 1

The centered hexagram has at least twenty-four unit-distance pairs.