Enlarging the degree data in Corvaja--Zannier Proposition 2

The actual coordinate degrees of a plane curve can be strictly smaller than the public bidegree bounds used by the final theorem. The degree alternative in Proposition 2 is not itself monotone in those bounds. Nevertheless, once the gcd quantity satisfies its trivial bound by the first actual degree, an actual degree alternative implies the numerical alternative for every larger pair of degrees: its Euler term already dominates the first degree.

This is the exact numerical bridge needed between a Proposition 2 proof at the curve's actual degrees and the public min/max degree convention.

theorem BGS.CorvajaZannier.propositionTwoNumericalAlternatives_mono_degreeBounds (a b A B p chi Chi : ℕ) (G : ℝ) (ha : 0 < a) (hb : 0 < b) (haA : a ≤ A) (hbB : b ≤ B) (hchi : chi ≤ Chi) (hChi : 0 < Chi) (hG : G ≤ ↑a) (hactual : PropositionTwoNumericalAlternatives a b p chi G) : PropositionTwoNumericalAlternatives A B p Chi G

Proposition 2 remains valid after enlarging both degrees and the Euler budget, provided the gcd quantity has the trivial bound by the first original degree.

The old degree alternative cannot in general be transported to the larger degrees. In that case both parameters are positive, and 2 * k <= h * k + h + k - 1; hence the new Euler term (whose Euler budget is positive) is at least k, and therefore at least the gcd quantity.

theorem BGS.CorvajaZannier.propositionTwoNumericalAlternatives_of_scaledAuxiliaryDegreeAlternative (a b d A B p Chi : ℕ) (G : ℝ) (ha : 0 < a) (hb : 0 < b) (hA : A ≤ d * a) (hdChi : d ≤ Chi) (hG : G ≤ ↑A) (hauxiliary : ∀ (h k : ℕ), PropositionTwoParametersAreAdmissible A B p h k → a ≤ k ∧ b ≤ h ∨ G ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑A + ↑k / ↑(h * k + h + k) * ↑B + (↑(h * k + h + k) - 1) / 2 * ↑Chi) : PropositionTwoNumericalAlternatives A B p Chi G

Convert an auxiliary degree alternative on a finite image curve into the numerical alternative at the source-curve heights.

Here a and b are the two image-curve degrees, A is the first source height, and d is the source-to-image degree. In the intended application A = d * a. The hypothesis d ≤ Chi is the precise extra input needed to absorb the image degree alternative into the source Euler term. Merely knowing a ≤ A is not enough.

The hypothesis hauxiliary deliberately keeps the numerical branch already at the source degrees A, B: this is the shape produced by the canonical Wronskian sum, whose divisor degrees are computed on the source curve.