The parameterized numerical bound in Corvaja--Zannier Theorem 4

This file isolates the real and natural-number optimization in the proof of Corvaja--Zannier, JEMS 15 (2013), Theorem 4. The curve-theoretic content of their Proposition 2 is an ordinary proposition-valued hypothesis below. No function-field or valuation statement is assumed through a typeclass.

The source chooses

h = floor (t * (b^2 / (a * chi))^(1/3)) - 1 and k = floor (t * (a^2 / (b * chi))^(1/3)) - 1.

The proof below retains that choice and checks the small-k, degree- alternative, parameter-admissibility, and numerical-bound cases separately.

def BGS.CorvajaZannier.PropositionTwoParametersAreAdmissible (a b p h k : ℕ) : Prop

The natural parameters to which the numerical form of Corvaja--Zannier Proposition 2 applies. Positivity of h * k + h + k records that the denominator in Proposition 2 is meaningful.

Equations

• BGS.CorvajaZannier.PropositionTwoParametersAreAdmissible a b p h k = (0 < h * k + h + k ∧ a * h + b * k < p)

def BGS.CorvajaZannier.PropositionTwoNumericalAlternatives (a b p chi : ℕ) (G : ℝ) : Prop

The two alternatives supplied by the numerical part of Corvaja--Zannier Proposition 2.

Here a = deg(v), b = deg(u), chi is the Euler characteristic, and G is the gcd sum. This is deliberately an ordinary Prop, not a structure, class, or axiom.

Equations

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

theorem BGS.CorvajaZannier.theoremFour_parameterizedBound_of_propositionTwo (a b chi p : ℕ) (G t : ℝ) (ha : 0 < a) (hab : a ≤ b) (hchi : 0 < chi) (hp : 0 < p) (hGNonneg : 0 ≤ G) (hGTrivial : G ≤ ↑a) (ht : 0 < t) (hPropositionTwo : PropositionTwoNumericalAlternatives a b p chi G) (hSize : (↑a * ↑b) ^ 2 < (↑p + ↑a + ↑b) ^ 3 * ↑chi / (8 * t ^ 3)) : G ≤ (4 / t + t ^ 2 / 2) * (↑a * ↑b * ↑chi) ^ (1 / 3)

The floor-parameter optimization in Corvaja--Zannier Theorem 4.

The hypothesis hPropositionTwo is exactly the numerical alternative of Proposition 2, supplied for every admissible pair of natural parameters. All remaining hypotheses are elementary: positive natural degrees and Euler characteristic, positive characteristic and real parameter, a nonnegative gcd quantity, and its trivial upper bound by the smaller degree.