Canonical placewise bounds imply the exhaustive gcd estimate

This is the global composition boundary for Corvaja--Zannier Proposition 2. It fixes the canonical different divisor and the direct zero-and-pole exceptional set, discharges all support bookkeeping, performs the exhaustive weighted place sum, and then converts the resulting Wronskian inequality into the numerical gcd estimate.

theorem BGS.CorvajaZannier.finiteExtensionGcdBound_of_canonicalPlacewiseBounds (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (u v W : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) (hW : W ≠ 0) (h k : ℕ) (hn : 0 < h * k + h + k) (chi : ℕ) (hEuler : finiteExtensionDivisorDegree K L (finiteExtensionCanonicalDifferentDivisor K L ⋯) + ∑ P ∈ propositionTwoExceptionalPlaces K L u v, ↑(finiteExtensionPlaceDegree K L P) ≤ ↑chi) (hCaseI : ∀ P ∉ propositionTwoExceptionalPlaces K L u v, (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) P < 0 → ↑(h * k + h + k) * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) P ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) P + (finiteExtensionPrincipalDivisor K L W) P) (hCaseII : ∀ P ∉ propositionTwoExceptionalPlaces K L u v, 0 ≤ (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) P → 0 ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) P + (finiteExtensionPrincipalDivisor K L W) P) (hCaseIII : ∀ P ∈ propositionTwoExceptionalPlaces K L u v, 0 < (finiteExtensionPrincipalDivisor K L v) P → ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) P + ↑(h * k) * (finiteExtensionPrincipalDivisor K L v) P + ↑k * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) P + (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) P - ↑((h * k + h + k).choose 2) ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) P + (finiteExtensionPrincipalDivisor K L W) P) (hCaseIV : ∀ P ∈ propositionTwoExceptionalPlaces K L u v, (finiteExtensionPrincipalDivisor K L v) P ≤ 0 → ↑(k * (k - 1) / 2) * (finiteExtensionPrincipalDivisor K L u) P + ↑k * (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) P + (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) P - ↑((h * k + h + k).choose 2) ≤ ↑((h * k + h + k).choose 2) * (finiteExtensionCanonicalDifferentDivisor K L ⋯) P + (finiteExtensionPrincipalDivisor K L W) P) : ↑(finiteExtensionGcdWeightedDegree K L (1 - u) (1 - v)) ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * ↑(finiteExtensionPositiveDegree K L v) + ↑k / ↑(h * k + h + k) * ↑(finiteExtensionPositiveDegree K L u) + (↑(h * k + h + k) - 1) / 2 * ↑chi

The four canonical local estimates, together with the logarithmic Euler degree bound, imply the exact exhaustive weighted gcd bound of Proposition 2.