Fixed-point-free maximal-divisor trace pairing

After restricting to eigenvalues with x^2 ≠ 1, inversion has no fixed points. Every trace fiber therefore contains a genuine inverse pair, with no additive exceptional term. Applying this on each maximal-divisor piece gives

2 * |non-two-torsion bounded traces| ≤ (bound - 1) * M.

theorem BGS.Markoff.two_mul_card_image_le_card_of_inv_invariant_of_no_fixed {G : Type u_1} {T : Type u_2} [Group G] [DecidableEq T] (s : Finset G) (f : G → T) (hsinv : ∀ x ∈ s, x⁻¹ ∈ s) (hfinv : ∀ (x : G), f x⁻¹ = f x) (hnofixed : ∀ x ∈ s, x⁻¹ ≠ x) : 2 * (Finset.image f s).card ≤ s.card

An inversion-invariant map has at most half as many values as inputs when inversion has no fixed point on the source.

def BGS.Markoff.nonTwoTorsionElementsWithPowOne {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (m : ℕ) : Finset G

Elements of a roots-of-unity piece that are not fixed by inversion.

Equations

• BGS.Markoff.nonTwoTorsionElementsWithPowOne m = {x ∈ BGS.NumberTheory.elementsWithPowOne G m | x ^ 2 ≠ 1}

@[simp]

theorem BGS.Markoff.mem_nonTwoTorsionElementsWithPowOne_iff {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {m : ℕ} {x : G} : x ∈ nonTwoTorsionElementsWithPowOne m ↔ x ^ m = 1 ∧ x ^ 2 ≠ 1

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

Bounded-order trace values represented by non-two-torsion eigenvalues.

Equations

• BGS.Markoff.nonTwoTorsionBoundedOrderTraceSet trace bound = Finset.image trace {x : G | orderOf x < bound ∧ x ^ 2 ≠ 1}

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

The maximal-divisor cover built only from non-two-torsion roots.

Equations

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

theorem BGS.Markoff.nonTwoTorsionBoundedOrderTraceSet_subset_maximalDivisorTraceCover {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq G] [DecidableEq T] (trace : G → T) (bound : ℕ) : nonTwoTorsionBoundedOrderTraceSet trace bound ⊆ nonTwoTorsionMaximalDivisorTraceCover trace bound

Every bounded-order non-two-torsion trace lies in the fixed-point-free maximal-divisor cover.

theorem BGS.Markoff.two_mul_nonTwoTorsionMaximalDivisorTraceCover_card_le {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) (htraceInv : ∀ (x : G), trace x⁻¹ = trace x) : 2 * (nonTwoTorsionMaximalDivisorTraceCover trace bound).card ≤ (bound - 1) * (NumberTheory.maximalDivisorsBelow (Fintype.card G) bound).card

Each maximal-divisor piece is paired without fixed points, so summing the pieces introduces no additive constant.

theorem BGS.Markoff.two_mul_nonTwoTorsionBoundedOrderTraceSet_card_le_maximalDivisors {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) (htraceInv : ∀ (x : G), trace x⁻¹ = trace x) : 2 * (nonTwoTorsionBoundedOrderTraceSet trace bound).card ≤ (bound - 1) * (NumberTheory.maximalDivisorsBelow (Fintype.card G) bound).card

Fixed-point-free inversion pairing for the bounded-order trace set.