Corvaja--Zannier escape over maximal candidate orders

The published middle-game union runs over every candidate divisor of p - 1 or p + 1. Divisibility monotonicity of roots-of-unity subgroups shows that it is enough to run the union over middleGameMaximalOrders: every smaller candidate subgroup is contained in one of these maximal subgroups.

This file performs the finite union and its numerical reduction. The deep Corvaja--Zannier estimate remains an explicit hypothesis about the actual weighted trace-equation solution sets.

theorem BGS.Markoff.middleGameMaximalCorvajaZannierSum_le_card_mul_envelope (p currentOrder : ℕ) (hp : 1 < p) : ∑ d ∈ middleGameMaximalOrders p currentOrder, corvajaZannierTraceUpperBound p currentOrder d ≤ ↑(middleGameMaximalOrders p currentOrder).card * corvajaZannierCurrentOrderEnvelope p currentOrder

The Corvaja--Zannier sum over maximal candidate orders is bounded by the number of those orders times the common current-order envelope.

theorem BGS.Markoff.orderCount_mul_corvajaZannierEnvelope_lt_currentOrder (p currentOrder orderCount : ℕ) (hcurrentOrder : 0 < currentOrder) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * orderCount) ^ 3 < currentOrder) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * orderCount * currentOrder < p) : ↑orderCount * corvajaZannierCurrentOrderEnvelope p currentOrder < ↑currentOrder

A generic version of the two elementary inequalities controlling the Corvaja--Zannier envelope. It is deliberately parameterized by the number of orders in the union, so the maximal-divisor cover can use its much smaller cardinality.

Writing K for orderCount, the hypotheses are

• (48 K)^3 < currentOrder;
• 48 K * currentOrder < p.

theorem BGS.Markoff.exists_left_element_escaping_of_weightedCorvajaZannierEstimate_maximalOrders {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (alpha beta : E) (Hleft : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameMaximalOrders p (Nat.card ↥Hleft), Nat.card ↥(rightSubgroup d) = d) (hCZ : alpha * beta ≠ 1 → ∀ d ∈ middleGameMaximalOrders p (Nat.card ↥Hleft), ↑(weightedTraceEquationSolutions alpha beta Hleft (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥Hleft) (Nat.card ↥(rightSubgroup d))) (hnondegenerate : alpha * beta ≠ 1) (hcurrentOrder : 0 < Nat.card ↥Hleft) (hp : 1 < p) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * (middleGameMaximalOrders p (Nat.card ↥Hleft)).card) ^ 3 < Nat.card ↥Hleft) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * (middleGameMaximalOrders p (Nat.card ↥Hleft)).card * Nat.card ↥Hleft < p) : ∃ (hleft : ↥Hleft), ∀ d ∈ middleGameMaximalOrders p (Nat.card ↥Hleft), ∀ (hright : ↥(rightSubgroup d)), weightedSplitTorusTrace alpha beta ↑hleft ≠ splitTorusTrace ↑hright

The finite weighted Corvaja--Zannier escape step over maximal candidate orders only.