Numerical optimization in Corvaja--Zannier Theorem 2

The last step in the proof of Corvaja--Zannier's Theorem 2 optimizes the parameterized estimate of their Theorem 4. The split printed in the paper is not compatible with the strict hypothesis of Theorem 4: if

Q = p^3 * chi / (degreeU * degreeV)^2,

then the fixed choice t = 4^(1/3) requires Q >= 32, not Q >= 4. For Q < 32, the valid choice is t = Q^(1/3) / 2. These two choices give exactly the maximum displayed in Theorem 2.

This file isolates that corrected real-arithmetic argument. Its theorem takes the parameterized Theorem-4 estimate as an ordinary hypothesis, so it can be applied directly once the curve-theoretic part of Theorem 4 is formalized.

noncomputable def BGS.CorvajaZannier.optimizationRatio (p degreeProduct eulerCharacteristic : ℝ) : ℝ

The dimensionless ratio used in the final optimization of Corvaja--Zannier Theorem 2.

Equations

• BGS.CorvajaZannier.optimizationRatio p degreeProduct eulerCharacteristic = p ^ 3 * eulerCharacteristic / degreeProduct ^ 2

theorem BGS.CorvajaZannier.theoremTwo_bound_of_theoremFour_bound (p degreeU degreeV eulerCharacteristic gcdValue : ℝ) (hp : 0 < p) (hdegreeU : 0 < degreeU) (hdegreeV : 0 < degreeV) (hEuler : 0 < eulerCharacteristic) (hTheoremFour : ∀ (t : ℝ), 0 < t → 8 * t ^ 3 * (degreeU * degreeV) ^ 2 < (p + degreeU + degreeV) ^ 3 * eulerCharacteristic → gcdValue ≤ (4 / t + t ^ 2 / 2) * (degreeU * degreeV * eulerCharacteristic) ^ (1 / 3)) : gcdValue ≤ max (3 * (2 * (degreeU * degreeV * eulerCharacteristic)) ^ (1 / 3)) (12 * (degreeU * degreeV) / p)

The corrected numerical deduction of Corvaja--Zannier Theorem 2 from the parameterized estimate in Theorem 4.

The hypothesis hTheoremFour is precisely the real-valued part of Theorem 4: for every positive parameter satisfying its strict size condition, it supplies the parameterized gcd bound. The proof uses the valid split Q ≥ 32 and Q < 32; it does not use the erroneous Q = 4 split printed in the final paragraph of the paper.