TateCurveBaseChange.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

11 declarations, 0 contain sorry, 0 declared as axioms

Base change of integral power series evaluations

Support for the functoriality of the Tate curve (WeierstrassCurve.tateCurve_baseChange): the coefficients of the Tate curve are evaluations TateCurve.evalInt of integral power series, and such evaluations commute with any valuative extension k → l of nonarchimedean local fields (TateCurve.evalInt_map below) — both evaluations are within |q|^N of the common N-th partial sum, whose bound transfers along the strictly monotone map of value groups ValuativeExtension.mapValueGroupWithZero, so no continuity argument is needed.

To apply this to the Tate curve one needs its defining coefficient series tateA₄, tateA₆ — which are Lambert-type series ∑_{n≥1} c(n)qⁿ/(1-qⁿ), not power series — to be such evaluations. This is the Lambert series rearrangement ∑_{m≥1} c(m)qᵐ/(1-qᵐ) = ∑_{N≥1} (∑_{d ∣ N} c(d))qᴺ (TateCurve.tsum_lambert), proved by expanding each qᵐ/(1-qᵐ) as a geometric series and regrouping the double series along the fibres of (m, j) ↦ mj. The corresponding formal power series over ℤ are TateCurve.a₄Formal and TateCurve.a₆Formal; the identities tateA₄ q = evalInt q a₄Formal, tateA₆ q = evalInt q a₆Formal are proved in FLT.KnownIn1980s.EllipticCurves.TateCurve, where tateA₄ and tateA₆ are defined.

Everything here is extracted (minimally) from FLT PR #1081.

Imports (3)

Imported by 2 files

def TateCurve.a₄Formal The formal a₄-series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₄ line 53 source
Source documentation
The formal a₄-series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₄.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: HMul.hMul, Unit, Neg.neg, OfNat.ofNat, TateCurve.sInt, Nat
15 instances, coercions and auxiliary constants left out.
```
noncomputable def a₄Formal : ℤ⟦X⟧ :=
…
```
Mentions: TateCurve.X
def TateCurve.a₆Formal The formal a₆-series a₆(q) = -(5s₃(q) + 7s₅(q))/12 ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₆ line 59 source
Source documentation
The formal a₆-series a₆(q) = -(5s₃(q) + 7s₅(q))/12 ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₆. The division is exact, since 12 ∣ 5d³ + 7d⁵ for every d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PowerSeries, Int
Proof uses: PowerSeries.mk, Nat, Neg.neg, HDiv.hDiv, HAdd.hAdd, HMul.hMul, OfNat.ofNat, ArithmeticFunction, ArithmeticFunction.sigma
15 instances, coercions and auxiliary constants left out.
```
noncomputable def a₆Formal : ℤ⟦X⟧ :=
…
```
Mentions: TateCurve.X
theorem TateCurve.coeff_a₄Formal line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, TateCurve.a₄Formal, HMul.hMul, Neg.neg, OfNat.ofNat, ArithmeticFunction, ArithmeticFunction.sigma
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, RingHom, PowerSeries.C, PowerSeries.mk, congrFun', Eq.symm, map_ofNat, neg_mul, map_neg, PowerSeries.coeff_C_mul, PowerSeries.coeff_mk, eq_self
78 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TateCurve.coeff_a₆Formal line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, TateCurve.a₆Formal, Neg.neg, HDiv.hDiv, HAdd.hAdd, HMul.hMul, OfNat.ofNat, ArithmeticFunction, ArithmeticFunction.sigma
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, PowerSeries.coeff_mk, eq_self
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem TateCurve.evalInt_sub line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, IsTopologicalRing, T2Space, PowerSeries, Int, Summable, Nat, HMul.hMul, LinearMap, RingHom.id, Unit, PowerSeries.coeff, HPow.hPow, SummationFilter.unconditional, Eq, TateCurve.evalInt, HSub.hSub
Proof uses: Eq.mpr, tsum, id, congrFun', congrArg, SummationFilter, optParam, funext, Eq.trans, map_sub, RingHom, Int.cast_sub, sub_mul, Summable.tsum_sub
85 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem TateCurve.hasSum_geometric_succ The geometric series over a nonarchimedean local field: for |x| < 1, x + x² + x³ + ⋯ = x/(1 - x) line 105 source
Source documentation
The geometric series over a nonarchimedean local field: for |x| < 1, x + x² + x³ + ⋯ = x/(1 - x). (Summability is by the nonarchimedean criterion — the terms tend to zero — and the value is identified through the partial sums x(xⁿ - 1)/(x - 1).)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, HasSum, Nat, HPow.hPow, HAdd.hAdd, HDiv.hDiv, HSub.hSub, SummationFilter.unconditional
Proof uses: Ne, Eq, False, False.elim, Eq.mp, Eq.trans, congrFun', congrArg, map_one, Eq.symm, Iff.mpr, sub_ne_zero, Ne.symm, Summable, TateCurve.summable_of_valuation_le_pow, Set.Finite.subset, Set.Iio, Set.finite_Iio, Set.ofPred, Membership.mem and 119 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem hasSum_geometric_succ {x : k} (hx : valuation k x < 1) :
    HasSum (fun j : ℕ ↦ x ^ (j + 1)) (x / (1 - x)) := by
…
```
theorem TateCurve.tsum_lambert The Lambert series rearrangement over a nonarchimedean local field: for any integer coefficients c and |q| < 1, ∑_{m≥1} c(m)qᵐ/(1 - qᵐ) = ∑_{N≥1} (∑_{d ∣ N} c(d))qᴺ line 137 source
Source documentation
The Lambert series rearrangement over a nonarchimedean local field: for any integer coefficients c and |q| < 1, ∑_{m≥1} c(m)qᵐ/(1 - qᵐ) = ∑_{N≥1} (∑_{d ∣ N} c(d))qᴺ. This is the valuative instantiation of the general tsum_lambert_of_summable (FLT.Slop.NumberTheory.TsumDivisorsAntidiagonal): the geometric row expansions come from hasSum_geometric_succ, and the double series is summable since its terms tend to zero nonarchimedeanly (summable_of_valuation_le_pow).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Nat, Int, Eq, tsum, HDiv.hDiv, HMul.hMul, HAdd.hAdd, HPow.hPow, HSub.hSub, SummationFilter.unconditional, Finset.sum and 1 more
Proof uses: PNat, Eq.mpr, id, congrArg, map_pow, Trans.trans, LE.le, pow_le_pow_right_of_le_one', LT.lt.le, PNat.pos, pow_one, HasSum, Eq.mp, congrFun', SummationFilter, optParam, funext, TateCurve.hasSum_geometric_succ, Summable, Prod and 80 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem tsum_lambert (q : k) (hq : valuation k q < 1) (c : ℕ → ℤ) :
    ∑' m : ℕ, ((c (m + 1) : ℤ) : k) * q ^ (m + 1) / (1 - q ^ (m + 1)) =
      ∑' N : ℕ, ((∑ d ∈ N.divisors, c d : ℤ) : k) * q ^ N := by
…
```
theorem TateCurve.tsum_lambert_eq_evalInt Documented declaration: tsum_lambert_eq_evalInt line 182 source
Source documentation
Bridge form of the Lambert rearrangement: if the coefficients of F ∈ ℤ⟦X⟧ are the divisor sums Fₙ = ∑_{d ∣ n} c(d), then the Lambert series of c is the evaluation of F on the open unit disc. This is the form in which tsum_lambert is consumed: it turns the defining series of the Tate curve coefficients (tateA₄, tateA₆) into evalInts in one step.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Nat, Int, PowerSeries, Eq, LinearMap, RingHom.id, Unit, PowerSeries.coeff, Finset.sum, Nat.divisors, tsum and 7 more
Proof uses: Eq.mpr, id, congrArg, TateCurve.tsum_lambert, tsum_congr, Eq.refl
98 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem tsum_lambert_eq_evalInt (q : k) (hq : valuation k q < 1) (c : ℕ → ℤ) {F : ℤ⟦X⟧}
    (hF : ∀ n, PowerSeries.coeff n F = ∑ d ∈ n.divisors, c d) :
    ∑' m : ℕ, ((c (m + 1) : ℤ) : k) * q ^ (m + 1) / (1 - q ^ (m + 1)) = evalInt q F := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt
theorem TateCurve.valuation_evalInt_sub_sum_le Quantitative tail bound: the evaluation of an integral power series on the open unit disc is within |q|^N of its N-th partial sum line 193 source
Source documentation
Quantitative tail bound: the evaluation of an integral power series on the open unit disc is within |q|^N of its N-th partial sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, PowerSeries, Int, Nat, LE.le, HSub.hSub, TateCurve.evalInt, Finset.sum, Finset.range, HMul.hMul, LinearMap, RingHom.id and 3 more
Proof uses: Eq, Polynomial, PowerSeries.trunc, Not, Membership.mem, Finset, Eq.mpr, Finsupp, Polynomial.coeff, id, congrArg, Polynomial.coeff_coe, ite, PowerSeries.coeff_trunc, ite_eq_right, Eq.mp, Eq.trans, Int.cast_zero, MulZeroClass.zero_mul, Eq.refl and 16 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_evalInt_sub_sum_le (q : k) (hq : valuation k q < 1)
    (F : ℤ⟦X⟧) (N : ℕ) :
    valuation k (evalInt q F -
      ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) ≤
    valuation k q ^ N := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt
theorem TateCurve.valuation_algebraMap_lt_one A valuative extension maps the open unit disc into the open unit disc: the induced map of value groups (ValuativeExtension.mapValueGroupWithZero) is strictly monotone line 223 source
Source documentation
A valuative extension maps the open unit disc into the open unit disc: the induced map of value groups (ValuativeExtension.mapValueGroupWithZero) is strictly monotone.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, Algebra, ValuativeExtension, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, RingHom, Algebra.algebraMap
Proof uses: Eq.mp, MonoidWithZeroHom, ValuativeExtension.mapValueGroupWithZero, congr, congrArg, ValuativeExtension.mapValueGroupWithZero_valuation, map_one, ValuativeExtension.mapValueGroupWithZero_strictMono
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_algebraMap_lt_one {q : k} (hq : valuation k q < 1) :
    valuation l (algebraMap k l q) < 1 := by
…
```
theorem TateCurve.evalInt_map Documented declaration: evalInt_map line 232 source
Source documentation
Evaluation of integral power series commutes with valuative extensions of nonarchimedean local fields: the coefficients are (the same) integers on both sides, and both evaluations are within |q|^N of the common N-th partial sum (valuation_evalInt_sub_sum_le), whose bound transfers along the strictly monotone map of value groups — no continuity argument is needed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, Algebra, ValuativeExtension, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, PowerSeries, Int, Eq, RingHom, Algebra.algebraMap, TateCurve.evalInt
Proof uses: TateCurve.valuation_algebraMap_lt_one, Eq.mpr, HSub.hSub, id, congrArg, Eq.symm, propext, sub_eq_zero, Classical.byContradiction, Not, Nat, HPow.hPow, Units.mk0, Iff.mpr, Ne, Valuation.ne_zero_iff, Exists, False, ValuativeRel.exists_pow_valuation_lt, Finset.sum and 63 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem evalInt_map (q : k) (hq : valuation k q < 1) (F : ℤ⟦X⟧) :
    algebraMap k l (evalInt q F) = evalInt (algebraMap k l q) F := by
…
```
Mentions: TateCurve.X, TateCurve.evalInt