Global Wronskian summation for Corvaja--Zannier Proposition 2

This file formalizes the exact real-arithmetic passage from the global Wronskian divisor inequality to the numerical alternatives consumed by the proved optimization stage. The remaining geometric theorem must supply the displayed summed Wronskian inequality; it is not assumed as an axiom or hidden in a typeclass.

theorem BGS.CorvajaZannier.gcdBound_of_globalWronskianInequality (a b chi G heightOutside : ℝ) (h k : ℕ) (hn : 0 < h * k + h + k) (hGHeight : G ≤ a - heightOutside) (hWronskian : ↑(h * k) * a - ↑k * (a + b) - ↑(h * k + h + k) * (↑(h * k + h + k) - 1) / 2 * chi ≤ ↑(h * k + h + k) * heightOutside) : G ≤ ↑(h + 2 * k) / ↑(h * k + h + k) * a + ↑k / ↑(h * k + h + k) * b + (↑(h * k + h + k) - 1) / 2 * chi

The real-arithmetic passage from the global Wronskian inequality to the displayed gcd bound in Corvaja--Zannier Proposition 2.

theorem BGS.CorvajaZannier.propositionTwoNumericalAlternatives_of_globalWronskianInequality (a b p chi : ℕ) (G heightOutside : ℝ) (hGHeight : G ≤ ↑a - heightOutside) (hWronskian : ∀ (h k : ℕ), PropositionTwoParametersAreAdmissible a b p h k → ¬(a ≤ k ∧ b ≤ h) → ↑(h * k) * ↑a - ↑k * (↑a + ↑b) - ↑(h * k + h + k) * (↑(h * k + h + k) - 1) / 2 * ↑chi ≤ ↑(h * k + h + k) * heightOutside) : PropositionTwoNumericalAlternatives a b p chi G

Proposition 2's numerical alternatives follow once the single outside height comparison and the summed Wronskian inequality have been established for every admissible parameter pair outside the degree alternative.