The source-faithful Corvaja--Zannier numerical specialization

Corvaja--Zannier, Corollary 2, gives a torsion-intersection bound for a curve of bidegree (d₁, d₂) and Euler characteristic χ. This file records its printed right-hand side and proves that the specialization (d₁, d₂, χ) = (2, 2, 4) is dominated by the coefficient-48 envelope used by the Markoff middle game.

This is only the numerical specialization. It does not postulate or prove the geometric torsion-intersection estimate.

noncomputable def BGS.Markoff.corvajaZannierCorollaryTwoNumericalBound (p leftOrder rightOrder firstDegree secondDegree : ℕ) (eulerCharacteristic : ℝ) : ℝ

The numerical right-hand side printed in Corvaja--Zannier, Corollary 2.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.Markoff.corvajaZannierCorollaryTwoNumericalBound_bidegree_two_euler_four_le (p leftOrder rightOrder : ℕ) : corvajaZannierCorollaryTwoNumericalBound p leftOrder rightOrder 2 2 4 ≤ corvajaZannierTraceUpperBound p leftOrder rightOrder

The exact (2,2) and Euler-characteristic-four specialization used by the Markoff middle game is dominated by the source-faithful coefficient 48.

theorem BGS.Markoff.corvajaZannierCorollaryTwoNumericalBound_bidegree_two_euler_eight_le (p leftOrder rightOrder : ℕ) : corvajaZannierCorollaryTwoNumericalBound p leftOrder rightOrder 2 2 8 ≤ corvajaZannierTraceUpperBound p leftOrder rightOrder

The degree-only Euler-characteristic bound χ ≤ 2 d₁ d₂ gives χ = 8 at bidegree (2,2). This slightly weaker but genuinely general specialization is still dominated by the coefficient-48 envelope used downstream.