Elementary counts for the giant-orbit assembly

This file isolates the two elementary finite counts omitted from the paper's final assembly:

• fixing the first two coordinates of a Markoff point leaves at most two choices for the third;
• traces coming from elements of bounded order in a finite cyclic group have a deliberately crude quadratic cardinality bound.

The cyclicity hypothesis in the second count is essential: the analogous statement for arbitrary finite groups is false (an elementary abelian 2-group can have more than two elements of order two). The split and norm-one tori to which this count will eventually be applied are cyclic.

noncomputable def BGS.Markoff.thirdCoordinatePolynomial {F : Type u_1} [Field F] (a b : F) : Polynomial F

The monic quadratic obtained from the Markoff equation after fixing its first two coordinates.

Equations

• BGS.Markoff.thirdCoordinatePolynomial a b = Polynomial.X ^ 2 - Polynomial.C (3 * a * b) * Polynomial.X + Polynomial.C (a ^ 2 + b ^ 2)

@[simp]

theorem BGS.Markoff.thirdCoordinatePolynomial_eval {F : Type u_1} [Field F] (a b c : F) : Polynomial.eval c (thirdCoordinatePolynomial a b) = markoffPolynomial { x1 := a, x2 := b, x3 := c }

theorem BGS.Markoff.thirdCoordinatePolynomial_monic {F : Type u_1} [Field F] (a b : F) : (thirdCoordinatePolynomial a b).Monic

@[simp]

theorem BGS.Markoff.thirdCoordinatePolynomial_natDegree {F : Type u_1} [Field F] (a b : F) : (thirdCoordinatePolynomial a b).natDegree = 2

noncomputable def BGS.Markoff.thirdCoordinatesOnMarkoffSurface {F : Type u_1} [Field F] [Fintype F] (a b : F) : Finset F

The possible third coordinates of Markoff points whose first two coordinates are a,b.

Equations

• BGS.Markoff.thirdCoordinatesOnMarkoffSurface a b = {c : F | BGS.Markoff.IsMarkoff { x1 := a, x2 := b, x3 := c }}

theorem BGS.Markoff.thirdCoordinatesOnMarkoffSurface_card_le_two {F : Type u_1} [Field F] [Fintype F] (a b : F) : (thirdCoordinatesOnMarkoffSurface a b).card ≤ 2

noncomputable def BGS.Markoff.markoffPointsWithFirstTwoCoordinates {F : Type u_1} [Field F] [Fintype F] (a b : F) : Finset (Point F)

Markoff-surface points, represented in the project's ambient Point type, with prescribed first and second coordinates.

Equations

• BGS.Markoff.markoffPointsWithFirstTwoCoordinates a b = Finset.image (fun (c : F) => { x1 := a, x2 := b, x3 := c }) (BGS.Markoff.thirdCoordinatesOnMarkoffSurface a b)

theorem BGS.Markoff.mem_markoffPointsWithFirstTwoCoordinates_iff {F : Type u_1} [Field F] [Fintype F] {a b : F} {x : Point F} : x ∈ markoffPointsWithFirstTwoCoordinates a b ↔ IsMarkoff x ∧ x.x1 = a ∧ x.x2 = b

theorem BGS.Markoff.markoffPointsWithFirstTwoCoordinates_card_le_two {F : Type u_1} [Field F] [Fintype F] (a b : F) : (markoffPointsWithFirstTwoCoordinates a b).card ≤ 2

noncomputable def BGS.Markoff.elementsOfOrderLessThan (G : Type u_3) [Group G] [Fintype G] (bound : ℕ) : Finset G

Elements of a finite group whose multiplicative order is strictly below bound.

Equations

• BGS.Markoff.elementsOfOrderLessThan G bound = {g : G | orderOf g < bound}

noncomputable def BGS.Markoff.boundedOrderTraceSet {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq T] (trace : G → T) (bound : ℕ) : Finset T

Values of a trace-like map on group elements whose multiplicative order is below bound.

Equations

• BGS.Markoff.boundedOrderTraceSet trace bound = Finset.image trace (BGS.Markoff.elementsOfOrderLessThan G bound)

theorem BGS.Markoff.elementsOfOrderLessThan_card_le_sum_range {G : Type u_1} [Group G] [Fintype G] [IsCyclic G] (bound : ℕ) : (elementsOfOrderLessThan G bound).card ≤ ∑ d ∈ Finset.range bound, d

theorem BGS.Markoff.elementsOfOrderLessThan_card_le_pred_mul_card_divisors {G : Type u_1} [Group G] [Fintype G] [IsCyclic G] (bound : ℕ) : (elementsOfOrderLessThan G bound).card ≤ (bound - 1) * (Fintype.card G).divisors.card

A divisor-sensitive version of the bounded-order count. Only orders dividing the group cardinality can occur, and each such order contributes fewer than bound elements.

theorem BGS.Markoff.elementsOfOrderLessThan_card_le_bound_mul_card_divisors {G : Type u_1} [Group G] [Fintype G] [IsCyclic G] (bound : ℕ) : (elementsOfOrderLessThan G bound).card ≤ bound * (Fintype.card G).divisors.card

theorem BGS.Markoff.boundedOrderTraceSet_card_le_sum_range {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) : (boundedOrderTraceSet trace bound).card ≤ ∑ d ∈ Finset.range bound, d

theorem BGS.Markoff.boundedOrderTraceSet_card_le_bound_mul_card_divisors {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) : (boundedOrderTraceSet trace bound).card ≤ bound * (Fintype.card G).divisors.card

theorem BGS.Markoff.boundedOrderTraceSet_card_le_pred_mul_card_divisors {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) : (boundedOrderTraceSet trace bound).card ≤ (bound - 1) * (Fintype.card G).divisors.card

theorem BGS.Markoff.sum_orders_below_bound_le_bound_sq (bound : ℕ) : ∑ d ∈ Finset.range bound, d ≤ bound ^ 2

theorem BGS.Markoff.boundedOrderTraceSet_card_le_bound_sq {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) : (boundedOrderTraceSet trace bound).card ≤ bound ^ 2

noncomputable def BGS.Markoff.lowOrderTraceSet {Gsplit : Type u_3} {Gnonsplit : Type u_4} {T : Type u_5} [Group Gsplit] [Fintype Gsplit] [Group Gnonsplit] [Fintype Gnonsplit] [DecidableEq T] (parabolic : Finset T) (splitTrace : Gsplit → T) (nonsplitTrace : Gnonsplit → T) (bound : ℕ) : Finset T

The union of bounded-order trace values from the split and norm-one tori, together with a finite set of exceptional (parabolic) trace values.

Equations

• BGS.Markoff.lowOrderTraceSet parabolic splitTrace nonsplitTrace bound = parabolic ∪ BGS.Markoff.boundedOrderTraceSet splitTrace bound ∪ BGS.Markoff.boundedOrderTraceSet nonsplitTrace bound

theorem BGS.Markoff.lowOrderTraceSet_card_le {Gsplit : Type u_3} {Gnonsplit : Type u_4} {T : Type u_5} [Group Gsplit] [Fintype Gsplit] [IsCyclic Gsplit] [Group Gnonsplit] [Fintype Gnonsplit] [IsCyclic Gnonsplit] [DecidableEq T] (parabolic : Finset T) (splitTrace : Gsplit → T) (nonsplitTrace : Gnonsplit → T) (bound : ℕ) : (lowOrderTraceSet parabolic splitTrace nonsplitTrace bound).card ≤ parabolic.card + 2 * ∑ d ∈ Finset.range bound, d

theorem BGS.Markoff.lowOrderTraceSet_card_le_parabolic_add_two_mul_bound_sq {Gsplit : Type u_3} {Gnonsplit : Type u_4} {T : Type u_5} [Group Gsplit] [Fintype Gsplit] [IsCyclic Gsplit] [Group Gnonsplit] [Fintype Gnonsplit] [IsCyclic Gnonsplit] [DecidableEq T] (parabolic : Finset T) (splitTrace : Gsplit → T) (nonsplitTrace : Gnonsplit → T) (bound : ℕ) : (lowOrderTraceSet parabolic splitTrace nonsplitTrace bound).card ≤ parabolic.card + 2 * bound ^ 2

theorem BGS.Markoff.lowOrderTraceSet_card_le_parabolic_add_pred_mul_divisor_cards {Gsplit : Type u_3} {Gnonsplit : Type u_4} {T : Type u_5} [Group Gsplit] [Fintype Gsplit] [IsCyclic Gsplit] [Group Gnonsplit] [Fintype Gnonsplit] [IsCyclic Gnonsplit] [DecidableEq T] (parabolic : Finset T) (splitTrace : Gsplit → T) (nonsplitTrace : Gnonsplit → T) (bound : ℕ) : (lowOrderTraceSet parabolic splitTrace nonsplitTrace bound).card ≤ parabolic.card + (bound - 1) * ((Fintype.card Gsplit).divisors.card + (Fintype.card Gnonsplit).divisors.card)

A divisor-sensitive count for the union of the two bounded-order trace sets.

theorem BGS.Markoff.lowOrderTraceSet_card_le_parabolic_add_bound_mul_divisor_cards {Gsplit : Type u_3} {Gnonsplit : Type u_4} {T : Type u_5} [Group Gsplit] [Fintype Gsplit] [IsCyclic Gsplit] [Group Gnonsplit] [Fintype Gnonsplit] [IsCyclic Gnonsplit] [DecidableEq T] (parabolic : Finset T) (splitTrace : Gsplit → T) (nonsplitTrace : Gnonsplit → T) (bound : ℕ) : (lowOrderTraceSet parabolic splitTrace nonsplitTrace bound).card ≤ parabolic.card + bound * ((Fintype.card Gsplit).divisors.card + (Fintype.card Gnonsplit).divisors.card)