/- Copyright (c) 2026 LANA Project. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: LANA Project -/ import Iut.Tower.Residual /-! # The ramification bound (R4) of IUT IV, Theorem 1.10 * `Iut.finrank_torsionField_le`: `[K : F] ≀ |GLβ‚‚(𝔽_β„“)| = (β„“Β² βˆ’ 1)(β„“Β² βˆ’ β„“)`, from the Galois correspondence: `K` is the fixed field of the (open, hence closed) kernel of the mod-`β„“` representation, so `[K : F]` is the index of the kernel, the order of the image. * `Iut.ramIdx_bound_of_facts`, **(R4)**: for a finite place `v` of `K` with `e_v > p_v βˆ’ 2`, `p_v ≀ 552960Β·d_modΒ·β„“` and `log e_v ≀ βˆ’3 + 4Β·log(552960Β·d_modΒ·β„“)`. Away from `2Β·3Β·5Β·β„“`, `e_v = e_uΒ·e(v/u) ≀ [F_tpd : β„š]Β·30β„“ ≀ 180Β·d_modΒ·β„“` (the ramification bound of `TowerLocalFacts`, `[F_tpd : F_mod] ≀ 6`); at `p ∈ {2, 3, 5, β„“}` the first bound is trivial. The second uses only `e_v ≀ [K : β„š] ≀ |GLβ‚‚(𝔽_β„“)|Β·[F : β„š]` and `[F : β„š] ≀ 552960Β·[F_tpd : β„š] ≀ 552960Β·6Β·d_mod`. -/ namespace Iut open NumberField IsDedekindDomain universe u section Degree variable {F : Type u} [Field F] [NumberField F] {E : WeierstrassCurve F} [E.IsElliptic] variable {Fbar : Type u} [Field Fbar] [Algebra F Fbar] [IsAlgClosure F Fbar] variable {VBad : Set (FinitePlace β†₯(fieldOfModuli F E))} variable (Pr : AdmissiblePrimeData F E Fbar VBad) /-- `|GLβ‚‚(𝔽_β„“)| = (β„“Β² βˆ’ 1)(β„“Β² βˆ’ β„“)` for `β„“` prime. -/ lemma card_GL_two_of_prime (β„“ : β„•) (hβ„“ : β„“.Prime) : Nat.card (Matrix.GeneralLinearGroup (Fin 2) (ZMod β„“)) = (β„“ ^ 2 - 1) * (β„“ ^ 2 - β„“) := by haveI : Fact β„“.Prime := ⟨hβ„“βŸ© rw [Matrix.card_GL_field, Fin.prod_univ_two, ZMod.card] simp /-- **`[K : F] ≀ |GLβ‚‚(𝔽_β„“)|`**: the torsion field is the fixed field of the kernel of the mod-`β„“` representation, whose index is the order of the image. -/ theorem finrank_torsionField_le : Module.finrank F β†₯Pr.torsionField ≀ (Pr.β„“ ^ 2 - 1) * (Pr.β„“ ^ 2 - Pr.β„“) := by let H : ClosedSubgroup (Fbar ≃ₐ[F] Fbar) := ⟨Pr.rep.ker, Subgroup.isClosed_of_isOpen _ Pr.ker_isOpen⟩ have h1 : Module.finrank F β†₯Pr.torsionField = Pr.rep.ker.index := by rw [IntermediateField.finrank_eq_fixingSubgroup_index] change (IntermediateField.fixedField H.1).fixingSubgroup.index = H.1.index rw [InfiniteGalois.fixingSubgroup_fixedField H] haveI : NeZero Pr.β„“ := ⟨Pr.β„“_prime.ne_zero⟩ rw [h1, Subgroup.index_ker, ← card_GL_two_of_prime Pr.β„“ Pr.β„“_prime] exact Nat.card_le_card_of_injective _ Subtype.val_injective /-- `(β„“Β² βˆ’ 1)(β„“Β² βˆ’ β„“) ≀ ℓ⁴`. -/ lemma card_GL_two_le (β„“ : β„•) : (β„“ ^ 2 - 1) * (β„“ ^ 2 - β„“) ≀ β„“ ^ 4 := by calc (β„“ ^ 2 - 1) * (β„“ ^ 2 - β„“) ≀ β„“ ^ 2 * β„“ ^ 2 := Nat.mul_le_mul (Nat.sub_le _ _) (Nat.sub_le _ _) _ = β„“ ^ 4 := by ring end Degree /-! ### (R4) -/ section R4 variable {F : Type u} [Field F] [NumberField F] {E : WeierstrassCurve F} [E.IsElliptic] variable {Fbar : Type u} [Field Fbar] [Algebra F Fbar] [IsAlgClosure F Fbar] variable {VBad : Set (FinitePlace β†₯(fieldOfModuli F E))} variable {Pr : AdmissiblePrimeData F E Fbar VBad} [NumberField β†₯Pr.torsionField] /-- `2 ≀ log 552960`. -/ lemma two_le_log_552960 : (2 : ℝ) ≀ Real.log 552960 := by rw [Real.le_log_iff_exp_le (by norm_num)] have h := Real.exp_one_lt_d9 have h2 : Real.exp 2 = Real.exp 1 * Real.exp 1 := by rw [← Real.exp_add]; norm_num rw [h2] have h0 : 0 < Real.exp 1 := Real.exp_pos 1 nlinarith /-- `log 6 ≀ 2`. -/ lemma log_six_le_two : Real.log 6 ≀ 2 := by rw [Real.log_le_iff_le_exp (by norm_num)] have h := Real.exp_one_gt_d9 have h2 : Real.exp 2 = Real.exp 1 * Real.exp 1 := by rw [← Real.exp_add]; norm_num rw [h2] nlinarith /-- **(R4)** from the local facts and the degree bounds `[F_tpd : F_mod] ≀ 6`, `[F : β„š] ≀ 552960Β·[F_tpd : β„š]`. -/ theorem ramIdx_bound_of_facts (H : TowerLocalFacts E VBad Pr) (h6 : Module.finrank β†₯(fieldOfModuli F E) β†₯(tripodalFieldOf F E) ≀ 6) (hF : Module.finrank β„š F ≀ 552960 * Module.finrank β„š β†₯(tripodalFieldOf F E)) (v : FinitePlace β†₯Pr.torsionField) (hv : residueChar v - 2 < ramIdx (β†₯Pr.torsionField) v) : residueChar v ≀ 552960 * Module.finrank β„š β†₯(fieldOfModuli F E) * Pr.β„“ ∧ Real.log (ramIdx (β†₯Pr.torsionField) v) ≀ -3 + 4 * Real.log (((552960 * Module.finrank β„š β†₯(fieldOfModuli F E) : β„•) : ℝ) * Pr.β„“) := by set d := Module.finrank β„š β†₯(fieldOfModuli F E) with hd set β„“ := Pr.β„“ with hβ„“ have hd1 : 1 ≀ d := Module.finrank_pos have hβ„“5 : 5 ≀ β„“ := Pr.five_le have hT : Module.finrank β„š β†₯(tripodalFieldOf F E) ≀ 6 * d := by rw [finrank_tripodal_eq_mul F E] calc d * Module.finrank β†₯(fieldOfModuli F E) β†₯(tripodalFieldOf F E) ≀ d * 6 := Nat.mul_le_mul_left _ h6 _ = 6 * d := mul_comm _ _ constructor Β· by_cases hp : residueChar v ∈ ({2, 3, 5, β„“} : Finset β„•) Β· have : residueChar v ≀ β„“ := by simp only [Finset.mem_insert, Finset.mem_singleton] at hp omega calc residueChar v ≀ β„“ := this _ ≀ 552960 * d * β„“ := Nat.le_mul_of_pos_left _ (by positivity) Β· have h1 := H.relRamIdx_le v hp have h2 := ramIdx_eq_ramIdx_placeTpd_mul (F := F) (E := E) v have h3 := ramIdx_le_finrank (placeTpd F E Pr.torsionField v) have h4 : ramIdx (β†₯Pr.torsionField) v ≀ 6 * d * (30 * β„“) := by rw [h2] exact Nat.mul_le_mul (h3.trans hT) h1 have h5 : residueChar v < ramIdx (β†₯Pr.torsionField) v + 2 := by omega nlinarith Β· have hK : Module.finrank β„š β†₯Pr.torsionField ≀ β„“ ^ 4 * (552960 * (6 * d)) := by rw [← Module.finrank_mul_finrank β„š F β†₯Pr.torsionField] calc Module.finrank β„š F * Module.finrank F β†₯Pr.torsionField ≀ (552960 * (6 * d)) * β„“ ^ 4 := Nat.mul_le_mul (hF.trans (Nat.mul_le_mul_left _ hT)) ((finrank_torsionField_le Pr).trans (card_GL_two_le β„“)) _ = β„“ ^ 4 * (552960 * (6 * d)) := mul_comm _ _ have he : ramIdx (β†₯Pr.torsionField) v ≀ β„“ ^ 4 * (552960 * (6 * d)) := (ramIdx_le_finrank v).trans hK have hepos : (0 : ℝ) < ramIdx (β†₯Pr.torsionField) v := by exact_mod_cast ramIdx_pos' v have hβ„“pos : (0 : ℝ) < β„“ := by exact_mod_cast (by omega : 0 < β„“) have hdpos : (0 : ℝ) < d := by exact_mod_cast hd1 have hlog1 : Real.log (ramIdx (β†₯Pr.torsionField) v) ≀ 4 * Real.log β„“ + (Real.log 6 + Real.log (552960 * d)) := by calc Real.log (ramIdx (β†₯Pr.torsionField) v) ≀ Real.log ((β„“ : ℝ) ^ 4 * (552960 * (6 * d))) := by apply Real.log_le_log hepos exact_mod_cast he _ = 4 * Real.log β„“ + (Real.log 6 + Real.log (552960 * d)) := by rw [Real.log_mul (by positivity) (by positivity), Real.log_pow, show (552960 * (6 * d) : ℝ) = 6 * (552960 * d) by ring, Real.log_mul (by norm_num) (by positivity)] push_cast ring have hlog2 : (2 : ℝ) ≀ Real.log (552960 * d) := by refine two_le_log_552960.trans (Real.log_le_log (by norm_num) ?_) have : (1 : ℝ) ≀ d := by exact_mod_cast hd1 nlinarith have hlog3 := log_six_le_two have hsplit : Real.log (((552960 * d : β„•) : ℝ) * β„“) = Real.log (552960 * d) + Real.log β„“ := by rw [Real.log_mul (by positivity) (by positivity)] push_cast ring rw [hsplit] linarith end R4 end Iut