The cyclotomic defect in the opening

This module isolates the characteristic-zero algebra used after compatible finite-field eigenvalues have been lifted to roots of unity. The difficult number-field reduction interface is not assumed here: given three complex unit-circle lifts, we define the symmetric defect, prove its uniform archimedean bound, and prove that it cannot vanish unless all three traces do.

def BGS.Markoff.cyclotomicTrace {K : Type u_1} [Field K] (z : K) : K

The trace associated to a nonzero eigenvalue and its reciprocal.

Equations

• BGS.Markoff.cyclotomicTrace z = z + z⁻¹

def BGS.Markoff.cyclotomicDefect {K : Type u_1} [Field K] (z₁ z₂ z₃ : K) : K

The symmetric Markoff defect of three lifted eigenvalues.

Equations

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

theorem BGS.Markoff.cyclotomicTrace_eq_two_mul_re {z : ℂ} (hz : ‖z‖ = 1) : cyclotomicTrace z = ↑(2 * z.re)

On the complex unit circle, reciprocal-eigenvalue trace is twice the real part.

theorem BGS.Markoff.norm_cyclotomicTrace_le_two {z : ℂ} (hz : ‖z‖ = 1) : ‖cyclotomicTrace z‖ ≤ 2

A unit-circle trace has complex norm at most two.

theorem BGS.Markoff.norm_cyclotomicDefect_le_twenty {z₁ z₂ z₃ : ℂ} (hz₁ : ‖z₁‖ = 1) (hz₂ : ‖z₂‖ = 1) (hz₃ : ‖z₃‖ = 1) : ‖cyclotomicDefect z₁ z₂ z₃‖ ≤ 20

Every complex embedding of the symmetric cyclotomic defect has absolute value at most 20, provided the three eigenvalues lie on the unit circle.

theorem BGS.Markoff.cyclotomicTrace_eq_zero_of_defect_eq_zero {z₁ z₂ z₃ : ℂ} (hz₁ : ‖z₁‖ = 1) (hz₂ : ‖z₂‖ = 1) (hz₃ : ‖z₃‖ = 1) (hdefect : cyclotomicDefect z₁ z₂ z₃ = 0) : cyclotomicTrace z₁ = 0 ∧ cyclotomicTrace z₂ = 0 ∧ cyclotomicTrace z₃ = 0

Three unit-circle lifts with vanishing cyclotomic defect have zero trace in every coordinate.

theorem BGS.Markoff.cyclotomicDefect_ne_zero_of_some_trace_ne_zero {z₁ z₂ z₃ : ℂ} (hz₁ : ‖z₁‖ = 1) (hz₂ : ‖z₂‖ = 1) (hz₃ : ‖z₃‖ = 1) (htrace : cyclotomicTrace z₁ ≠ 0 ∨ cyclotomicTrace z₂ ≠ 0 ∨ cyclotomicTrace z₃ ≠ 0) : cyclotomicDefect z₁ z₂ z₃ ≠ 0

Unless all three reciprocal-eigenvalue traces vanish, the cyclotomic defect is nonzero.