Paired Corvaja--Zannier escape over maximal candidate orders

Right-coordinate inversion halves the unconditional bidegree-(2,2) Corvaja--Zannier estimate on the nonparabolic support. Combining that factor with the maximal-divisor cover gives two separate sufficient inequalities:

• (6 * K)^3 < currentOrder for the cube-root branch;
• 24 * K * currentOrder < p for the branch divided by p,

where K is the number of divisibility-maximal candidate orders.

No Euler-characteristic improvement is used in this module.

noncomputable def BGS.Markoff.pairedCorvajaZannierCurrentOrderEnvelope (p currentOrder : ℕ) : ℝ

A common paired Corvaja--Zannier bound for every right order at most the current left order.

Equations

• BGS.Markoff.pairedCorvajaZannierCurrentOrderEnvelope p currentOrder = max (6 * ↑(currentOrder * currentOrder) ^ (1 / 3)) (24 * (↑(currentOrder * currentOrder) / ↑p))

theorem BGS.Markoff.pairedCorvajaZannierTraceUpperBound_le_currentOrderEnvelope (p currentOrder d : ℕ) (hd : d ≤ currentOrder) : pairedCorvajaZannierTraceUpperBound p currentOrder d ≤ pairedCorvajaZannierCurrentOrderEnvelope p currentOrder

Replacing a candidate right order by the current left order enlarges both branches of the paired bound.

theorem BGS.Markoff.middleGameMaximalPairedCorvajaZannierSum_le_card_mul_envelope (p currentOrder : ℕ) (hp : 1 < p) : ∑ d ∈ middleGameMaximalOrders p currentOrder, pairedCorvajaZannierTraceUpperBound p currentOrder d ≤ ↑(middleGameMaximalOrders p currentOrder).card * pairedCorvajaZannierCurrentOrderEnvelope p currentOrder

The paired bounds over the maximal candidate orders are controlled by the number of those orders times the common current-order envelope.

theorem BGS.Markoff.orderCount_mul_pairedCorvajaZannierEnvelope_lt_currentOrder (p currentOrder orderCount : ℕ) (hcurrentOrder : 0 < currentOrder) (hcube : (6 * orderCount) ^ 3 < currentOrder) (hlinear : 24 * orderCount * currentOrder < p) : ↑orderCount * pairedCorvajaZannierCurrentOrderEnvelope p currentOrder < ↑currentOrder

The two coefficient-sensitive natural-number inequalities imply that the whole paired maximal-order envelope is smaller than the current order.

theorem BGS.Markoff.eulerSeven_bound_le_six_cube (count : ℕ) : 189 * count ^ 3 ≤ (6 * count) ^ 3

The stronger six-cube hypothesis supplies the Euler-seven order budget.

theorem BGS.Markoff.exists_left_element_escaping_nonparabolic_maximalOrders (p : ℕ) [Fact (Nat.Prime p)] (E : Type) [Field E] [Finite E] [CharP E p] (alpha beta : E) (Hleft : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameMaximalOrders p (Nat.card ↥Hleft), Nat.card ↥(rightSubgroup d) = d) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) (hcurrentOrder : 0 < Nat.card ↥Hleft) (hp : 1 < p) (hcube : (6 * (middleGameMaximalOrders p (Nat.card ↥Hleft)).card) ^ 3 < Nat.card ↥Hleft) (hlinear : 24 * (middleGameMaximalOrders p (Nat.card ↥Hleft)).card * Nat.card ↥Hleft < p) : ∃ (hleft : ↥Hleft), ∀ d ∈ middleGameMaximalOrders p (Nat.card ↥Hleft), ∀ (hright : ↥(rightSubgroup d)), ↑hright ^ 2 ≠ 1 → weightedSplitTorusTrace alpha beta ↑hleft ≠ splitTorusTrace ↑hright

The finite nonparabolic escape theorem over maximal candidate orders. The Corvaja--Zannier estimate is supplied by the in-repository general bidegree-(2,2) theorem and right-inversion pairing.