lemmaroutineinferred_dep

Modular level is polynomially bounded in M

Bounds the newform level by N≤CMaN\le CM^a
makes the modular Jacobian polynomial in M
Lemma·hei:level-bound·§4.8 A uniform bound for the modular level

Statement (paper)

There are fixed constants C,a>0C,a>0 such that N≤CMa. N\le C M^a.

In plain English

There are fixed constants C,a>0C,a>0 such that the level NN of the weight-two newform attached to rℓr_\ell satisfies N≤CMaN\le CM^a.

Why it's here

The proof turns the level into a product of local Artin conductors. Large primes of TT are tame, contributing exponent at most two, and the finitely many small primes contribute a constant via uniform ramification cuts, giving the polynomial bound (in fact a=2a=2). It uses the field bound from hei-hom-field and the sign-splitting cochain from hei-sign-splitting, and the polynomial bound on NN feeds the Faltings height estimate.
Classified routine:
Follows from the standard expression of the newform level as a product of local Artin conductors (Carayol's theorem on levels of modular Galois representations), using tame ramification at large primes and a bounded wild contribution at the finitely many small primes. The input bounds come from the earlier field and cochain lemmas.

Uses

lem3-adic and 2-adic representations are compatiblelemSign-splitting cochain with square-root characterlemBounded field for all geometric homomorphisms

Used by

claimFaltings height of A is polynomial in M

Inside the proof

claimLevel exponents equal Artin conductorsclaimLarge primes in T are tameclaimUniform ramification cut for betaclaimWild inertia acts trivially over F_1claimUniform conductor bound gives N ≤ CM²

Sources

PaperOpen
Section
§4.8 A uniform bound for the modular level
Page
—
Label
hei:level-bound
Line
sections/04-height.tex:1043
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof repeatedly uses the field L and its uniformly bounded degree ('the uniform upper bound for [L:Q]', 'The uniform local bounds use the bounded degree of L'), which is the field constructed in that lemma.