The sharp Corvaja--Zannier bound after right-inversion pairing

The unconditional general plane-curve theorem specializes at bidegree (2, 2) to Euler-characteristic bound 8. Its two numerical branches are

• 12 * (leftOrder * rightOrder)^(1/3), and
• 48 * leftOrder * rightOrder / p.

Right-coordinate inversion pairs all solutions whose right coordinate is not two-torsion. Dividing the exact source bound by two therefore gives coefficients 6 and 24 for the nonparabolic left support.

No genus-one or Euler-characteristic-3 assertion is used here.

noncomputable def BGS.Markoff.pairedCorvajaZannierTraceUpperBound (p leftOrder rightOrder : ℕ) : ℝ

The exact coefficient improvement obtained by pairing the two right-coordinate inverses before taking the left support.

Equations

• BGS.Markoff.pairedCorvajaZannierTraceUpperBound p leftOrder rightOrder = max (6 * ↑(leftOrder * rightOrder) ^ (1 / 3)) (24 * (↑(leftOrder * rightOrder) / ↑p))

theorem BGS.Markoff.corvajaZannierCorollaryTwoNumericalBound_bidegree_two_euler_eight_eq_twice_paired (p leftOrder rightOrder : ℕ) : corvajaZannierCorollaryTwoNumericalBound p leftOrder rightOrder 2 2 8 = 2 * pairedCorvajaZannierTraceUpperBound p leftOrder rightOrder

At bidegree (2,2) and the unconditional Euler bound 8, the source-faithful Corvaja--Zannier right-hand side is exactly twice the paired bound. Keeping this equality explicit prevents the cube-root branch from being weakened to the older coefficient-48 envelope before pairing.

theorem BGS.Markoff.weightedTraceEquationNonparabolicLeftSupport_card_cast_le_pairedCorvajaZannier (p : ℕ) [Fact (Nat.Prime p)] (E : Type) [Field E] [Fintype E] [CharP E p] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) : ↑(weightedTraceEquationNonparabolicLeftSupport alpha beta H₁ H₂).card ≤ pairedCorvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥H₂)

The unconditional bidegree-(2,2), Euler-bound-8 Corvaja--Zannier theorem, combined with right inversion, gives the sharp nonparabolic left-support estimate

max (6 * (|H₁| |H₂|)^(1/3), 24 * |H₁| |H₂| / p).