Summing the four local Corvaja--Zannier Wronskian cases

This module proves the exact finite-support divisor summation used in Corvaja--Zannier Proposition 2. Its hypotheses are the four already proved local lower bounds together with explicit principal-divisor, degree, and canonical-divisor identities. Thus it isolates the remaining geometric boundary: constructing these data from the places of the plane-curve function field.

theorem BGS.CorvajaZannier.globalWronskianInequality_of_placewiseBounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (S : Finset ι) (ordU ordV ordRho ordGrid ordW : ι → ℤ) (h k n sigma degreeU degreeV chi heightOutside : ℕ) (canonicalDegree : ℤ) (hUOutside : ∀ i ∉ S, ordU i = 0) (hGridOutside : ∀ i ∉ S, ordGrid i = 0) (hUSum : ∑ i : ι, ordU i = 0) (hGridSum : ∑ i : ι, ordGrid i = 0) (hDegreeV : ∑ i ∈ S with 0 < ordV i, ordV i = ↑degreeV) (hOutsideHeight : ∑ i : ι with i ∉ S ∧ ordRho i < 0, ordRho i = -↑heightOutside) (hCanonical : ∑ i : ι, ordW i = ↑sigma * canonicalDegree) (hEuler : canonicalDegree + ↑S.card ≤ ↑chi) (hRhoSupport : -(↑degreeU + ↑degreeV) ≤ ∑ i ∈ S, ordRho i) (hCaseI : ∀ i ∉ S, ordRho i < 0 → ↑n * ordRho i ≤ ordW i) (hCaseII : ∀ i ∉ S, 0 ≤ ordRho i → 0 ≤ ordW i) (hCaseIII : ∀ i ∈ S, 0 < ordV i → ↑(k * (k - 1) / 2) * ordU i + ↑(h * k) * ordV i + ↑k * ordRho i + ordGrid i - ↑sigma ≤ ordW i) (hCaseIV : ∀ i ∈ S, ordV i ≤ 0 → ↑(k * (k - 1) / 2) * ordU i + ↑k * ordRho i + ordGrid i - ↑sigma ≤ ordW i) : ↑(h * k) * ↑degreeV - ↑k * (↑degreeU + ↑degreeV) - ↑sigma * ↑chi ≤ ↑n * ↑heightOutside

Finite-support form of the summation step in the proof of Corvaja--Zannier Proposition 2.