Euler-seven paired escape over maximal candidate orders

The exact χ≤7 paired bound gives two sufficient inequalities:

• 189 * K^3 < currentOrder;
• 24 * K * currentOrder < p.

Here K is the number of divisibility-maximal candidate orders. The first coefficient is exact: it is the cube of the paired χ≤7 root coefficient.

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

A common χ≤7 paired bound for every candidate right order at most the current left order.

Equations

• BGS.Markoff.pairedEulerSevenCurrentOrderEnvelope p currentOrder = max (3 / 2 * (56 * ↑(currentOrder * currentOrder)) ^ (1 / 3)) (24 * (↑(currentOrder * currentOrder) / ↑p))

theorem BGS.Markoff.pairedEulerSevenTraceUpperBound_le_currentOrderEnvelope (p currentOrder d : ℕ) (hd : d ≤ currentOrder) : pairedEulerSevenCorvajaZannierTraceUpperBound p currentOrder d ≤ pairedEulerSevenCurrentOrderEnvelope p currentOrder

theorem BGS.Markoff.middleGameMaximalPairedEulerSevenSum_le_card_mul_envelope (p currentOrder : ℕ) (hp : 1 < p) : ∑ d ∈ middleGameMaximalOrders p currentOrder, pairedEulerSevenCorvajaZannierTraceUpperBound p currentOrder d ≤ ↑(middleGameMaximalOrders p currentOrder).card * pairedEulerSevenCurrentOrderEnvelope p currentOrder

theorem BGS.Markoff.orderCount_mul_pairedEulerSevenEnvelope_lt_currentOrder (p currentOrder orderCount : ℕ) (hcurrentOrder : 0 < currentOrder) (hcube : 189 * orderCount ^ 3 < currentOrder) (hlinear : 24 * orderCount * currentOrder < p) : ↑orderCount * pairedEulerSevenCurrentOrderEnvelope p currentOrder < ↑currentOrder

The exact coefficient-189 cube condition and the coefficient-24 linear condition make the whole maximal-order envelope smaller than the current order.

theorem BGS.Markoff.exists_left_element_escaping_nonparabolic_maximalOrders_eulerSeven (p : ℕ) [Fact (Nat.Prime p)] (E : Type u_2) [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 : 189 * (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

Finite nonparabolic escape over maximal candidate orders with the exact χ≤7 cube coefficient 189.