Definitions/Def_FreyPackage_LoweringAtUniform.lean

Fix a Frey package P=(a,b,c,p), so a^p+b^p=c^p with abc\neq0, \gcd(a,b)=1, a\equiv3\pmod 4, b\equiv0\pmod 2 and p\ge 5 prime, and let freyCurveInt P be the explicit integral Weierstrass model with a_1=1, a_2=(b^p-1-a^p)/4, a_3=a_6=0, a_4=-a^pb^p/16.

The first definition, ModularRepOfLevelNewAtPinned P M q, asserts the existence of a cusp form g of weight 2 on \Gamma_0(M) and a maximal ideal \mathfrak m of the ring \overline{\mathbb Z} of algebraic integers in \mathbb C such that: g is a normalised eigenform in the project's sense (first q-coefficient 1, multiplicativity at coprime indices, and the two Hecke recursions at prime powers according as the prime divides M or not); \mathfrak m contains p; for every prime \ell with \ell\nmid \Delta(\mathtt{freyCurveInt }P), \ell\nmid M and \ell\neq p there is an algebraic integer a whose complex value is the \ell-th q-expansion coefficient of g and with a-a_\ell\in\mathfrak m, where a_\ell=\ell+1-\#(\mathtt{freyCurveInt }P\bmod \ell)(\mathbb F_\ell); and g satisfies the project's newness condition at q, namely that its q-th coefficient squares to 1. So the congruence is pinned to the one fixed integral model, with no existential quantification over integral models of the Frey curve.

The remaining three definitions are statement bundles of level-lowering form, each a \Pi-type whose conclusion is the pinned condition ModularRepOfLevelAt N (the same congruence data at level N, without the newness clause). MazurPrincipleNewLoweringAtUniform P q says: for all N>0 with q prime, q\neq2, q\neq p, q\nmid N, with p\nmid q^2-1 (the negation of ExchangeCongruence), with the mod-p representation on the p-torsion of the Frey curve over \overline{\mathbb Q} irreducible (no Galois-stable \mathbb Z/p-submodule other than 0 and everything, the torsion being nontrivial), and with freyGaloisRep unramified at q (inertia at every valuation subring lying over q is in the kernel), a pinned witness at level Nq new at q gives the pinned condition at level N. ExchangeCaseLoweringAtUniform P q is the same implication with p\mid q^2-1 assumed instead. AtPNewLoweringAtUniform P treats removal of p itself: for N_0>0 with p\nmid N_0, irreducibility, and p\mid v_p(\Delta) of the Frey curve over \mathbb Q (the IsPeuRamifieeAt condition), a pinned witness at level N_0p new at p gives the pinned condition at level N_0. A local classical decidable-equality instance on \overline{\mathbb Q} accompanies the definitions.