The norm and reduction bridge in the cyclotomic opening

This module connects the already formalized archimedean estimate for the symmetric cyclotomic defect to the arithmetic norm used in the opening argument. It also records the exact ideal theoretic step turning vanishing modulo a prime above p into divisibility of the integer norm by p.

The construction of simultaneous compatible lifts and of the prime ideal realizing their finite-field reduction is deliberately not assumed here. Those are the remaining inputs needed before prime_dvd_integerNorm_of_quotient_eq_zero can be applied to the defect.

theorem BGS.Markoff.algebraNorm_norm_le_pow_of_embeddings {K : Type u_1} [Field K] [NumberField K] (x : K) (B : ℝ) (hB : ∀ (σ : K →+* ℂ), ‖σ x‖ ≤ B) : ‖(Algebra.norm ℚ) x‖ ≤ B ^ Module.finrank ℚ K

If every complex embedding of a number-field element has norm at most B, then its rational field norm has norm at most B to the field degree.

theorem BGS.Markoff.integerNorm_natAbs_le_pow_of_embeddings {K : Type u_1} [Field K] [NumberField K] (x : NumberField.RingOfIntegers K) (B : ℕ) (hB : ∀ (σ : K →+* ℂ), ‖σ ↑x‖ ≤ ↑B) : ((Algebra.norm ℤ) x).natAbs ≤ B ^ Module.finrank ℚ K

Integral version of algebraNorm_norm_le_pow_of_embeddings, with an integer-valued bound.

theorem BGS.Markoff.integerNorm_natAbs_pos {K : Type u_1} [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} (hx : x ≠ 0) : 0 < ((Algebra.norm ℤ) x).natAbs

A nonzero algebraic integer has a nonzero, hence positive-natural-absolute, integer norm.

theorem BGS.Markoff.prime_dvd_integerNorm_of_mem_idealAbove {K : Type u_1} [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) (p : ℕ) (x : NumberField.RingOfIntegers K) (hP : Ideal.under ℤ P = Ideal.span {↑p}) (hx : x ∈ P) : ↑p ∣ (Algebra.norm ℤ) x

If an algebraic integer lies in an ideal above the rational ideal (p), then p divides its integer norm. Primality is not needed for this algebraic implication; it is needed when the ideal above p is constructed.

theorem BGS.Markoff.prime_dvd_integerNorm_of_quotient_eq_zero {K : Type u_1} [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) (p : ℕ) (x : NumberField.RingOfIntegers K) (hP : Ideal.under ℤ P = Ideal.span {↑p}) (hx : (Ideal.Quotient.mk P) x = 0) : ↑p ∣ (Algebra.norm ℤ) x

Quotient-map form of prime_dvd_integerNorm_of_mem_idealAbove, matching the reduction step in the paper: reduction of x to zero modulo a prime above p forces p ∣ N(x).

theorem BGS.Markoff.modulus_le_integerNorm_natAbs_of_quotient_eq_zero {K : Type u_1} [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) (p : ℕ) (x : NumberField.RingOfIntegers K) (hP : Ideal.under ℤ P = Ideal.span {↑p}) (hx : (Ideal.Quotient.mk P) x = 0) (hxne : x ≠ 0) : p ≤ ((Algebra.norm ℤ) x).natAbs

If a nonzero algebraic integer reduces to zero modulo an ideal above (p), then p is at most the natural absolute value of its integer norm.

theorem BGS.Markoff.isIntegral_cyclotomicTrace {K : Type u_1} [Field K] {z : K} (hz : IsIntegral ℤ z) (hzinv : IsIntegral ℤ z⁻¹) : IsIntegral ℤ (cyclotomicTrace z)

Reciprocal trace preserves integrality when both the eigenvalue and its inverse are integral.

theorem BGS.Markoff.isIntegral_cyclotomicDefect {K : Type u_1} [Field K] {z₁ z₂ z₃ : K} (hz₁ : IsIntegral ℤ z₁) (hz₁inv : IsIntegral ℤ z₁⁻¹) (hz₂ : IsIntegral ℤ z₂) (hz₂inv : IsIntegral ℤ z₂⁻¹) (hz₃ : IsIntegral ℤ z₃) (hz₃inv : IsIntegral ℤ z₃⁻¹) : IsIntegral ℤ (cyclotomicDefect z₁ z₂ z₃)

The symmetric defect is integral when the three reciprocal traces are integral.

theorem BGS.Markoff.isIntegral_cyclotomicDefect_of_primitiveRoots {K : Type u_1} [Field K] {z₁ z₂ z₃ : K} {l₁ l₂ l₃ : ℕ} (hz₁ : IsPrimitiveRoot z₁ l₁) (hl₁ : 0 < l₁) (hz₂ : IsPrimitiveRoot z₂ l₂) (hl₂ : 0 < l₂) (hz₃ : IsPrimitiveRoot z₃ l₃) (hl₃ : 0 < l₃) : IsIntegral ℤ (cyclotomicDefect z₁ z₂ z₃)

The cyclotomic defect of three primitive roots of positive orders is an algebraic integer.

theorem BGS.Markoff.cyclotomicDefect_integerNorm_natAbs_le_twenty_pow_totient {K : Type u_1} [Field K] [NumberField K] {n l₁ l₂ l₃ : ℕ} [NeZero n] [IsCyclotomicExtension {n} ℚ K] {z₁ z₂ z₃ : K} (hz₁ : IsPrimitiveRoot z₁ l₁) (hl₁ : 0 < l₁) (hz₂ : IsPrimitiveRoot z₂ l₂) (hl₂ : 0 < l₂) (hz₃ : IsPrimitiveRoot z₃ l₃) (hl₃ : 0 < l₃) : have η := ⟨cyclotomicDefect z₁ z₂ z₃, ⋯⟩; ((Algebra.norm ℤ) η).natAbs ≤ 20 ^ n.totient

The exact archimedean norm conclusion needed in the opening: the integer norm of a cyclotomic defect is bounded by 20 ^ φ(n).

theorem BGS.Markoff.cyclotomicDefect_integerNorm_natAbs_pos {K : Type u_1} [Field K] [NumberField K] {z₁ z₂ z₃ : K} {l₁ l₂ l₃ : ℕ} (hz₁ : IsPrimitiveRoot z₁ l₁) (hl₁ : 0 < l₁) (hz₂ : IsPrimitiveRoot z₂ l₂) (hl₂ : 0 < l₂) (hz₃ : IsPrimitiveRoot z₃ l₃) (hl₃ : 0 < l₃) (hη : cyclotomicDefect z₁ z₂ z₃ ≠ 0) : have η := ⟨cyclotomicDefect z₁ z₂ z₃, ⋯⟩; 0 < ((Algebra.norm ℤ) η).natAbs

A nonzero cyclotomic defect has positive natural absolute integer norm.

theorem BGS.Markoff.modulus_le_twenty_pow_totient_of_cyclotomicDefect_reduction {K : Type u_1} [Field K] [NumberField K] {n l₁ l₂ l₃ : ℕ} [NeZero n] [IsCyclotomicExtension {n} ℚ K] {z₁ z₂ z₃ : K} (hz₁ : IsPrimitiveRoot z₁ l₁) (hl₁ : 0 < l₁) (hz₂ : IsPrimitiveRoot z₂ l₂) (hl₂ : 0 < l₂) (hz₃ : IsPrimitiveRoot z₃ l₃) (hl₃ : 0 < l₃) (P : Ideal (NumberField.RingOfIntegers K)) (p : ℕ) (hP : Ideal.under ℤ P = Ideal.span {↑p}) (hη : cyclotomicDefect z₁ z₂ z₃ ≠ 0) (hred : have η := ⟨cyclotomicDefect z₁ z₂ z₃, ⋯⟩; (Ideal.Quotient.mk P) η = 0) : p ≤ 20 ^ n.totient

The completed norm-and-reduction implication: if the nonzero cyclotomic defect reduces to zero at an ideal above (p), then p ≤ 20 ^ φ(n). Constructing the compatible reduction data is the remaining opening problem, not an assumption hidden in this theorem.