Definitions/Def_ModularCurve_JZeroNeronAtPDataOrdV22.lean

Fix N \ge 1, a prime q with q \nmid N, and a valuation subring A of \overline{\mathbb Q} whose maximal ideal contains q (the predicate ValuationSubring.LiesOverPrime, i.e. q is a non-unit of A); write J = J_0(Nq) for the project's Jacobian JZero (N * q) and \mathbb T = HeckeAlg = \mathbb Z[X_\ell : \ell \text{ prime}], acting on J through heckeModuleBar. The structure JZeroNeronAtPDataOrdV22 extends JZeroNeronAtPDataOrdCore by a single further field. The inherited data consist of the three-step filtration \mathrm{toric}(m) \le \mathrm{fin}(m) \le \mathrm{finPart}(m) \le J[m] with its compatibilities under divisibility, its Hecke- and decomposition-stability, the inertia laws on the toric part, the component-group module \Phi with its specialisation maps and Eisenstein relations, the abelian quotient maps to J_0(N)^2, the Raynaud prolongation clause, the cardinality pins \#\mathrm{toric}(m) = m^{\mathrm{toricRank}} and \#\mathrm{fin}(m) = m^{\mathrm{toricRank}+2\,\mathrm{abelianRank}}, the two lower-level detection clauses, and the monodromy inclusion \sigma x - x \in \mathrm{fin}(m) for every m \ne 0, every \sigma in the inertia subgroup of A over \mathbb Q and every x \in J[m].

The new field toric_card_heckeTorsion_le asserts a bound on the toric \mathfrak m-torsion. It is required only under the following guards: q \ne 2; the Hecke inputs HeckeInputsAll (N * q) and the commutation hypothesis HeckeOperatorsCommuteBar (N * q); and, for a maximal ideal \mathfrak m \subseteq \mathbb T which is not eventually Eisenstein (there is no finite set S of primes with T_\ell - (\ell+1) \in \mathfrak m for all \ell \notin S), with q \in \mathfrak m, with \mathbb T/\mathfrak m finite, and with \dim_{\mathbb T/\mathfrak m} J[\mathfrak m] = 2, where J[\mathfrak m] = \{x \in J : t x = 0 \ \forall t \in \mathfrak m\}. Under these hypotheses the conclusion is \#\bigl(\mathrm{toric}(q) \cap J[\mathfrak m]\bigr) \le \#(\mathbb T/\mathfrak m), the intersection being taken inside the additive group J. Thus the multiplicity-one hypothesis on J[\mathfrak m] is built into the clause rather than derived. The predicate HasJZeroNeronAtPDataOrdV22 N q hqN says that such a datum exists for every valuation subring of \overline{\mathbb Q} lying over q.