The middle-game bad-order union

The published middle game considers, for a left rotation group H₁, every possible right rotation order d ≤ |H₁| dividing p - 1 or p + 1. A power-saving estimate for the trace equation bounds the left elements that can meet a right subgroup of each such order. The divisor bound then makes the union of all those exceptional left elements smaller than H₁.

This file formalizes that finite combinatorial wiring. It deliberately does not postulate the Corvaja--Zannier estimate: the estimate appears below as an ordinary theorem hypothesis on the actual trace-equation solution finsets.

def BGS.Markoff.middleGameCandidateOrders (p currentOrder : ℕ) : Finset ℕ

Candidate right rotation orders in the middle game: divisors of p - 1 or p + 1 that do not exceed the current left rotation order.

Equations

• BGS.Markoff.middleGameCandidateOrders p currentOrder = {d ∈ (p - 1).divisors ∪ (p + 1).divisors | d ≤ currentOrder}

theorem BGS.Markoff.mem_middleGameCandidateOrders_iff {p currentOrder d : ℕ} : d ∈ middleGameCandidateOrders p currentOrder ↔ d ≤ currentOrder ∧ (d ∣ p - 1 ∧ p - 1 ≠ 0 ∨ d ∣ p + 1)

theorem BGS.Markoff.middleGameCandidateOrders_card_le (p currentOrder : ℕ) : (middleGameCandidateOrders p currentOrder).card ≤ (p - 1).divisors.card + (p + 1).divisors.card

There are no more candidate orders than the sum of the two divisor counts.

theorem BGS.Markoff.exists_threshold_middleGameCandidateOrders_card_le_two_mul_rpow {ε : ℝ} (hε : 0 < ε) : ∃ (threshold : ℕ), ∀ (p currentOrder : ℕ), threshold ≤ p → ↑(middleGameCandidateOrders p currentOrder).card ≤ 2 * ↑(p + 1) ^ ε

The proved subpolynomial divisor estimate controls both possible torus orders at once. This is the analytic input needed after taking the finite union over candidate right rotation orders.

noncomputable def BGS.Markoff.traceEquationLeftSupport {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ H₂ : Subgroup Eˣ) : Finset ↥H₁

Left elements of H₁ occurring in the trace equation with some element of H₂.

Equations

• BGS.Markoff.traceEquationLeftSupport sigma H₁ H₂ = Finset.image Prod.fst (BGS.Markoff.traceEquationSolutions sigma H₁ H₂)

@[simp]

theorem BGS.Markoff.mem_traceEquationLeftSupport_iff {E : Type u_1} [Field E] [Fintype E] {sigma : E} {H₁ H₂ : Subgroup Eˣ} {h₁ : ↥H₁} : h₁ ∈ traceEquationLeftSupport sigma H₁ H₂ ↔ ∃ (h₂ : ↥H₂), twistedUnitTrace sigma ↑h₁ = twistedUnitTrace 1 ↑h₂

theorem BGS.Markoff.traceEquationLeftSupport_card_le_solutions {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ H₂ : Subgroup Eˣ) : (traceEquationLeftSupport sigma H₁ H₂).card ≤ (traceEquationSolutions sigma H₁ H₂).card

Projection to the left coordinate cannot increase the number of trace-equation solutions.

def BGS.Markoff.corvajaZannierCorollaryTwoSafeCoefficient : ℕ

The safe coefficient obtained from Corvaja--Zannier, Corollary 2, after specializing its explicit constants to the middle-game trace curve.

Equations

• BGS.Markoff.corvajaZannierCorollaryTwoSafeCoefficient = 48

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

The numerical right-hand side of the Corvaja--Zannier trace estimate used in the published paper, with the source-justified safe coefficient from Corollary 2 kept explicit.

Equations

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

noncomputable def BGS.Markoff.badOrderTraceSupport {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ : Subgroup Eˣ) (orders : Finset ℕ) (rightSubgroup : ℕ → Subgroup Eˣ) : Finset ↥H₁

All left elements that meet at least one member of a supplied family of right subgroups.

Equations

• BGS.Markoff.badOrderTraceSupport sigma H₁ orders rightSubgroup = orders.biUnion fun (d : ℕ) => BGS.Markoff.traceEquationLeftSupport sigma H₁ (rightSubgroup d)

@[simp]

theorem BGS.Markoff.mem_badOrderTraceSupport_iff {E : Type u_1} [Field E] [Fintype E] {sigma : E} {H₁ : Subgroup Eˣ} {orders : Finset ℕ} {rightSubgroup : ℕ → Subgroup Eˣ} {h₁ : ↥H₁} : h₁ ∈ badOrderTraceSupport sigma H₁ orders rightSubgroup ↔ ∃ d ∈ orders, ∃ (h₂ : ↥(rightSubgroup d)), twistedUnitTrace sigma ↑h₁ = twistedUnitTrace 1 ↑h₂

theorem BGS.Markoff.badOrderTraceSupport_card_le {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ : Subgroup Eˣ) (orders : Finset ℕ) (rightSubgroup : ℕ → Subgroup Eˣ) (bound : ℕ) (hbound : ∀ d ∈ orders, (traceEquationSolutions sigma H₁ (rightSubgroup d)).card ≤ bound) : (badOrderTraceSupport sigma H₁ orders rightSubgroup).card ≤ orders.card * bound

A uniform bound for each trace-equation solution set gives the expected finite-union bound.

theorem BGS.Markoff.badOrderTraceSupport_card_cast_le_sum {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ : Subgroup Eˣ) (orders : Finset ℕ) (rightSubgroup : ℕ → Subgroup Eˣ) (bound : ℕ → ℝ) (hbound : ∀ d ∈ orders, ↑(traceEquationSolutions sigma H₁ (rightSubgroup d)).card ≤ bound d) : ↑(badOrderTraceSupport sigma H₁ orders rightSubgroup).card ≤ ∑ d ∈ orders, bound d

A nonuniform real-valued estimate for the individual trace equations sums over the candidate orders. This form accepts the quoted Corvaja--Zannier bound without rounding it to a natural number.

theorem BGS.Markoff.middleGameBadOrderTraceSupport_card_cast_le_corvajaZannierSum {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (sigma : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hCZ : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ↑(traceEquationSolutions sigma H₁ (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) d) : ↑(badOrderTraceSupport sigma H₁ (middleGameCandidateOrders p (Nat.card ↥H₁)) rightSubgroup).card ≤ ∑ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), corvajaZannierTraceUpperBound p (Nat.card ↥H₁) d

Direct wiring of the quoted Corvaja--Zannier estimate into the finite bad-order union. The deep estimate is the explicit hypothesis hCZ; this theorem proves only its combinatorial use.

theorem BGS.Markoff.middleGameBadOrderTraceSupport_card_le {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (sigma : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (bound : ℕ) (hbound : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), (traceEquationSolutions sigma H₁ (rightSubgroup d)).card ≤ bound) : (badOrderTraceSupport sigma H₁ (middleGameCandidateOrders p (Nat.card ↥H₁)) rightSubgroup).card ≤ ((p - 1).divisors.card + (p + 1).divisors.card) * bound

The published bad-order union bound, with the deep estimate exposed as a bound on each actual trace-equation solution set.

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

If the divisor-counted union is strictly smaller than H₁, some left rotation element cannot meet any right subgroup of candidate order. This is the exact pigeonhole step used to increase the maximal rotation order in the published middle game.