Research proof index

The Lambert series rearrangement ∑_{n≥1} n³qⁿ/(1-qⁿ) = ∑_{n≥1} σ₃(n)qⁿ for |q| < 1: the defining series of tateA₄ is the evaluation of the formal series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧.

The Lambert series rearrangement for tateA₆, as for tateA₄_eq_evalInt; the bookkeeping of the exact division by 12 uses 12 ∣ 5d³ + 7d⁵ termwise.

The construction of the Tate curve commutes on the nose with any valuative morphism: its coefficients are power series in q with integer coefficients, and the partial sums converge at matching rates on both sides (TateCurve.evalInt_map). The same is true of the uniformisation tateCurveEquiv (a statement we defer, as it needs transport along this e...

The c₄ of the base change has adic valuation 1. Multiplicative reduction of E makes the canonical valuation |E.c₄| = 1 (via adicValuation_eq_one_iff and integralModel_c₄_eq, as in WeierstrassCurve.valuation_c₄_eq_one); this transfers to l by valuation_algebraMap_eq_one, and converts back to the adic valuation over 𝒪[l]. Shared by `isM...

The discriminant of the base change has adic valuation < 1. Multiplicative reduction of E makes |E.Δ| < 1 (via adicValuation_lt_one_iff and integralModel_Δ_eq, as in WeierstrassCurve.valuation_Δ_lt_one); this transfers to l by valuation_algebraMap_lt_one, and converts back to the adic valuation over 𝒪[l].

The base change of the twisted integral model has nonzero discriminant: its Δ is (t'² - 4n')⁶ · Δ (Δ_quadraticTwistOf), and both factors are nonzero.