/-
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.Concrete.ThetaRegion
import Iut.Implication.Theorem110

/-!
# Concrete arithmetic invariants of Theorem 1.10 (taxis #1453)

For the concrete variant data `concreteVariantData D`, the invariants of
`Theorem110Invariants` that live on the `ℓ`-torsion field `K` are defined here from the
local theory:

* the **distinguished primes** `V_ℚ^dst`: the primes dividing `2·3·5·ℓ`, the residue
  characteristics of the bad places, and the primes ramified in `K` (conditions (D6)/(D7)
  in the proof of Theorem 1.10, taken as the definition);
* the **local different contributions** `log(d^K_p) = ∑_{v ∣ p} w_v·d_v·log p`, from the
  different exponents `d_v = ord_𝔭(𝔡_{K/ℚ})/e_v` (`Iut.differentExponent`) and the weights
  `w_v = [K_v : ℚ_p]/[K : ℚ]`, the sum running over all places of `K` over `p` (so that
  `∑_p log(d^K_p) = log(d_K)`, `Iut.InitialThetaData.sum_dst_logDK_eq`). It equals the average
  over the places of the section `V ≅ V_mod` with the weights of IUT III, Remark 3.1.1(ii), that
  enters the log-volume estimates (`Iut.InitialThetaData.logDK_sect`, `K/F_mod` Galois).

The tripodal field `F_tpd = F_mod(E[2])` is defined as the subfield of `F` generated by
`j(E)` and the `x`-coordinates of the `2`-torsion, and `log(d_{F_tpd})`, `log(f_{F_tpd})` as
the normalized degrees of its different and conductor; `e_mod` is replaced by `d_mod`. The
three facts of the tower's arithmetic that Theorem 1.10 consumes — the ramification bound
(R4) and the inequalities of Steps (ii), (iii) — form the `Prop`-structure
`TowerArithmetic`, a standard-mathematics target (IUT IV, Propositions 1.3 and 1.8).

The file also proves the weighted-average identities of IUT IV, Proposition 1.7 in the
form used by Step (v): for weights summing to `1`, the weighted sum over tuples of a
quantity depending on one coordinate is the weighted sum over places.
-/

namespace Iut

universe u

open NumberField
open scoped Pointwise

/-! ### Weighted averages over tuples (IUT IV, Proposition 1.7) -/

section Average

variable {ι E : Type*} [Fintype ι] [Fintype E] [DecidableEq ι] (w : E → ℝ)

/-- The tuple weights sum to `(∑ w)^{|ι|}`. -/
lemma sum_prod_tuple : ∑ c : ι → E, ∏ i, w (c i) = (∑ e, w e) ^ Fintype.card ι := by
  rw [← Fintype.prod_sum (fun _ : ι => w)]
  simp

/-- Proposition 1.7, one coordinate: `∑_c (∏_i w(c i))·f(c i₀) = (∑_e w e f e)·(∑ w)^{|ι|−1}`;
with `∑ w = 1` the right-hand side is `∑_e w e f e`. -/
lemma sum_prod_tuple_mul_coord (hw : ∑ e, w e = 1) (f : E → ℝ) (i₀ : ι) :
    ∑ c : ι → E, (∏ i, w (c i)) * f (c i₀) = ∑ e, w e * f e := by
  let g : ι → E → ℝ := fun i e => if i = i₀ then w e * f e else w e
  have hg : ∀ c : ι → E, (∏ i, w (c i)) * f (c i₀) = ∏ i, g i (c i) := by
    intro c
    rw [← Finset.mul_prod_erase Finset.univ (fun i => g i (c i)) (Finset.mem_univ i₀),
      ← Finset.mul_prod_erase Finset.univ (fun i => w (c i)) (Finset.mem_univ i₀)]
    have : ∏ i ∈ Finset.univ.erase i₀, g i (c i) = ∏ i ∈ Finset.univ.erase i₀, w (c i) :=
      Finset.prod_congr rfl fun i hi => by simp [g, (Finset.mem_erase.mp hi).1]
    rw [this]
    simp only [g, if_true]
    ring
  simp_rw [hg]
  rw [← Fintype.prod_sum g,
    ← Finset.mul_prod_erase Finset.univ (fun i => ∑ e, g i e) (Finset.mem_univ i₀)]
  have : ∏ i ∈ Finset.univ.erase i₀, ∑ e, g i e = 1 := by
    refine Finset.prod_eq_one fun i hi => ?_
    simp [g, (Finset.mem_erase.mp hi).1, hw]
  rw [this, mul_one]
  simp [g]

/-- Proposition 1.7, summed over the coordinates:
`∑_c (∏_i w(c i))·∑_i f(c i) = |ι|·∑_e w e f e`. -/
lemma sum_prod_tuple_mul_sum (hw : ∑ e, w e = 1) (f : E → ℝ) :
    ∑ c : ι → E, (∏ i, w (c i)) * ∑ i, f (c i) = Fintype.card ι * ∑ e, w e * f e := by
  simp_rw [Finset.mul_sum]
  rw [Finset.sum_comm]
  simp_rw [sum_prod_tuple_mul_coord w hw f]
  rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, Finset.mul_sum]

omit [DecidableEq ι] in
/-- The tuple weights sum to `1` when the weights do (for any `Fintype` instance on the
tuples). -/
lemma sum_prod_tuple_eq_one (hw : ∑ e, w e = 1) [inst : Fintype (ι → E)] :
    ∑ c : ι → E, ∏ i, w (c i) = 1 := by
  classical
  rw [Subsingleton.elim inst Pi.instFintype]
  clear inst
  rw [sum_prod_tuple, hw, one_pow]

end Average

/-! ### The concrete invariants -/

namespace InitialThetaData

variable (D : InitialThetaData.{u})

/-- The residue characteristics of the primes ramified in `K`, as a finite set. -/
noncomputable def ramifiedChars : Finset ℕ :=
  ((LocalTheory.ramified_finite D.Kt).toFinset).image residueChar

/-- `log(d^K_p) = ∑_{v ∣ p} w_v·d_v·log p` (the contribution of `p` to the normalized
degree of the different of `K`), and `0` at non-primes. -/
noncomputable def logDK (p : ℕ) : ℝ :=
  if hp : p.Prime then
    ∑ v : LocalTheory.Fiber D.Kt (.finite ⟨p, hp⟩),
      LocalTheory.weight D.Kt _ v * differentExponent D.Kt (LocalTheory.fiberPlace D.Kt v)
          * Real.log p
  else 0

lemma differentExponent_nonneg (w : FinitePlace D.Kt) : 0 ≤ differentExponent D.Kt w :=
  div_nonneg (by positivity) (by positivity)

lemma logDK_nonneg (p : ℕ) : 0 ≤ D.logDK p := by
  unfold InitialThetaData.logDK
  split_ifs with hp
  · exact Finset.sum_nonneg fun v _ => mul_nonneg
      (mul_nonneg (LocalTheory.weight_pos D.Kt _ v).le (D.differentExponent_nonneg _))
      (Real.log_nonneg (by exact_mod_cast hp.one_lt.le))
  · exact le_rfl


/-- **The distinguished primes** `V_ℚ^dst`: `2, 3, 5, ℓ`, the bad residue characteristics,
and the primes ramified in `K` ((D6)/(D7), as the definition). -/
noncomputable def dst : Finset ℕ :=
  {2, 3, 5, D.ℓ} ∪ D.badChars ∪ D.ramifiedChars

lemma dst_prime (p : ℕ) (hp : p ∈ D.dst) : p.Prime := by
  simp only [dst, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton,
    InitialThetaData.ramifiedChars, Finset.mem_image, Set.Finite.mem_toFinset] at hp
  rcases hp with ((rfl | rfl | rfl | rfl) | hb) | ⟨w, _, rfl⟩
  · exact Nat.prime_two
  · exact Nat.prime_three
  · exact Nat.prime_five
  · exact D.prime.ℓ_prime
  · exact D.badChars_prime _ hb
  · exact LocalTheory.residueChar_prime D.Kt w

lemma mem_dst_of_ramified (w : FinitePlace D.Kt) (hw : ramIdx D.Kt w ≠ 1) :
    residueChar w ∈ D.dst := by
  refine Finset.mem_union_right _ ?_
  simp only [InitialThetaData.ramifiedChars, Finset.mem_image, Set.Finite.mem_toFinset]
  exact ⟨w, hw, rfl⟩

lemma mem_dst_of_badChars (p : ℕ) (hp : p ∈ D.badChars) : p ∈ D.dst :=
  Finset.mem_union_left _ (Finset.mem_union_right _ hp)

lemma two_mem_dst : 2 ∈ D.dst := by
  refine Finset.mem_union_left _ (Finset.mem_union_left _ ?_)
  simp

lemma logDK_eq_zero (p : ℕ) (hp : p ∉ D.dst) : D.logDK p = 0 := by
  unfold InitialThetaData.logDK
  split_ifs with hpp
  · refine Finset.sum_eq_zero fun v _ => ?_
    have hunr : ramIdx D.Kt (LocalTheory.fiberPlace D.Kt v) = 1 := by
      by_contra hne
      apply hp
      have := D.mem_dst_of_ramified _ hne
      rwa [LocalTheory.residueChar_fiberPlace D.Kt] at this
    simp [differentExponent, LocalTheory.ordDifferent_eq_zero D.Kt _ hunr]
  · rfl

end InitialThetaData

/-! ### The tripodal field and its different and conductor degrees -/

/-- The normalized degree `log(d_L) = log N(𝔡_{L/ℚ})/[L : ℚ]` of the different divisor of a
number field `L` (IUT IV, Theorem 1.10: `deg(d_ADiv)`). -/
noncomputable def logDifferentDeg (L : Type*) [Field L] [NumberField L] : ℝ :=
  Real.log (Ideal.absNorm (differentIdeal ℤ (𝓞 L))) / Module.finrank ℚ L

lemma logDifferentDeg_nonneg (L : Type*) [Field L] [NumberField L] :
    0 ≤ logDifferentDeg L := by
  apply div_nonneg _ (by positivity)
  apply Real.log_nonneg
  have h : Ideal.absNorm (differentIdeal ℤ (𝓞 L)) ≠ 0 := by
    rw [Ne, Ideal.absNorm_eq_zero_iff]
    exact differentIdeal_ne_bot
  exact_mod_cast Nat.one_le_iff_ne_zero.mpr h

section Tripodal

variable (F : Type*) [Field F] [NumberField F] (E : WeierstrassCurve F) [E.IsElliptic]

open scoped Classical in
/-- The `x`-coordinates of the `F`-rational `2`-torsion points of `E`. -/
def twoTorsionXOf : Set F :=
  {a | ∃ (b : F) (h : E.toAffine.Nonsingular a b),
    WeierstrassCurve.Affine.Point.some a b h ∈ AddSubgroup.torsionBy E.toAffine.Point 2}

/-- **The tripodal field** `F_tpd = F_mod(E[2])` (IUT IV, Theorem 1.10; Proposition
1.8(ii),(iii)): the subfield of `F` generated over `ℚ` by `j(E)` and the `x`-coordinates
of the `2`-torsion points (rational over `F` by IUT I, Definition 3.1(b)). -/
noncomputable def tripodalFieldOf : IntermediateField ℚ F :=
  IntermediateField.adjoin ℚ (insert E.j (twoTorsionXOf F E))

instance : FiniteDimensional ℚ ↥(tripodalFieldOf F E) :=
  Module.Finite.left ℚ ↥(tripodalFieldOf F E) F

instance : NumberField ↥(tripodalFieldOf F E) where

variable (VBad : Set (FinitePlace ↥(fieldOfModuli F E)))

/-- A finite place of `F_tpd` is **bad** if a bad place of `F` lies over it. -/
def IsBadTpdOf (𝔭 : FinitePlace ↥(tripodalFieldOf F E)) : Prop :=
  ∃ w ∈ badPlacesOver F E VBad, (Place.finite w).LiesOver (Place.finite 𝔭)

open scoped Classical in
/-- The normalized degree `log(f_{F_tpd})` of the **conductor divisor** of `F_tpd`: the
sum of `log N(𝔭)` over the bad places of `F_tpd`, divided by `[F_tpd : ℚ]` (finitely
supported; `0` if not). -/
noncomputable def logConductorDegOf : ℝ :=
  (∑ᶠ 𝔭 : FinitePlace ↥(tripodalFieldOf F E),
    if IsBadTpdOf F E VBad 𝔭 then Real.log (Ideal.absNorm 𝔭.maximalIdeal.asIdeal) else 0) /
    Module.finrank ℚ ↥(tripodalFieldOf F E)

lemma logConductorDegOf_nonneg : 0 ≤ logConductorDegOf F E VBad := by
  apply div_nonneg _ (by positivity)
  apply finsum_nonneg
  intro 𝔭
  split_ifs
  · exact Real.log_nonneg
      (by exact_mod_cast (NumberField.HeightOneSpectrum.one_lt_absNorm 𝔭.maximalIdeal).le)
  · exact le_rfl

end Tripodal

namespace InitialThetaData

variable (D : InitialThetaData.{u})

/-- `d_mod = [F_mod : ℚ]`. -/
noncomputable abbrev dmod : ℕ := Module.finrank ℚ ↥(fieldOfModuli D.F D.E)

lemma one_le_dmod : 1 ≤ D.dmod := Module.finrank_pos

/-- The tripodal field `F_tpd` of the Θ-data (`Iut.tripodalFieldOf`). -/
noncomputable abbrev tripodalField : IntermediateField ℚ D.F := tripodalFieldOf D.F D.E

/-- The conductor invariant `log(f_{F_tpd})` of the Θ-data (`Iut.logConductorDegOf`). -/
noncomputable abbrev logConductorDeg : ℝ := logConductorDegOf D.F D.E D.VBad

lemma logConductorDeg_nonneg : 0 ≤ D.logConductorDeg := logConductorDegOf_nonneg _ _ _

end InitialThetaData

variable (D : InitialThetaData.{u})

/-- **The concrete invariants of Theorem 1.10** for the concrete variant data, with
`e_mod := d_mod` (Theorem 1.10 holds with `e_mod` replaced by any `e ≥ e_mod`, and
Corollary 2.2 uses `d*_mod` anyway), `log(d_{F_tpd})`, `log(f_{F_tpd})` the different and
conductor degrees of the tripodal field, the distinguished primes and `log(d^K_p)`. -/
noncomputable def InitialThetaData.invariants :
    Theorem110Invariants (concreteVariantData D) where
  emod := D.dmod
  one_le_emod := D.one_le_dmod
  emod_le_dmod := le_rfl
  logDtpd := logDifferentDeg ↥D.tripodalField
  logDtpd_nonneg := logDifferentDeg_nonneg _
  logFtpd := D.logConductorDeg
  logFtpd_nonneg := D.logConductorDeg_nonneg
  dst := D.dst
  dst_prime := D.dst_prime
  logDK := D.logDK
  logDK_nonneg := D.logDK_nonneg
  logDK_eq_zero := D.logDK_eq_zero

/-- **The tower arithmetic of Theorem 1.10** (IUT IV, Steps (ii)–(iii) and (R4)): standard
algebraic number theory of the tower `F_mod ⊆ F_tpd ⊆ F ⊆ K = F(E[ℓ])`, from
Proposition 1.3 (differents in towers of local fields, taxis #1463), Proposition 1.8
(reduction theory, taxis #5; Néron–Ogg–Shafarevich, taxis #73) and the Galois-group
inclusions `Gal(K/F) ↪ GL₂(𝔽_ℓ)`, `Gal(F/F_tpd) ↪ GL₂(𝔽_3) × GL₂(𝔽_5) × ℤ/2`,
`Gal(F_tpd/F_mod) ↪ GL₂(𝔽_2)`. With `e_mod` replaced by `d_mod` and `e*_mod = 552960·d_mod`.
For the Θ-data of the points of the tripod it is proved in this repository
(`Iut.Tripod.towerArithmetic_of_towerLocalHyp`, `Iut/Tripod/Tower.lean`, from the local facts
`Iut.Tripod.TowerLocalHyp`, which are theorems in `Iut/Tripod/`); no external repository (such
as `lana-agents/elliptic-reduction`) is used. -/
structure TowerArithmetic (D : InitialThetaData.{u}) : Prop where
  /-- **(R4)**: if `e_v > p_v − 2` then `p_v ≤ e*_mod·ℓ` and
  `log e_v ≤ −3 + 4·log(e*_mod·ℓ)`. -/
  ramIdx_bound : ∀ v : FinitePlace D.Kt, residueChar v - 2 < ramIdx D.Kt v →
    residueChar v ≤ 552960 * D.dmod * D.ℓ ∧
      Real.log (ramIdx D.Kt v) ≤ -3 + 4 * Real.log (((552960 * D.dmod : ℕ) : ℝ) * D.ℓ)
  /-- **Step (ii)**: `log(d_K) ≤ log(d_{F_tpd}) + log(f_{F_tpd}) + 2·log ℓ + 21`. -/
  step_ii : ∑ p ∈ D.dst, D.logDK p ≤
    logDifferentDeg ↥D.tripodalField + D.logConductorDeg + 2 * Real.log D.ℓ + 21
  /-- **Step (iii)**: `log(s^ℚ) ≤ 2·d_mod·(log(d_{F_tpd}) + log(f_{F_tpd})) + 5 + log ℓ`. -/
  step_iii : ∑ p ∈ D.dst, Real.log p ≤
    2 * D.dmod * (logDifferentDeg ↥D.tripodalField + D.logConductorDeg) + 5 + Real.log D.ℓ

variable {D}

/-- The residue characteristics of the bad places of `F` are distinguished ((D2)). -/
lemma InitialThetaData.bad_mem_dst (w : FinitePlace D.F)
    (hw : w ∈ (concreteVariantData D).qPilot.badFinset) : residueChar w ∈ D.dst :=
  D.mem_dst_of_badChars _ (D.bad_residueChar_mem w
    ((concreteVariantData D).qPilot.mem_bad hw))

/-- The arithmetic certificate of Theorem 1.10 for the concrete invariants, from `ℓ ≥ 7`
and the tower arithmetic. -/
theorem TowerArithmetic.certificate (TA : TowerArithmetic D) (h7 : 7 ≤ D.ℓ) :
    Theorem110Certificate (D.invariants) where
  seven_le := h7
  bad_mem_dst := InitialThetaData.bad_mem_dst
  step_ii := by exact TA.step_ii
  step_iii := by exact TA.step_iii

end Iut