The middle-game trace equation

This module gives the exact finite solution set for equation (41) and proves the elementary quadratic-fiber bound used when one subgroup is small. The genuinely deep uniform power-saving estimate remains a separate Blueprint input.

noncomputable def BGS.Markoff.twistedUnitTrace {E : Type u_1} [Field E] (sigma : E) (h : Eˣ) : E

The twisted eigenvalue trace h + sigma / h.

Equations

• BGS.Markoff.twistedUnitTrace sigma h = ↑h + sigma * ↑h⁻¹

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

The possible left-hand elements above one fixed right-hand trace.

Equations

• BGS.Markoff.traceEquationLeftFiber sigma H₁ h₂ = {h₁ : ↥H₁ | BGS.Markoff.twistedUnitTrace sigma ↑h₁ = BGS.Markoff.twistedUnitTrace 1 h₂}

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

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

Equations

• BGS.Markoff.traceEquationSolutions sigma H₁ H₂ = Finset.univ.biUnion fun (h₂ : ↥H₂) => Finset.image (fun (h₁ : ↥H₁) => (h₁, h₂)) (BGS.Markoff.traceEquationLeftFiber sigma H₁ ↑h₂)

@[simp]

theorem BGS.Markoff.mem_traceEquationSolutions_iff {E : Type u_1} [Field E] [Fintype E] {sigma : E} {H₁ H₂ : Subgroup Eˣ} {h : ↥H₁ × ↥H₂} : h ∈ traceEquationSolutions sigma H₁ H₂ ↔ twistedUnitTrace sigma ↑h.1 = twistedUnitTrace 1 ↑h.2

noncomputable def BGS.Markoff.twistedTracePolynomial {E : Type u_1} [Field E] (sigma trace : E) : Polynomial E

After one trace value is fixed, the other unit satisfies a monic quadratic.

Equations

• BGS.Markoff.twistedTracePolynomial sigma trace = Polynomial.X ^ 2 - Polynomial.C trace * Polynomial.X + Polynomial.C sigma

theorem BGS.Markoff.twistedTracePolynomial_monic {E : Type u_1} [Field E] (sigma trace : E) : (twistedTracePolynomial sigma trace).Monic

@[simp]

theorem BGS.Markoff.twistedTracePolynomial_natDegree {E : Type u_1} [Field E] (sigma trace : E) : (twistedTracePolynomial sigma trace).natDegree = 2

theorem BGS.Markoff.eval_twistedTracePolynomial_eq_zero_iff {E : Type u_1} [Field E] (sigma trace : E) (h : Eˣ) : Polynomial.eval (↑h) (twistedTracePolynomial sigma trace) = 0 ↔ twistedUnitTrace sigma h = trace

theorem BGS.Markoff.traceEquationLeftFiber_card_le_two {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ : Subgroup Eˣ) (h₂ : Eˣ) : (traceEquationLeftFiber sigma H₁ h₂).card ≤ 2

For a fixed right-hand trace, at most two elements of the left subgroup solve the equation.

theorem BGS.Markoff.traceEquationSolutions_card_le_two_mul_right {E : Type u_1} [Field E] [Fintype E] (sigma : E) (H₁ H₂ : Subgroup Eˣ) : (traceEquationSolutions sigma H₁ H₂).card ≤ 2 * Nat.card ↥H₂

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