Exhaustive gcd divisor at the plane-curve endpoint

This module converts the exhaustive, degree-weighted gcd divisor into the certificate expected by the public Corvaja--Zannier endpoint. The sharp bidegree fiber count supplies the certificate's elementary upper bound, while the injection of rational torsion points into the exhaustive divisor lets us transfer Proposition 2 downward to the actual torsion-point cardinality.

theorem BGS.CorvajaZannier.planeCurvePropositionTwoCertificate_of_exhaustiveGcdWeightedDegree_and_bidegree {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) (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) ↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond firstOrder secondOrder)) : PlaneCurvePropositionTwoCertificate p K f firstDegree secondDegree firstOrder secondOrder

The exhaustive weighted gcd divisor supplies a Proposition 2 certificate.

The certificate uses the actual torsion-point cardinality as its gcd quantity. The bidegree estimate gives its trivial bound, and monotonicity transfers the Proposition 2 alternatives from the larger exhaustive weighted gcd degree.