The Corvaja--Zannier middle-game escape step

This module connects the published Corvaja--Zannier estimate to the already formalized bad-order union. The deep estimate remains an explicit hypothesis about the actual trace-equation solution sets. Two details that are easy to lose in an abstract union bound are kept in the statement:

• sigma != 1, as required in equation (62) of the published paper;
• the subgroup indexed by d must actually have cardinality d.

The theorem below reduces the paper-specific order-increase step to one visible numerical inequality. It does not postulate the Corvaja--Zannier theorem.

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

A common Corvaja--Zannier bound for every candidate order not exceeding the current order.

Equations

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

theorem BGS.Markoff.corvajaZannierTraceUpperBound_le_currentOrderEnvelope (p currentOrder d : ℕ) (hd : d ≤ currentOrder) : corvajaZannierTraceUpperBound p currentOrder d ≤ corvajaZannierCurrentOrderEnvelope p currentOrder

Replacing a candidate right order by the current left order only enlarges the quoted Corvaja--Zannier bound.

theorem BGS.Markoff.middleGameCorvajaZannierSum_le_divisorCount_mul_envelope (p currentOrder : ℕ) : ∑ d ∈ middleGameCandidateOrders p currentOrder, corvajaZannierTraceUpperBound p currentOrder d ≤ ↑((p - 1).divisors.card + (p + 1).divisors.card) * corvajaZannierCurrentOrderEnvelope p currentOrder

The summed Corvaja--Zannier expression is bounded by the divisor count times the common current-order envelope.

theorem BGS.Markoff.divisorCount_mul_corvajaZannierEnvelope_lt_currentOrder (p currentOrder : ℕ) (hcurrentOrder : 0 < currentOrder) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < currentOrder) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * currentOrder < p) : ↑((p - 1).divisors.card + (p + 1).divisors.card) * corvajaZannierCurrentOrderEnvelope p currentOrder < ↑currentOrder

Two elementary natural-number inequalities imply that the entire divisor-counted Corvaja--Zannier envelope is smaller than the current order. Writing D = tau(p - 1) + tau(p + 1), these are exactly

• (48 D)^3 < currentOrder for the cube-root term, and
• 48 D * currentOrder < p for the term divided by p.

Thus the remaining asymptotic work is reduced to the proved subpolynomial divisor bound and the chosen middle-game range for currentOrder.

theorem BGS.Markoff.exists_left_element_escaping_of_corvajaZannierEstimate {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (sigma : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), Nat.card ↥(rightSubgroup d) = d) (hCZ : sigma ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ↑(traceEquationSolutions sigma H₁ (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥(rightSubgroup d))) (hsigma : sigma ≠ 1) (hsmall : ↑((p - 1).divisors.card + (p + 1).divisors.card) * corvajaZannierCurrentOrderEnvelope p (Nat.card ↥H₁) < ↑(Nat.card ↥H₁)) : ∃ (h₁ : ↥H₁), ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ∀ (h₂ : ↥(rightSubgroup d)), twistedUnitTrace sigma ↑h₁ ≠ twistedUnitTrace 1 ↑h₂

The paper's middle-game pigeonhole step, now fed by the real-valued Corvaja--Zannier estimate. The estimate is stated using the actual subgroup cardinality, and hrightOrder performs the indispensable identification of that cardinality with the divisor d indexing the union.

The sole remaining numerical premise is exactly the inequality needed after summing over all candidate orders.

theorem BGS.Markoff.exists_left_element_escaping_of_corvajaZannierEstimate_and_sizeBounds {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (sigma : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), Nat.card ↥(rightSubgroup d) = d) (hCZ : sigma ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ↑(traceEquationSolutions sigma H₁ (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥(rightSubgroup d))) (hsigma : sigma ≠ 1) (hcurrentOrder : 0 < Nat.card ↥H₁) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < Nat.card ↥H₁) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * Nat.card ↥H₁ < p) : ∃ (h₁ : ↥H₁), ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ∀ (h₂ : ↥(rightSubgroup d)), twistedUnitTrace sigma ↑h₁ ≠ twistedUnitTrace 1 ↑h₂

A fully finite version of the paper's Corvaja--Zannier order-escape step. Apart from the deep estimate itself, its hypotheses are natural-number cardinality and size inequalities.