The level-seven modular correspondence has no noncuspidal rational point

The symmetric bidegree-(7,7) polynomial G obtained by removing the diagonal from the level-seven hauptmodul modular equation is a plane model of X₀(49). An explicit rational map, discovered by exact q-expansion fits and verified here purely algebraically, sends every rational solution with s·B ≠ 0 to an affine rational point of the X₀(49) Weierstrass model y² = x(x² + 21x + 112) whose abscissa is nonzero. The complete two-isogeny descent proved that the only rational points of that model are 0 and (0,0), so no such solution exists: the affine curve G = 0 has no rational point outside the singular cusp image (0,0).

theorem MazurTorsion.XZeroFortyNine.no_noncuspidal_correspondence_point {s B : ℚ} (hs : s ≠ 0) (hB : B ≠ 0) (hG : Kubert.orderSevenG7F s B = 0) : False

The affine level-seven modular correspondence has no rational point away from the singular cusp image: G(s,B) = 0 with s·B ≠ 0 is impossible over ℚ.

The explicit order-seven isogeny-tower consumer

The only remaining input in this route is the third polynomial pseudo-division recurrence. All other normalization, isogeny, resultant, and rational-point-classification steps are checked below.

theorem MazurTorsion.XZeroFortyNine.rationalPoint_addOrderOf_ne_fortyNine_of_recurrence3 (hrec3 : Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence3) (E : WeierstrassCurve ℚ) [E.IsElliptic] (P : E.toAffine.Point) : addOrderOf P ≠ 49

The third pseudo-division recurrence completes the explicit order-seven isogeny-tower obstruction to rational points of exact order 49.

This is the named downstream consumer of recurrence3: once that concrete polynomial identity is checked, this theorem supplies the order-49 challenge bridge without any additional geometric hypothesis.

The direct X₀(49) moduli consumer

The checked group-theoretic source datum and the checked two-cusp target are now connected by the exact geometric interface still required from the coarse moduli construction. No explicit Vélu additivity or nonbacktracking isogeny tower occurs in this interface.

noncomputable def MazurTorsion.XZeroFortyNine.splitFiniteFlatSourceOfOrderFortyNineTorsion (E : WeierstrassCurve ℚ) [E.IsElliptic] (M : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface E) (P : E.toAffine.Point) (hP : addOrderOf P = 49) : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.SplitGammaZeroDatum E M

An exact-order-49 rational point supplies the genuine split finite-flat source datum that a future coarse X₀(49) classifying morphism must consume.

This is an actual closed finite-flat subgroup of the represented Weierstrass group scheme, not a postulated point of the modular curve. The remaining geometric theorem is to construct its coarse classifying point and prove that the point is noncuspidal.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.XZeroFortyNine.splitFiniteFlatSourceOfOrderFortyNineTorsion_hasConstantOrder (E : WeierstrassCurve ℚ) [E.IsElliptic] (M : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface E) (P : E.toAffine.Point) (hP : addOrderOf P = 49) : (splitFiniteFlatSourceOfOrderFortyNineTorsion E M P hP).subgroup.carrier.HasConstantOrder 49

The order-49 finite-flat source has geometric order exactly 49.

theorem MazurTorsion.XZeroFortyNine.rationalDatumOfSplitFiniteFlatSourceOfOrderFortyNineTorsion (E : WeierstrassCurve ℚ) [E.IsElliptic] (M : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface E) (P : E.toAffine.Point) (hP : addOrderOf P = 49) : M.rationalDatumOfSplitGammaZeroDatum (splitFiniteFlatSourceOfOrderFortyNineTorsion E M P hP) = ModularCurve.XZeroModuli.RationalDatum.datumOfTorsion E P hP

Recovering coordinate moduli data from the genuine order-49 finite-flat source returns the original datum generated by P. This is the checked handoff to the still-missing coarse classifying construction.

The supplied geometric quotient seam

theorem MazurTorsion.XZeroFortyNine.orderFortyNineGeometricPointQuotientMap_injective (E : WeierstrassCurve ℚ) [E.IsElliptic] (M : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface E) (P : E.toAffine.Point) (hP : addOrderOf P = 49) (Q : AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation (splitFiniteFlatSourceOfOrderFortyNineTorsion E M P hP).subgroup.inclusion) : Function.Injective ⇑(Q.pointQuotientMap (AlgebraicGeometry.AffineCommGroupScheme.testObject ℚ))

If a geometric fppf quotient of the actual order-49 subgroup has been constructed, the quotient of represented rational points embeds in its rational points. This consumes the specific subgroup above; it does not assert that such a quotient presentation exists.

theorem MazurTorsion.XZeroFortyNine.orderFortyNineGeometricPointQuotient_boundary_exact (E : WeierstrassCurve ℚ) [E.IsElliptic] (M : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface E) (P : E.toAffine.Point) (hP : addOrderOf P = 49) (Q : AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation (splitFiniteFlatSourceOfOrderFortyNineTorsion E M P hP).subgroup.inclusion) : Function.MulExact ⇑(Q.pointQuotientMap (AlgebraicGeometry.AffineCommGroupScheme.testObject ℚ)) ⇑(ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumGeometricPointBoundaryHom (ModularCurve.XZeroModuli.RationalDatum.datumOfTorsion E P hP) M Q)

For a supplied geometric quotient of the actual order-49 subgroup, its rational-point image is exactly the zero fibre of the fppf boundary map. In particular no surjectivity of the point quotient map is introduced at the order-49 endpoint.

theorem MazurTorsion.XZeroFortyNine.orderFortyNineGeometricQuotient_baseChange_kernel_inclusion (E : WeierstrassCurve ℚ) [E.IsElliptic] (M : ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface E) (P : E.toAffine.Point) (hP : addOrderOf P = 49) (Q : AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation (splitFiniteFlatSourceOfOrderFortyNineTorsion E M P hP).subgroup.inclusion) (L : Type) [Field L] [Algebra ℚ L] : (Q.baseChange (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℚ L)))).kernelPresentation.inclusion = (splitFiniteFlatSourceOfOrderFortyNineTorsion E M P hP).subgroup.baseChange.inclusion

Extension of the base field preserves the identification of the order-49 subgroup with the geometric kernel of any supplied quotient presentation.

theorem MazurTorsion.XZeroFortyNine.no_rationalDatum_of_classifyingMap (classify : ModularCurve.XZeroModuli.RationalDatum ℚ 49 → curve.toAffine.Point) (hclassify : ∀ (x : ModularCurve.XZeroModuli.RationalDatum ℚ 49), classify x ≠ 0 ∧ classify x ≠ T) : IsEmpty (ModularCurve.XZeroModuli.RationalDatum ℚ 49)

Any classifying map from rational Γ₀(49) data to the explicit X₀(49) model which sends every elliptic datum away from the two cusps forces the rational moduli datum to be empty.

The function and its two noncuspidality laws are the honest missing geometry: they must be constructed from coarse Y₀(49) representability and the identification with curve. The conclusion itself uses the already checked two-cusp classification point_eq_zero_or_T.

theorem MazurTorsion.XZeroFortyNine.rationalPoint_addOrderOf_ne_fortyNine_of_classifyingMap (classify : ModularCurve.XZeroModuli.RationalDatum ℚ 49 → curve.toAffine.Point) (hclassify : ∀ (x : ModularCurve.XZeroModuli.RationalDatum ℚ 49), classify x ≠ 0 ∧ classify x ≠ T) (E : WeierstrassCurve ℚ) [E.IsElliptic] (P : E.toAffine.Point) : addOrderOf P ≠ 49

Real downstream consumer for the order-49 classifying map: a rational point of exact order 49 supplies its generated cyclic subgroup, the classifying map supplies a noncuspidal point on the explicit X₀(49) model, and the two-cusp theorem gives the contradiction.

theorem MazurTorsion.XZeroFortyNine.no_rationalDatum_of_variableChangeClassifyingMap (classify : ModularCurve.XZeroModuli.RationalDatum.VariableChangeClass → curve.toAffine.Point) (hclassify : ∀ (x : ModularCurve.XZeroModuli.RationalDatum.VariableChangeClass), classify x ≠ 0 ∧ classify x ≠ T) : IsEmpty (ModularCurve.XZeroModuli.RationalDatum ℚ 49)

A presentation-independent classifying map from rational Γ₀(49) data modulo admissible Weierstrass changes to the explicit two-cusp model forces the raw rational moduli datum to be empty. Compared with no_rationalDatum_of_classifyingMap, invariance under the checked model changes is now built into the domain rather than left implicit in the missing coarse moduli construction.

theorem MazurTorsion.XZeroFortyNine.rationalPoint_addOrderOf_ne_fortyNine_of_variableChangeClassifyingMap (classify : ModularCurve.XZeroModuli.RationalDatum.VariableChangeClass → curve.toAffine.Point) (hclassify : ∀ (x : ModularCurve.XZeroModuli.RationalDatum.VariableChangeClass), classify x ≠ 0 ∧ classify x ≠ T) (E : WeierstrassCurve ℚ) [E.IsElliptic] (P : E.toAffine.Point) : addOrderOf P ≠ 49

Direct order-49 endpoint for a presentation-independent cyclic-subgroup moduli map. The remaining hypothesis is now exactly a map from the checked variable-change quotient to the explicit X₀(49) model whose image is noncuspidal.