Numerical assembly of plane-curve Proposition 2

This module isolates the final numerical use of the powered-image relation. The geometric Wronskian estimate is supplied pointwise; the remaining degree, index, and trivial-gcd bookkeeping is discharged here in both coordinate orientations.

theorem BGS.CorvajaZannier.planeCurvePropositionTwo_natural_of_auxiliaryBounds {K : Type u_1} [Field K] [DecidableEq K] [Finite K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n p Chi : ℕ) (hm : 0 < m) (hn : 0 < n) (hindex : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ Chi) (hauxiliary : ∀ (h k : ℕ), 0 < h → 0 < k → PropositionTwoParametersAreAdmissible (n * MvPolynomial.degreeOf 0 f) (m * MvPolynomial.degreeOf 1 f) p h k → ¬((transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree ≤ k ∧ (poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree ≤ h) → have hx := ⋯; ↑(finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 0 ^ m) (1 - planeCurveFunction f 1 ^ n)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(n * MvPolynomial.degreeOf 0 f) + ↑k / ↑(h * k + h + k) * ↑(m * MvPolynomial.degreeOf 1 f) + (↑(h * k + h + k) - 1) / 2 * ↑Chi) : PropositionTwoNumericalAlternatives (n * MvPolynomial.degreeOf 0 f) (m * MvPolynomial.degreeOf 1 f) p Chi ↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond m n)

Proposition 2 in the orientation (u,v)=(x^m,y^n).

theorem BGS.CorvajaZannier.planeCurvePropositionTwo_swapped_of_auxiliaryBounds {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n p Chi : ℕ) (hm : 0 < m) (hn : 0 < n) (hindex : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ Chi) (hauxiliary : ∀ (h k : ℕ), 0 < h → 0 < k → PropositionTwoParametersAreAdmissible (m * MvPolynomial.degreeOf 1 f) (n * MvPolynomial.degreeOf 0 f) p h k → ¬((poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree ≤ k ∧ (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree ≤ h) → have hx := ⋯; ↑(finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 1 ^ n) (1 - planeCurveFunction f 0 ^ m)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(m * MvPolynomial.degreeOf 1 f) + ↑k / ↑(h * k + h + k) * ↑(n * MvPolynomial.degreeOf 0 f) + (↑(h * k + h + k) - 1) / 2 * ↑Chi) : PropositionTwoNumericalAlternatives (m * MvPolynomial.degreeOf 1 f) (n * MvPolynomial.degreeOf 0 f) p Chi ↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond m n)

Proposition 2 in the swapped orientation (u,v)=(y^n,x^m).