From actual plane-curve degrees to the public Proposition 2 certificate

The canonical divisor argument naturally computes with the actual coordinate degrees degreeOf 0 f and degreeOf 1 f. The public theorem instead accepts arbitrary declared bidegree bounds. This file performs that last change of degree data without asserting the false monotonicity of Proposition 2's degree alternative.

theorem BGS.CorvajaZannier.planeCurveTorsionLowerDegree_actual_le_public {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (firstDegree secondDegree firstOrder secondOrder : ℕ) (hbidegree : External.HasBidegreeAtMost f firstDegree secondDegree) : planeCurveTorsionLowerDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) firstOrder secondOrder ≤ planeCurveTorsionLowerDegree firstDegree secondDegree firstOrder secondOrder

The actual lower powered-coordinate degree is bounded by the lower degree built from any declared bidegree bounds.

theorem BGS.CorvajaZannier.planeCurveTorsionUpperDegree_actual_le_public {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (firstDegree secondDegree firstOrder secondOrder : ℕ) (hbidegree : External.HasBidegreeAtMost f firstDegree secondDegree) : planeCurveTorsionUpperDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) firstOrder secondOrder ≤ planeCurveTorsionUpperDegree firstDegree secondDegree firstOrder secondOrder

The actual upper powered-coordinate degree is bounded by the upper degree built from any declared bidegree bounds.

theorem BGS.CorvajaZannier.planeCurve_actualEulerBudget_le_public {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (firstDegree secondDegree : ℕ) (hbidegree : External.HasBidegreeAtMost f firstDegree secondDegree) : 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f ≤ 2 * firstDegree * secondDegree

The actual bidegree Euler budget is bounded by the public one.

theorem BGS.CorvajaZannier.planeCurvePropositionTwoCertificate_of_actualDegree_exhaustiveGcd {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (p firstDegree secondDegree firstOrder secondOrder : ℕ) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hbidegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hcurve : External.IsCorvajaZannierPlaneCurve f) (hfirstDegree : 0 < firstDegree) (hsecondDegree : 0 < secondDegree) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (hpropositionTwoActual : PropositionTwoNumericalAlternatives (planeCurveTorsionLowerDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) firstOrder secondOrder) (planeCurveTorsionUpperDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) firstOrder secondOrder) p (2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f) ↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond firstOrder secondOrder)) : PlaneCurvePropositionTwoCertificate p K f firstDegree secondDegree firstOrder secondOrder

Proposition 2 at the actual coordinate degrees supplies the public certificate at arbitrary declared bidegree bounds.

The actual Proposition 2 input is allowed to bound the exhaustive gcd degree. The certificate itself uses the torsion-point cardinality. It is below that gcd degree, has the required trivial bound at the actual degrees, and can therefore be transported to the larger public degrees by propositionTwoNumericalAlternatives_mono_degreeBounds.

theorem BGS.CorvajaZannier.generalPlaneCurvePropositionTwoCertificatesAboveElementaryRange_of_actualDegree (hactual : ∀ (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [inst : Field K] [Fintype K] [inst_2 : DecidableEq K] [CharP K p] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ), 0 < firstDegree → 0 < secondDegree → External.HasBidegreeAtMost f firstDegree secondDegree → ∀ (hcurve : External.IsCorvajaZannierPlaneCurve f), 0 < firstOrder → 0 < secondOrder → ¬p ∣ firstOrder → ¬p ∣ secondOrder → 12 * firstDegree * secondDegree < p → have hf := ⋯; PropositionTwoNumericalAlternatives (planeCurveTorsionLowerDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) firstOrder secondOrder) (planeCurveTorsionUpperDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) firstOrder secondOrder) p (2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f) ↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf ⋯ firstOrder secondOrder)) : GeneralPlaneCurvePropositionTwoCertificatesAboveElementaryRange

Pointwise Proposition 2 at the actual source-coordinate heights assembles the exact universal certificate proposition expected by the public endpoint.

This theorem is intentionally a composition boundary, not a replacement for the geometric proof: its hypothesis still asks for the actual-height Proposition 2 estimate for the exhaustive gcd divisor.