The weighted middle-game trace equation

An arbitrary Markoff rotation orbit produces the equation

alpha * h₁ + beta / h₁ = h₂ + 1 / h₂,

with h₁ in the cyclic rotation subgroup. This module formalizes its finite solution sets, the elementary quadratic-fiber bound, and the complete bad-order union and pigeonhole reduction. The deep weighted Corvaja--Zannier estimate is an explicit theorem hypothesis; it is not encoded as an axiom, class, or structure field.

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

The possible left subgroup elements above one fixed right trace in the weighted equation.

Equations

• BGS.Markoff.weightedTraceEquationLeftFiber alpha beta H₁ h₂ = {h₁ : ↥H₁ | BGS.Markoff.weightedSplitTorusTrace alpha beta ↑h₁ = BGS.Markoff.splitTorusTrace h₂}

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

Solutions of the weighted middle-game trace equation inside two finite subgroups.

Equations

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

@[simp]

theorem BGS.Markoff.mem_weightedTraceEquationSolutions_iff {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {H₁ H₂ : Subgroup Eˣ} {h : ↥H₁ × ↥H₂} : h ∈ weightedTraceEquationSolutions alpha beta H₁ H₂ ↔ weightedSplitTorusTrace alpha beta ↑h.1 = splitTorusTrace ↑h.2

theorem BGS.Markoff.weightedSplitTorusTrace_eq_iff_twistedUnitTrace_eq {E : Type u_1} [Field E] (alpha beta trace : E) (h : Eˣ) (halpha : alpha ≠ 0) : weightedSplitTorusTrace alpha beta h = trace ↔ twistedUnitTrace (beta / alpha) h = trace / alpha

Dividing the weighted equation by its nonzero leading weight gives the monic twisted-trace equation used by the existing quadratic polynomial API.

theorem BGS.Markoff.weightedTraceEquationLeftFiber_card_le_two {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ : Subgroup Eˣ) (h₂ : Eˣ) (halpha : alpha ≠ 0) : (weightedTraceEquationLeftFiber alpha beta H₁ h₂).card ≤ 2

For a fixed right-hand trace, at most two left subgroup elements solve the weighted equation when the leading weight is nonzero.

theorem BGS.Markoff.weightedTraceEquationSolutions_card_le_two_mul_right {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) (halpha : alpha ≠ 0) : (weightedTraceEquationSolutions alpha beta H₁ H₂).card ≤ 2 * Nat.card ↥H₂

The elementary weighted estimate: every right subgroup element has at most two lifts.

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

Left elements occurring in the weighted trace equation with some right subgroup element.

Equations

• BGS.Markoff.weightedTraceEquationLeftSupport alpha beta H₁ H₂ = Finset.image Prod.fst (BGS.Markoff.weightedTraceEquationSolutions alpha beta H₁ H₂)

@[simp]

theorem BGS.Markoff.mem_weightedTraceEquationLeftSupport_iff {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {H₁ H₂ : Subgroup Eˣ} {h₁ : ↥H₁} : h₁ ∈ weightedTraceEquationLeftSupport alpha beta H₁ H₂ ↔ ∃ (h₂ : ↥H₂), weightedSplitTorusTrace alpha beta ↑h₁ = splitTorusTrace ↑h₂

theorem BGS.Markoff.weightedTraceEquationLeftSupport_card_le_solutions {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) : (weightedTraceEquationLeftSupport alpha beta H₁ H₂).card ≤ (weightedTraceEquationSolutions alpha beta H₁ H₂).card

Projection to the left coordinate cannot increase the weighted solution count.

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

Left elements meeting at least one member of an indexed family of right subgroups.

Equations

• BGS.Markoff.weightedBadOrderTraceSupport alpha beta H₁ orders rightSubgroup = orders.biUnion fun (d : ℕ) => BGS.Markoff.weightedTraceEquationLeftSupport alpha beta H₁ (rightSubgroup d)

@[simp]

theorem BGS.Markoff.mem_weightedBadOrderTraceSupport_iff {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {H₁ : Subgroup Eˣ} {orders : Finset ℕ} {rightSubgroup : ℕ → Subgroup Eˣ} {h₁ : ↥H₁} : h₁ ∈ weightedBadOrderTraceSupport alpha beta H₁ orders rightSubgroup ↔ ∃ d ∈ orders, ∃ (h₂ : ↥(rightSubgroup d)), weightedSplitTorusTrace alpha beta ↑h₁ = splitTorusTrace ↑h₂

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

A real-valued estimate for each weighted solution set sums over an arbitrary finite family of candidate right orders.

theorem BGS.Markoff.weightedBadOrderTraceSupport_card_le {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ : Subgroup Eˣ) (orders : Finset ℕ) (rightSubgroup : ℕ → Subgroup Eˣ) (bound : ℕ) (hbound : ∀ d ∈ orders, (weightedTraceEquationSolutions alpha beta H₁ (rightSubgroup d)).card ≤ bound) : (weightedBadOrderTraceSupport alpha beta H₁ orders rightSubgroup).card ≤ orders.card * bound

A uniform natural-valued bound gives the corresponding weighted finite-union bound.

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

The published divisor-counted natural-valued weighted bad-order bound.

theorem BGS.Markoff.middleGameWeightedBadOrderTraceSupport_card_cast_le_corvajaZannierSum {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (alpha beta : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), Nat.card ↥(rightSubgroup d) = d) (hCZ : alpha * beta ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ↑(weightedTraceEquationSolutions alpha beta H₁ (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥(rightSubgroup d))) (hnondegenerate : alpha * beta ≠ 1) : ↑(weightedBadOrderTraceSupport alpha beta H₁ (middleGameCandidateOrders p (Nat.card ↥H₁)) rightSubgroup).card ≤ ∑ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), corvajaZannierTraceUpperBound p (Nat.card ↥H₁) d

The weighted Corvaja--Zannier estimate, when supplied for each actual right subgroup, sums to the same numerical expression as in the normalized equation. The essential nondegeneracy alpha * beta != 1 is an explicit premise of the estimate.

theorem BGS.Markoff.middleGameWeightedBadOrderTraceSupport_card_cast_le_divisorEnvelope {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (alpha beta : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), Nat.card ↥(rightSubgroup d) = d) (hCZ : alpha * beta ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ↑(weightedTraceEquationSolutions alpha beta H₁ (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥(rightSubgroup d))) (hnondegenerate : alpha * beta ≠ 1) : ↑(weightedBadOrderTraceSupport alpha beta H₁ (middleGameCandidateOrders p (Nat.card ↥H₁)) rightSubgroup).card ≤ ↑((p - 1).divisors.card + (p + 1).divisors.card) * corvajaZannierCurrentOrderEnvelope p (Nat.card ↥H₁)

Combining the weighted Corvaja--Zannier estimate with the common current-order envelope.

theorem BGS.Markoff.exists_left_element_escaping_weightedCandidateOrders {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (alpha beta : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (bound : ℕ) (hbound : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), (weightedTraceEquationSolutions alpha beta 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)), weightedSplitTorusTrace alpha beta ↑h₁ ≠ splitTorusTrace ↑h₂

If the divisor-counted weighted bad set is smaller than the left subgroup, one left element avoids every candidate right-order trace.

theorem BGS.Markoff.exists_left_element_escaping_of_weightedCorvajaZannierEstimate_and_sizeBounds {E : Type u_1} [Field E] [Fintype E] (p : ℕ) (alpha beta : E) (H₁ : Subgroup Eˣ) (rightSubgroup : ℕ → Subgroup Eˣ) (hrightOrder : ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), Nat.card ↥(rightSubgroup d) = d) (hCZ : alpha * beta ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (Nat.card ↥H₁), ↑(weightedTraceEquationSolutions alpha beta H₁ (rightSubgroup d)).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥(rightSubgroup d))) (hnondegenerate : alpha * beta ≠ 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)), weightedSplitTorusTrace alpha beta ↑h₁ ≠ splitTorusTrace ↑h₂

The complete finite weighted Corvaja--Zannier escape reduction. The only deep premise is hCZ; the remaining hypotheses are actual subgroup cardinalities and the two explicit size inequalities controlling the cube-root and 1 / p terms.