Finite unions of nonparabolic trace supports

The middle game only needs to exclude right traces coming from nonparabolic coordinates: a parabolic target already lies above the endgame threshold. This module packages that logical split before any numerical estimate is inserted. In particular, the inversion-pairing factor can be applied to each right subgroup without counting its two fixed points.

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

Left elements meeting a nonparabolic point in one of a finite family of right subgroups.

Equations

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

@[simp]

theorem BGS.Markoff.mem_weightedNonparabolicBadOrderTraceSupport_iff {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {Hleft : Subgroup Eˣ} {orders : Finset ℕ} {rightSubgroup : ℕ → Subgroup Eˣ} {hleft : ↥Hleft} : hleft ∈ weightedNonparabolicBadOrderTraceSupport alpha beta Hleft orders rightSubgroup ↔ ∃ d ∈ orders, ∃ (hright : ↥(rightSubgroup d)), weightedSplitTorusTrace alpha beta ↑hleft = splitTorusTrace ↑hright ∧ ↑hright ^ 2 ≠ 1

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

Bounds on the individual nonparabolic left supports sum over an arbitrary finite family of candidate right subgroups.

theorem BGS.Markoff.exists_left_element_escaping_nonparabolic_orders_of_sum_bound {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (Hleft : Subgroup Eˣ) (orders : Finset ℕ) (rightSubgroup : ℕ → Subgroup Eˣ) (bound : ℕ → ℝ) (hbound : ∀ d ∈ orders, ↑(weightedTraceEquationNonparabolicLeftSupport alpha beta Hleft (rightSubgroup d)).card ≤ bound d) (hsmall : ∑ d ∈ orders, bound d < ↑(Nat.card ↥Hleft)) : ∃ (hleft : ↥Hleft), ∀ d ∈ orders, ∀ (hright : ↥(rightSubgroup d)), ↑hright ^ 2 ≠ 1 → weightedSplitTorusTrace alpha beta ↑hleft ≠ splitTorusTrace ↑hright

If the summed nonparabolic support bound is smaller than the left subgroup, one left element avoids every nonparabolic candidate trace.