Documentation

LeanPool.MarkoffModP.BGS.Markoff.MiddleGame.RightInversionPairing

The right-coordinate inversion pairing #

The right-hand trace in the weighted middle-game equation is invariant under inversion. Away from the two-torsion points, every solution therefore occurs with a distinct partner having the same left coordinate. This gives a genuine factor of two for the nonparabolic left support, while leaving the existing parabolic escape branch responsible for the two fixed points.

source
theorem BGS.Markoff.splitTorusTrace_right_inv {E : Type u_1} [Field E] (h : Eˣ) :
splitTorusTrace h⁻¹ = splitTorusTrace h

The ordinary split trace is invariant under inversion.

source
theorem BGS.Markoff.weightedTraceEquationSolutions_right_inv_mem {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {H₁ H₂ : Subgroup Eˣ} {z : ↥H₁ × ↥H₂} (hz : z ∈ weightedTraceEquationSolutions alpha beta H₁ H₂) :
(z.1, z.2⁻¹) ∈ weightedTraceEquationSolutions alpha beta H₁ H₂

Inverting the right coordinate preserves every weighted trace-equation solution and leaves its left coordinate unchanged.

source
theorem BGS.Markoff.subgroupElement_ne_inv_of_sq_ne_one {E : Type u_1} [Field E] {H : Subgroup Eˣ} (h : ↥H) (hsq : ↑h ^ 2 ≠ 1) :
h ≠ h⁻¹

A subgroup element whose square is not one is distinct from its inverse.

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

The nonparabolic part of a weighted trace-equation solution set.

Equations
Instances For
    source
    @[simp]
    theorem BGS.Markoff.mem_weightedTraceEquationNonparabolicSolutions_iff {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {H₁ H₂ : Subgroup Eˣ} {z : ↥H₁ × ↥H₂} :
    z ∈ weightedTraceEquationNonparabolicSolutions alpha beta H₁ H₂ ↔ z ∈ weightedTraceEquationSolutions alpha beta H₁ H₂ ∧ ↑z.2 ^ 2 ≠ 1
    source
    noncomputable def BGS.Markoff.weightedTraceEquationNonparabolicLeftSupport {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) :
    Finset ↥H₁

    Left elements occurring in a nonparabolic weighted solution.

    Equations
    Instances For
      source
      @[simp]
      theorem BGS.Markoff.mem_weightedTraceEquationNonparabolicLeftSupport_iff {E : Type u_1} [Field E] [Fintype E] {alpha beta : E} {H₁ H₂ : Subgroup Eˣ} {h₁ : ↥H₁} :
      h₁ ∈ weightedTraceEquationNonparabolicLeftSupport alpha beta H₁ H₂ ↔ ∃ (h₂ : ↥H₂), weightedSplitTorusTrace alpha beta ↑h₁ = splitTorusTrace ↑h₂ ∧ ↑h₂ ^ 2 ≠ 1
      source
      theorem BGS.Markoff.two_mul_weightedTraceEquationNonparabolicLeftSupport_card_le_solutions {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) :
      2 * (weightedTraceEquationNonparabolicLeftSupport alpha beta H₁ H₂).card ≤ (weightedTraceEquationSolutions alpha beta H₁ H₂).card

      Every fiber of the nonparabolic right-inversion quotient has at least two points. Consequently twice the left-support cardinality is bounded by the full Corvaja--Zannier solution count.