Composition of the Corvaja--Zannier plane-curve endpoint

This module discharges the algebraic and numerical bookkeeping between the public plane-curve interface and the remaining global geometric estimate. It constructs the powered-image relation from IsCorvajaZannierPlaneCurve, proves that the two powered torsion functions are nonzero, identifies the finite-set cardinality with the torsion-point subtype cardinality, and composes the Dedekind gcd divisor estimate with the proved numerical optimization.

The only remaining input is exposed as the ordinary proposition GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange. Its certificate is precisely a gcd-divisor number which bounds the rational torsion points, satisfies the trivial degree bound, and satisfies the Corvaja--Zannier Proposition 2 alternatives. No axiom or typeclass hides this geometric obligation.

theorem BGS.CorvajaZannier.pow_sub_one_ne_zero_of_transcendental {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {z : L} (hz : Transcendental K z) (n : ℕ) (hn : 0 < n) : z ^ n - 1 ≠ 0

theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_eq_torsionPoint_card {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) : (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card = Fintype.card (TorusCurveTorsionPoint f firstOrder secondOrder)

theorem BGS.CorvajaZannier.poweredTorsionFunctions_ne_zero_of_isCorvajaZannierPlaneCurve {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hcurve : External.IsCorvajaZannierPlaneCurve f) (firstOrder secondOrder : ℕ) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) : have hf := ⋯; planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0 ∧ planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_spec_of_isCorvajaZannierPlaneCurve {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (firstDegree secondDegree firstOrder secondOrder : ℕ) (hbidegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hcurve : External.IsCorvajaZannierPlaneCurve f) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) : have hf := ⋯; have g := poweredCoordinateImageRelation hf ⋯ firstOrder hfirstOrder secondOrder; Irreducible g ∧ evalBivariate (planeCurveFunction f 0 ^ firstOrder) (planeCurveFunction f 1 ^ secondOrder) g = 0 ∧ 0 < g.natDegree ∧ 0 < (transposeBivariate g).natDegree ∧ g.natDegree ≤ firstOrder * secondDegree ∧ (transposeBivariate g).natDegree ≤ secondOrder * firstDegree ∧ ∀ (i : ℕ), (g.coeff i).natDegree ≤ secondOrder * firstDegree

The public curve hypotheses instantiate the canonical powered-image relation, including the advertised source bidegree bounds.

def BGS.CorvajaZannier.planeCurveTorsionLowerDegree (firstDegree secondDegree firstOrder secondOrder : ℕ) : ℕ

The smaller of the degrees of x ^ firstOrder and y ^ secondOrder, using only the public bidegree bounds.

Equations

• BGS.CorvajaZannier.planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder = min (secondOrder * firstDegree) (firstOrder * secondDegree)

def BGS.CorvajaZannier.planeCurveTorsionUpperDegree (firstDegree secondDegree firstOrder secondOrder : ℕ) : ℕ

The larger of the degrees of x ^ firstOrder and y ^ secondOrder, using only the public bidegree bounds.

Equations

• BGS.CorvajaZannier.planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder = max (secondOrder * firstDegree) (firstOrder * secondDegree)

theorem BGS.CorvajaZannier.planeCurveTorsionLowerDegree_mul_upperDegree (firstDegree secondDegree firstOrder secondOrder : ℕ) : planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder * planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder = firstOrder * secondOrder * firstDegree * secondDegree

theorem BGS.CorvajaZannier.planeCurveCorvajaZannierNumericalBound_of_propositionTwo (p firstDegree secondDegree firstOrder secondOrder : ℕ) (G : ℝ) (hfirstDegree : 0 < firstDegree) (hsecondDegree : 0 < secondDegree) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) (hp : 0 < p) (hGNonneg : 0 ≤ G) (hGTrivial : G ≤ ↑(planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder)) (hPropositionTwo : PropositionTwoNumericalAlternatives (planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder) (planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder) p (2 * firstDegree * secondDegree) G) : G ≤ Markoff.corvajaZannierCorollaryTwoNumericalBound p firstOrder secondOrder firstDegree secondDegree (External.planeTorusEulerCharacteristicBound firstDegree secondDegree)

Proposition 2 plus the trivial gcd bound gives exactly the numerical right-hand side of the public plane-curve theorem, independently of which powered coordinate has the smaller degree.

def BGS.CorvajaZannier.PlaneCurvePropositionTwoCertificate (p : ℕ) (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) : Prop

A certificate for the only remaining geometric input at the endpoint. The real number G is intended to be the degree of the gcd divisor of the two powered torsion functions. Its fields state, respectively, that every rational torsion point contributes to it, that the elementary divisor bound holds, and that the Corvaja--Zannier Proposition 2 alternatives hold.

Equations

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

theorem BGS.CorvajaZannier.propositionTwoNumericalAlternatives_mono {a b p chi : ℕ} {G H : ℝ} (hGH : G ≤ H) (hH : PropositionTwoNumericalAlternatives a b p chi H) : PropositionTwoNumericalAlternatives a b p chi G

Proposition 2's alternatives are downward closed in the gcd quantity.

theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_le_corvajaZannierBound_of_certificate (p : ℕ) (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) (hfirstDegree : 0 < firstDegree) (hsecondDegree : 0 < secondDegree) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) (hp : 0 < p) (hcertificate : PlaneCurvePropositionTwoCertificate p K f firstDegree secondDegree firstOrder secondOrder) : ↑(External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ Markoff.corvajaZannierCorollaryTwoNumericalBound p firstOrder secondOrder firstDegree secondDegree (External.planeTorusEulerCharacteristicBound firstDegree secondDegree)

theorem BGS.CorvajaZannier.planeCurvePropositionTwoCertificate_of_dedekindGcdSum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (p firstDegree secondDegree firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (htrivial : ↑(∑ v ∈ torsionGcdPlaceSupport firstOrder secondOrder, torsionGcdMultiplicity firstOrder secondOrder v) ≤ ↑(planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder)) (hpropositionTwo : PropositionTwoNumericalAlternatives (planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder) (planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder) p (2 * firstDegree * secondDegree) ↑(∑ v ∈ torsionGcdPlaceSupport firstOrder secondOrder, torsionGcdMultiplicity firstOrder secondOrder v)) : PlaneCurvePropositionTwoCertificate p K f firstDegree secondDegree firstOrder secondOrder

The explicit Dedekind gcd sum supplies a Proposition 2 certificate once the two still-geometric inequalities for that sum have been proved.

theorem BGS.CorvajaZannier.planeCurvePropositionTwoCertificate_of_dedekindGcdSum_and_bidegree {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (p firstDegree secondDegree firstOrder secondOrder : ℕ) (hbidegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hcurve : External.IsCorvajaZannierPlaneCurve f) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (hpropositionTwo : PropositionTwoNumericalAlternatives (planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder) (planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder) p (2 * firstDegree * secondDegree) ↑(∑ v ∈ torsionGcdPlaceSupport firstOrder secondOrder, torsionGcdMultiplicity firstOrder secondOrder v)) : PlaneCurvePropositionTwoCertificate p K f firstDegree secondDegree firstOrder secondOrder

The sharp fiber-counting bound supplies the trivial certificate bound directly. Consequently an upper gcd divisor only has to satisfy Proposition 2; it need not separately be proved below the smaller coordinate height.

theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_le_corvajaZannierBound_of_dedekindGcdSum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (p firstDegree secondDegree firstOrder secondOrder : ℕ) (hfirstDegree : 0 < firstDegree) (hsecondDegree : 0 < secondDegree) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) (hp : 0 < p) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (htrivial : ↑(∑ v ∈ torsionGcdPlaceSupport firstOrder secondOrder, torsionGcdMultiplicity firstOrder secondOrder v) ≤ ↑(planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder)) (hpropositionTwo : PropositionTwoNumericalAlternatives (planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder) (planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder) p (2 * firstDegree * secondDegree) ↑(∑ v ∈ torsionGcdPlaceSupport firstOrder secondOrder, torsionGcdMultiplicity firstOrder secondOrder v)) : ↑(External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ Markoff.corvajaZannierCorollaryTwoNumericalBound p firstOrder secondOrder firstDegree secondDegree (External.planeTorusEulerCharacteristicBound firstDegree secondDegree)

A concrete Dedekind gcd sum satisfying the divisor and Proposition 2 inequalities gives the public numerical endpoint directly.

def BGS.CorvajaZannier.GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange : Prop

The remaining above-elementary-range assertion, now reduced to explicit Proposition 2 certificates. It contains no axiom or typeclass assumption.

Equations

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

theorem BGS.CorvajaZannier.generalCorvajaZannierPlaneCurveTheoremAboveElementaryRange_of_certificates (hcertificates : GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange) : External.GeneralCorvajaZannierPlaneCurveTheoremAboveElementaryRange

theorem BGS.CorvajaZannier.generalCorvajaZannierPlaneCurveTheorem_of_certificates (hcertificates : GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange) : External.GeneralCorvajaZannierPlaneCurveTheorem

The exact endpoint follows from the remaining certificate proposition; the complementary characteristic range is the proved elementary theorem.