The numerical Corvaja--Zannier Theorem 2 bound

This file composes the floor-parameter proof of Theorem 4 with the corrected one-parameter optimization in NumericalOptimization. Its only substantive hypothesis is the ordinary Proposition 2 alternative for every admissible pair of natural parameters.

theorem BGS.CorvajaZannier.theoremTwo_maxBound_of_propositionTwo (a b chi p : ℕ) (G : ℝ) (ha : 0 < a) (hab : a ≤ b) (hchi : 0 < chi) (hp : 0 < p) (hGNonneg : 0 ≤ G) (hGTrivial : G ≤ ↑a) (hPropositionTwo : PropositionTwoNumericalAlternatives a b p chi G) : G ≤ max (3 * (2 * (↑a * ↑b * ↑chi)) ^ (1 / 3)) (12 * (↑a * ↑b) / ↑p)

The exact numerical maximum in Corvaja--Zannier Theorem 2, deduced from the numerical alternatives in Proposition 2.

The final optimization uses the corrected split recorded in theoremTwo_bound_of_theoremFour_bound; it does not use the incompatible parameter choices printed in the last paragraph of the source proof.