Rational points of order thirty-five #

This module reserves the permanent library destination for the order-35 challenge. A solution belongs here; the published challenge module can then become a thin, immutable bridge to that theorem.

source

@[instance_reducible]

noncomputable def MazurTorsion.OrderThirtyFive.instDecidableEqResidueFieldSubtypeAdicCompletionIntRatAtElevenMemValuationSubringAdicCompletionIntegers :

DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven))

Equations

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

Instances For

source

theorem MazurTorsion.OrderThirtyFive.reductionAtEleven_addOrderOf_ne_thirtyFive (W : WeierstrassCurve (ZMod 11)) [W.IsElliptic] (P : W.toAffine.Point) :

addOrderOf P ≠ 35

The checked F_11 enumeration rules out a specialized point of exact order 35. The remaining rational theorem must construct this point through the squarefree-level formal-immersion and Néron-specialization route.

source

theorem MazurTorsion.OrderThirtyFive.rationalPoint_addOrderOf_ne_thirtyFive_of_goodReductionAtEleven {E : WeierstrassCurve.Affine ℚ} {W₀ : WeierstrassCurve ℤ} (hE : W₀.map (algebraMap ℤ ℚ) = E) [WeierstrassCurve.IsElliptic E] [WeierstrassCurve.IsElliptic (WeierstrassCurve.Affine.redCurve IntegerPrimeSpecialization.atEleven W₀)] {P : E.Point} :

addOrderOf P ≠ 35

If an integral model has good reduction at eleven, a rational point on its generic fibre cannot have exact order 35. This is the checked join between unramified specialization and the exhaustive F_11 certificate.

source

theorem MazurTorsion.OrderThirtyFive.addOrderOf_ne_thirtyFive_of_tameAdditiveFiltrationAtEleven {G : Type u} [AddCommGroup G] (F : EllipticCurve.TameAdditiveFiltrationData G) (hresidue : Nat.card F.ResidueAdditive = 11) (P : G) :

addOrderOf P ≠ 35

A tame additive filtration with eleven-element residue group has no point of exact order 35. This is the local bad-fibre consumer that the future Néron-model construction must instantiate.

source

theorem MazurTorsion.OrderThirtyFive.addOrderOf_ne_thirtyFive_of_componentExponentTwelveAtEleven {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) {ResidueAdditive : Type v} [AddCommGroup ResidueAdditive] [Finite ResidueAdditive] (identityReduction : ↥identitySubgroup →+ ResidueAdditive) (formalKernel : AddSubgroup ↥identitySubgroup) (identityReduction_ker : identityReduction.ker = formalKernel) (formalKernel_torsionFree : ∀ (Q : ↥formalKernel), IsOfFinAddOrder Q → Q = 0) (hresidue : Nat.card ResidueAdditive = 11) (P : G) (hcomponent : 12 • P ∈ identitySubgroup) :

addOrderOf P ≠ 35

The order-35 additive contradiction through the narrower tame component-exponent handoff. The universal exponent 12 is coprime to 35, and the eleven-element additive residue group is also coprime to 35; no cardinality or finiteness of the full component quotient is used.

source

The order-35 additive-fibre contradiction from the canonical eleven-adic reduction data. The component is the quotient by the specified identity subgroup, reduction targets the actual eleven-adic residue field, and formal-kernel torsion-freeness comes from the checked unramified formal-group theorem.

source

theorem MazurTorsion.OrderThirtyFive.addOrderOf_ne_thirtyFive_of_nonsingularReductionAtEleven {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)] (especial : (WeierstrassCurve.Affine.adicRedCurve W₀).Point ≃+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (hcomponent : Nat.card (W.Point ⧸ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯) ≤ 4) (P : W.Point) :

addOrderOf P ≠ 35

The order-35 additive-fibre contradiction using only canonical coordinatewise nonsingular reduction. The identity subgroup and its reduction map are constructed, rather than supplied; the group-law compatibility is checked, and the remaining inputs are the additive classification of the actual special cubic and the genuine component bound.

source

theorem MazurTorsion.OrderThirtyFive.addOrderOf_ne_thirtyFive_of_nonsingularReduction_of_componentExponentTwelveAtEleven {W : WeierstrassCurve.Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)) = W) [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ IntegerPrimeSpecialization.atEleven)] (especial : (WeierstrassCurve.Affine.adicRedCurve W₀).Point ≃+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (P : W.Point) (hcomponent : 12 • P ∈ WeierstrassCurve.Affine.nonsingularReductionSubgroup hW ⋯) :

addOrderOf P ≠ 35

The canonical eleven-adic additive contradiction through the component-exponent handoff.

This is the first geometric consumer of addOrderOf_ne_thirtyFive_of_componentExponentTwelveAtEleven: coordinatewise nonsingular reduction supplies the identity subgroup and reduction homomorphism, while the exact-pinned formal-group theorem supplies torsion-freeness of its kernel. The remaining component input is only the marked-point assertion 12 • P ∈ E₀; no component quotient or cardinality bound is constructed.

source

addOrderOf P ≠ 35

In the order-one branch of the normalized tame Tate equation at eleven, every local point belongs to the canonical nonsingular-reduction subgroup. The checked eleven-adic filtration therefore excludes a marked point of exact order thirty-five.

source

addOrderOf P ≠ 35

In the next coefficient branch at eleven, the tangent calculation puts the marked double in canonical nonsingular reduction. The established exponent-twelve endpoint therefore excludes exact order thirty-five.

source

addOrderOf P ≠ 35

In the exact depth-two a₆ branch at eleven, the checked tangent--secant calculation puts the twelfth multiple of the marked point in canonical nonsingular reduction. This is incompatible with exact order thirty-five.

source

addOrderOf P ≠ 35

A simple marked root of the exceptional cubic at eleven forces the marked twelfth multiple into canonical nonsingular reduction, contradicting exact order thirty-five.

source

addOrderOf P ≠ 35

A nonzero repeated marked root of the exceptional cubic at eleven forces the marked twelfth multiple into canonical nonsingular reduction, contradicting exact order thirty-five.

source

(IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) D.X = 0 ∧ (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) D.A = 0 ∧ (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) D.B = 0 ∧ D.x ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven) ^ 2 ∧ W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven) ^ 3 ∧ W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven) ^ 4

For an order-35 point on the selected eleven-adic short equation, a repeated marked exceptional root must be zero. The marked abscissa and both coefficients consequently gain one power of the same bundled uniformizer.

source

addOrderOf P ≠ 35

On the selected marked branch, a₆ ∉ 𝔪⁵ puts 12P in canonical nonsingular reduction, contradicting exact order thirty-five over the eleven-adic field.

source

W₀.a₆ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven) ^ 5

An order-35 marked point forces a₆ to gain the fifth power of the maximal ideal on the same selected eleven-adic short model.

source

addOrderOf P ≠ 35

Exact depth three of a₄ on the selected marked branch puts 12P in canonical nonsingular reduction, contradicting exact order thirty-five.

source

W₀.a₄ ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven) ^ 4

An order-35 marked point forces a₄ to weighted depth four on the same selected eleven-adic short model.

Documentation

MazurTorsion.Kubert.OrderThirtyFive

Rational points of order thirty-five #