Explicit parametrizations of normalized Markoff fibers

This module formalizes the split and nonsplit parametrizations underlying Lemmas 4 and 5 of Bourgain--Gamburd--Sarnak. The trace-zero fiber is deliberately kept visible: although its rotation is semisimple, its conic is singular, so the paper's claimed single-torus parametrization needs the additional hypothesis that the fixed normalized trace is nonzero.

def BGS.Markoff.splitFiberProduct {F : Type u} [Field F] (w : Fˣ) : F

The scalar product of the two eigen-coordinates on a nonparabolic normalized fiber.

Equations

• BGS.Markoff.splitFiberProduct w = BGS.Markoff.splitTorusTrace w ^ 2 / (BGS.Markoff.splitTorusTrace w ^ 2 - 4)

def BGS.Markoff.splitFiberPoint {F : Type u} [Field F] (w s : Fˣ) : NormalizedPoint F

The point on the normalized fiber obtained from a nonzero first eigen-coordinate.

Equations

• BGS.Markoff.splitFiberPoint w s = { u1 := BGS.Markoff.splitTorusTrace w, u2 := ↑s + BGS.Markoff.splitFiberProduct w * ↑s⁻¹, u3 := ↑s * ↑w + BGS.Markoff.splitFiberProduct w * ↑s⁻¹ * ↑w⁻¹ }

def BGS.Markoff.splitFiberFirstEigenCoordinate {F : Type u} [Field F] (w : Fˣ) (x : NormalizedPoint F) : F

The first eigen-coordinate recovered from a point in the fixed-trace plane.

Equations

• BGS.Markoff.splitFiberFirstEigenCoordinate w x = (x.u3 - ↑w⁻¹ * x.u2) / (↑w - ↑w⁻¹)

def BGS.Markoff.splitFiberSecondEigenCoordinate {F : Type u} [Field F] (w : Fˣ) (x : NormalizedPoint F) : F

The second eigen-coordinate recovered from a point in the fixed-trace plane.

Equations

• BGS.Markoff.splitFiberSecondEigenCoordinate w x = (↑w * x.u2 - x.u3) / (↑w - ↑w⁻¹)

theorem BGS.Markoff.splitTorusTrace_sq_sub_four {F : Type u} [Field F] (w : Fˣ) : splitTorusTrace w ^ 2 - 4 = (↑w - ↑w⁻¹) ^ 2

theorem BGS.Markoff.splitEigenvalueDifference_ne_zero {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) : ↑w - ↑w⁻¹ ≠ 0

theorem BGS.Markoff.splitFiberProduct_ne_zero {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) : splitFiberProduct w ≠ 0

theorem BGS.Markoff.normalizedPolynomial_splitEigenCoordinates {F : Type u} [Field F] (w : Fˣ) (a b : F) : normalizedPolynomial { u1 := splitTorusTrace w, u2 := a + b, u3 := a * ↑w + b * ↑w⁻¹ } = splitTorusTrace w ^ 2 + (4 - splitTorusTrace w ^ 2) * a * b

theorem BGS.Markoff.splitFiberPoint_mem {F : Type u} [Field F] (w s : Fˣ) (hw : ↑w ^ 2 ≠ 1) : splitFiberPoint w s ∈ normalizedFiber1 (splitTorusTrace w)

theorem BGS.Markoff.splitFiberFirstEigenCoordinate_point {F : Type u} [Field F] (w s : Fˣ) (hw : ↑w ^ 2 ≠ 1) : splitFiberFirstEigenCoordinate w (splitFiberPoint w s) = ↑s

theorem BGS.Markoff.splitFiberEigenCoordinates_add {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (x : NormalizedPoint F) : splitFiberFirstEigenCoordinate w x + splitFiberSecondEigenCoordinate w x = x.u2

theorem BGS.Markoff.splitFiberEigenCoordinates_weighted_add {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (x : NormalizedPoint F) : splitFiberFirstEigenCoordinate w x * ↑w + splitFiberSecondEigenCoordinate w x * ↑w⁻¹ = x.u3

theorem BGS.Markoff.splitFiberEigenCoordinates_product {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (x : ↑(normalizedFiber1 (splitTorusTrace w))) : splitFiberFirstEigenCoordinate w ↑x * splitFiberSecondEigenCoordinate w ↑x = splitFiberProduct w

theorem BGS.Markoff.splitFiberFirstEigenCoordinate_ne_zero {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) (x : ↑(normalizedFiber1 (splitTorusTrace w))) : splitFiberFirstEigenCoordinate w ↑x ≠ 0

noncomputable def BGS.Markoff.splitFiberEquiv {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) : Fˣ ≃ ↑(normalizedFiber1 (splitTorusTrace w))

The split semisimple normalized fiber, away from trace zero, is explicitly equivalent to the multiplicative group of the base field.

Equations

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

theorem BGS.Markoff.normalizedRotate1_splitFiberPoint {F : Type u} [Field F] (w s : Fˣ) : normalizedRotate1 (splitFiberPoint w s) = splitFiberPoint w (s * w)

Under the explicit split-fiber parametrization, normalized rotation is multiplication by the chosen eigenvalue.

theorem BGS.Markoff.iterate_normalizedRotate1_splitFiberPoint {F : Type u} [Field F] (w s : Fˣ) (n : ℕ) : normalizedRotate1^[n] (splitFiberPoint w s) = splitFiberPoint w (s * w ^ n)

Every iterate of the split-fiber rotation multiplies the eigen-coordinate by the matching power of the eigenvalue.

theorem BGS.Markoff.iterate_normalizedRotate1_splitFiberPoint_eq_self_iff {F : Type u} [Field F] (w s : Fˣ) (hw : ↑w ^ 2 ≠ 1) (n : ℕ) : normalizedRotate1^[n] (splitFiberPoint w s) = splitFiberPoint w s ↔ w ^ n = 1

noncomputable def BGS.Markoff.splitRotationCycle {F : Type u} [Field F] (w s : Fˣ) : Finset (NormalizedPoint F)

The finite cycle obtained from one full split rotation period.

Equations

• BGS.Markoff.splitRotationCycle w s = Finset.image (fun (n : ℕ) => BGS.Markoff.normalizedRotate1^[n] (BGS.Markoff.splitFiberPoint w s)) (Finset.range (orderOf w))

theorem BGS.Markoff.splitRotationCycle_card {F : Type u} [Field F] (w s : Fˣ) (hw : ↑w ^ 2 ≠ 1) : (splitRotationCycle w s).card = orderOf w

The split rotation cycle has exactly the multiplicative order of its eigenvalue.

theorem BGS.Markoff.splitRotationCycle_card_eq_rotationOrder {F : Type u} [Field F] (w s : Fˣ) (hw : ↑w ^ 2 ≠ 1) : (splitRotationCycle w s).card = rotationOrder (splitTorusTrace w)

Replacing the eigenvalue order by the already-proved matrix rotation order connects the explicit split cycle to the project's canonical rotationOrder.

theorem BGS.Markoff.splitFiber_card {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) : Nat.card ↑(normalizedFiber1 (splitTorusTrace w)) = Nat.card F - 1

Consequently a finite split fiber with nonzero trace has exactly one fewer point than the base field.

theorem BGS.Markoff.splitNormalizedFiber_zmod_natCard (p : ℕ) [Fact (Nat.Prime p)] (w : (ZMod p)ˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) : Nat.card ↑(normalizedFiber1 (splitTorusTrace w)) = p - 1

def BGS.Markoff.normalizedPuncturedFiber1 {R : Type u} [CommRing R] (a : R) : Set (NormalizedPoint R)

The punctured normalized fiber used by the paper's conic sections.

Equations

• BGS.Markoff.normalizedPuncturedFiber1 a = BGS.Markoff.normalizedFiber1 a \ {BGS.Markoff.normalizedOrigin}

def BGS.Markoff.normalizedFiber1Finset (R : Type u) [CommRing R] [Fintype R] [DecidableEq R] (a : R) : Finset (NormalizedPoint R)

A computable finite presentation of a normalized fixed-coordinate fiber.

Equations

• BGS.Markoff.normalizedFiber1Finset R a = {x : BGS.Markoff.NormalizedPoint R | BGS.Markoff.normalizedPolynomial x = 0 ∧ x.u1 = a}

def BGS.Markoff.normalizedPuncturedFiber1Finset (R : Type u) [CommRing R] [Fintype R] [DecidableEq R] (a : R) : Finset (NormalizedPoint R)

A computable finite presentation of a punctured normalized fixed-coordinate fiber.

Equations

• BGS.Markoff.normalizedPuncturedFiber1Finset R a = (BGS.Markoff.normalizedFiber1Finset R a).erase BGS.Markoff.normalizedOrigin

@[simp]

theorem BGS.Markoff.mem_normalizedFiber1Finset_iff {R : Type u} [CommRing R] [Fintype R] [DecidableEq R] {a : R} {x : NormalizedPoint R} : x ∈ normalizedFiber1Finset R a ↔ x ∈ normalizedFiber1 a

@[simp]

theorem BGS.Markoff.mem_normalizedPuncturedFiber1Finset_iff {R : Type u} [CommRing R] [Fintype R] [DecidableEq R] {a : R} {x : NormalizedPoint R} : x ∈ normalizedPuncturedFiber1Finset R a ↔ x ∈ normalizedPuncturedFiber1 a

def BGS.Markoff.normalizedPuncturedFiber1EquivFinset (R : Type u) [CommRing R] [Fintype R] [DecidableEq R] (a : R) : ↑(normalizedPuncturedFiber1 a) ≃ ↥(normalizedPuncturedFiber1Finset R a)

The set-theoretic and computable-finset presentations have the same elements.

Equations

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

theorem BGS.Markoff.normalizedFiber1_zero_zmod_five_card : (normalizedFiber1Finset (ZMod 5) 0).card = 9

At the split semisimple trace zero over ZMod 5, the full affine fiber has nine points.

theorem BGS.Markoff.normalizedPuncturedFiber1_zero_zmod_five_card : (normalizedPuncturedFiber1Finset (ZMod 5) 0).card = 8

Removing the singular origin leaves eight points, not the four predicted by the paper's uniform p - 1 assertion for split semisimple fibers.

theorem BGS.Markoff.no_split_torus_equiv_normalizedPuncturedFiber1_zero_zmod_five : ¬Nonempty ((ZMod 5)ˣ ≃ ↑(normalizedPuncturedFiber1 0))

Thus the trace-zero punctured fiber cannot be equivalent to the multiplicative group, which has four elements. This is the exact obstruction requiring the nonzero-trace hypothesis above.

noncomputable def BGS.Markoff.quadraticNormUnitsHom (p : ℕ) [Fact (Nat.Prime p)] : (quadraticFiniteField p)ˣ →* (ZMod p)ˣ

The norm homomorphism on units of the canonical quadratic extension.

Equations

• BGS.Markoff.quadraticNormUnitsHom p = Units.map (Algebra.norm (ZMod p))

noncomputable def BGS.Markoff.quadraticNormFiber (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) : Set (quadraticFiniteField p)ˣ

A nonzero norm fiber in the canonical quadratic extension.

Equations

• BGS.Markoff.quadraticNormFiber p k = ⇑(BGS.Markoff.quadraticNormUnitsHom p) ⁻¹' {k}

noncomputable def BGS.Markoff.quadraticNormFiberEquivNormOne (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) : ↑(quadraticNormFiber p k) ≃ ↥(quadraticNormOneTorus p)

Every nonzero norm fiber is a torsor for the concrete quadratic norm-one torus.

Equations

• BGS.Markoff.quadraticNormFiberEquivNormOne p k = id (MonoidHom.fiberEquivKerOfSurjective ⋯ k)

noncomputable def BGS.Markoff.quadraticNormEquationFiberEquivNormOne (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) : { s : (quadraticFiniteField p)ˣ // (quadraticNormUnitsHom p) s = k } ≃ ↥(quadraticNormOneTorus p)

The equality-form fiber used by Equiv.sigmaFiberEquiv is the same norm torsor.

Equations

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

noncomputable def BGS.Markoff.quadraticUnitsEquivBaseUnitsProdNormOne (p : ℕ) [Fact (Nat.Prime p)] : (quadraticFiniteField p)ˣ ≃ (ZMod p)ˣ × ↥(quadraticNormOneTorus p)

The multiplicative group of the quadratic field is a product of the base-field units and the norm-one torus, after making the canonical finite-field norm-fiber choices.

Equations

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

theorem BGS.Markoff.quadraticNormOneTorus_natCard (p : ℕ) [Fact (Nat.Prime p)] : Nat.card ↥(quadraticNormOneTorus p) = p + 1

The concrete quadratic norm-one torus has exactly p + 1 elements.

theorem BGS.Markoff.quadraticNormFiber_natCard (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) : Nat.card ↑(quadraticNormFiber p k) = p + 1

Every nonzero quadratic norm fiber has p + 1 points.

theorem BGS.Markoff.algebraMap_quadraticTrace (p : ℕ) [Fact (Nat.Prime p)] (x : quadraticFiniteField p) : (algebraMap (ZMod p) (quadraticFiniteField p)) ((Algebra.trace (ZMod p) (quadraticFiniteField p)) x) = x + x ^ p

The quadratic field trace is the sum of an element and its p-power Frobenius conjugate.

theorem BGS.Markoff.algebraMap_quadraticNorm (p : ℕ) [Fact (Nat.Prime p)] (x : quadraticFiniteField p) : (algebraMap (ZMod p) (quadraticFiniteField p)) ((Algebra.norm (ZMod p)) x) = x * x ^ p

The quadratic field norm is the product of an element and its p-power Frobenius conjugate.

theorem BGS.Markoff.quadraticNormOne_frobenius_eq_inv (p : ℕ) [Fact (Nat.Prime p)] (w : ↥(quadraticNormOneTorus p)) : ↑↑w ^ p = ↑(↑w)⁻¹

Frobenius acts on a norm-one eigenvalue by inversion.

theorem BGS.Markoff.quadraticNormFiber_frobenius_eq_norm_mul_inv (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) : ↑↑s ^ p = (algebraMap (ZMod p) (quadraticFiniteField p)) ↑k * (↑↑s)⁻¹

Frobenius on a nonzero norm fiber is multiplication by the prescribed norm followed by inversion.

noncomputable def BGS.Markoff.quadraticFiberProduct (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) : ZMod p

The scalar t²/(t²-4) controlling either eigen-coordinate parametrization.

Equations

• BGS.Markoff.quadraticFiberProduct p t = t ^ 2 / (t ^ 2 - 4)

theorem BGS.Markoff.quadraticFiberProduct_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) : quadraticFiberProduct p t ≠ 0

noncomputable def BGS.Markoff.quadraticFiberProductUnit (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) : (ZMod p)ˣ

The nonzero scalar as a unit, used to index its norm fiber.

Equations

• BGS.Markoff.quadraticFiberProductUnit p t ht ht0 = Units.mk0 (BGS.Markoff.quadraticFiberProduct p t) ⋯

noncomputable def BGS.Markoff.quadraticConicNormFiber (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) : Set (quadraticFiniteField p)ˣ

The norm fiber occurring in the paper's nonsplit conic parametrization.

Equations

• BGS.Markoff.quadraticConicNormFiber p t ht ht0 = BGS.Markoff.quadraticNormFiber p (BGS.Markoff.quadraticFiberProductUnit p t ht ht0)

noncomputable def BGS.Markoff.algebraMapNormalizedPoint (p : ℕ) [Fact (Nat.Prime p)] (x : NormalizedPoint (ZMod p)) : NormalizedPoint (quadraticFiniteField p)

Coordinatewise scalar extension of a normalized point.

Equations

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

theorem BGS.Markoff.normalizedPolynomial_algebraMapNormalizedPoint (p : ℕ) [Fact (Nat.Prime p)] (x : NormalizedPoint (ZMod p)) : normalizedPolynomial (algebraMapNormalizedPoint p x) = (algebraMap (ZMod p) (quadraticFiniteField p)) (normalizedPolynomial x)

noncomputable def BGS.Markoff.quadraticNormFiberPoint (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (s : ↑(quadraticConicNormFiber p t ht ht0)) : NormalizedPoint (ZMod p)

Trace coordinates turn a point of the prescribed norm fiber into a normalized base-field point.

Equations

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

theorem BGS.Markoff.algebraMap_quadraticFiberProduct (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) : (algebraMap (ZMod p) (quadraticFiniteField p)) (quadraticFiberProduct p t) = splitFiberProduct ↑w

theorem BGS.Markoff.algebraMap_quadraticNormFiberPoint (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) : algebraMapNormalizedPoint p (quadraticNormFiberPoint p t ht ht0 w s) = splitFiberPoint ↑w ↑s

theorem BGS.Markoff.quadraticNormFiberPoint_mem (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (s : ↑(quadraticConicNormFiber p t ht ht0)) : quadraticNormFiberPoint p t ht ht0 w s ∈ normalizedFiber1 t

noncomputable def BGS.Markoff.quadraticNormFiberMulNormOne (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (g : ↥(quadraticNormOneTorus p)) : ↑(quadraticNormFiber p k)

Multiplication by a norm-one element preserves every nonzero norm fiber.

Equations

• BGS.Markoff.quadraticNormFiberMulNormOne p k s g = ⟨↑s * ↑g, ⋯⟩

theorem BGS.Markoff.algebraMapNormalizedPoint_injective (p : ℕ) [Fact (Nat.Prime p)] : Function.Injective (algebraMapNormalizedPoint p)

theorem BGS.Markoff.algebraMapNormalizedPoint_normalizedRotate1 (p : ℕ) [Fact (Nat.Prime p)] (x : NormalizedPoint (ZMod p)) : algebraMapNormalizedPoint p (normalizedRotate1 x) = normalizedRotate1 (algebraMapNormalizedPoint p x)

theorem BGS.Markoff.algebraMap_zmod_pow_card (p : ℕ) [Fact (Nat.Prime p)] (a : ZMod p) : (algebraMap (ZMod p) (quadraticFiniteField p)) a ^ p = (algebraMap (ZMod p) (quadraticFiniteField p)) a

noncomputable def BGS.Markoff.algebraMapNormalizedFiberPoint (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (x : ↑(normalizedFiber1 t)) : ↑(normalizedFiber1 (splitTorusTrace ↑w))

A base-field fiber point, viewed on the diagonalized fiber in the quadratic extension.

Equations

• BGS.Markoff.algebraMapNormalizedFiberPoint p t w htrace x = ⟨BGS.Markoff.algebraMapNormalizedPoint p ↑x, ⋯⟩

theorem BGS.Markoff.quadraticFiberFirstEigenCoordinate_frobenius (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (w : ↥(quadraticNormOneTorus p)) (hw : ↑↑w ^ 2 ≠ 1) (x : ↑(normalizedFiber1 t)) : splitFiberFirstEigenCoordinate (↑w) (algebraMapNormalizedPoint p ↑x) ^ p = splitFiberSecondEigenCoordinate (↑w) (algebraMapNormalizedPoint p ↑x)

For a base-field point, Frobenius exchanges its two eigen-coordinates in the quadratic extension.

noncomputable def BGS.Markoff.quadraticNormFiberParameter (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (x : ↑(normalizedFiber1 t)) : ↑(quadraticConicNormFiber p t ht ht0)

Recover the first extension-field eigen-coordinate from a base-field conic point and prove that it lies in the prescribed norm fiber.

Equations

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

theorem BGS.Markoff.quadraticNormFiberParameter_point (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (s : ↑(quadraticConicNormFiber p t ht ht0)) : quadraticNormFiberParameter p t ht ht0 w htrace hw ⟨quadraticNormFiberPoint p t ht ht0 w s, ⋯⟩ = s

theorem BGS.Markoff.quadraticNormFiberPoint_parameter (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (x : ↑(normalizedFiber1 t)) : quadraticNormFiberPoint p t ht ht0 w (quadraticNormFiberParameter p t ht ht0 w htrace hw x) = ↑x

noncomputable def BGS.Markoff.quadraticNormFiberEquiv (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) : ↑(quadraticConicNormFiber p t ht ht0) ≃ ↑(normalizedFiber1 t)

The nonsplit nonzero normalized fiber is explicitly equivalent to its quadratic norm fiber.

Equations

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

theorem BGS.Markoff.nonsplitNormalizedFiber_natCard (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) : Nat.card ↑(normalizedFiber1 t) = p + 1

Consequently the nonsplit nonzero normalized fiber has exactly p + 1 points.

theorem BGS.Markoff.normalizedRotate1_quadraticNormFiberPoint (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) : normalizedRotate1 (quadraticNormFiberPoint p t ht ht0 w s) = quadraticNormFiberPoint p t ht ht0 w (quadraticNormFiberMulNormOne p (quadraticFiberProductUnit p t ht ht0) s w)

On the nonsplit norm-fiber parametrization, normalized rotation is multiplication by its norm-one eigenvalue.

theorem BGS.Markoff.quadraticNormFiberMulNormOne_assoc (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (g h : ↥(quadraticNormOneTorus p)) : quadraticNormFiberMulNormOne p k (quadraticNormFiberMulNormOne p k s g) h = quadraticNormFiberMulNormOne p k s (g * h)

theorem BGS.Markoff.quadraticNormFiberMulNormOne_one (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) : quadraticNormFiberMulNormOne p k s 1 = s

theorem BGS.Markoff.quadraticNormFiberMulNormOne_pow (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (g : ↥(quadraticNormOneTorus p)) (n : ℕ) : ↑(quadraticNormFiberMulNormOne p k s (g ^ n)) = ↑s * ↑g ^ n

theorem BGS.Markoff.quadraticNormFiberPoint_injective (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) : Function.Injective (quadraticNormFiberPoint p t ht ht0 w)

theorem BGS.Markoff.iterate_normalizedRotate1_quadraticNormFiberPoint (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) (n : ℕ) : normalizedRotate1^[n] (quadraticNormFiberPoint p t ht ht0 w s) = quadraticNormFiberPoint p t ht ht0 w (quadraticNormFiberMulNormOne p (quadraticFiberProductUnit p t ht ht0) s (w ^ n))

theorem BGS.Markoff.iterate_normalizedRotate1_quadraticNormFiberPoint_eq_self_iff (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (s : ↑(quadraticConicNormFiber p t ht ht0)) (n : ℕ) : normalizedRotate1^[n] (quadraticNormFiberPoint p t ht ht0 w s) = quadraticNormFiberPoint p t ht ht0 w s ↔ w ^ n = 1

noncomputable def BGS.Markoff.quadraticNormFiberRotationCycle (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (s : ↑(quadraticConicNormFiber p t ht ht0)) : Finset (NormalizedPoint (ZMod p))

One full nonsplit rotation cycle, represented in the base-field conic.

Equations

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

theorem BGS.Markoff.quadraticNormFiberRotationCycle_card (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (s : ↑(quadraticConicNormFiber p t ht ht0)) : (quadraticNormFiberRotationCycle p t ht ht0 w s).card = orderOf w

theorem BGS.Markoff.quadraticNormFiberRotationCycle_card_eq_rotationOrder (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (s : ↑(quadraticConicNormFiber p t ht ht0)) : (quadraticNormFiberRotationCycle p t ht ht0 w s).card = rotationOrder t

noncomputable def BGS.Markoff.normalizedRotationCycle {F : Type u} [Field F] (t : F) (x : NormalizedPoint F) : Finset (NormalizedPoint F)

The canonical finite cycle cut out by one full matrix rotation period.

Equations

• BGS.Markoff.normalizedRotationCycle t x = Finset.image (fun (n : ℕ) => BGS.Markoff.normalizedRotate1^[n] x) (Finset.range (BGS.Markoff.rotationOrder t))

theorem BGS.Markoff.normalizedRotationCycle_card_split {F : Type u} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) (x : ↑(normalizedFiber1 (splitTorusTrace w))) : (normalizedRotationCycle (splitTorusTrace w) ↑x).card = rotationOrder (splitTorusTrace w)

Every point of a nonzero split semisimple fiber has orbit-cycle cardinality equal to the canonical matrix rotation order.

theorem BGS.Markoff.normalizedRotationCycle_card_nonsplit (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (hw : ↑↑w ^ 2 ≠ 1) (x : ↑(normalizedFiber1 t)) : (normalizedRotationCycle t ↑x).card = rotationOrder t

Every point of a nonzero nonsplit semisimple fiber has orbit-cycle cardinality equal to the canonical matrix rotation order.

theorem BGS.Markoff.normalizedRotationCycle_card_of_nonzero_nonparabolic (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (x : ↑(normalizedFiber1 t)) : (normalizedRotationCycle t ↑x).card = rotationOrder t

Every point of a nonzero nonparabolic normalized fiber has rotation-cycle cardinality equal to the canonical matrix rotation order. The split/nonsplit classification is consumed here to obtain the explicit eigenvalue witness required by the two parametrization kernels.

theorem BGS.Markoff.iterate_two_mul_normalizedRotate1_parabolicLineAtNegTwo {R : Type u} [CommRing R] (k : ℕ) (i t : R) : normalizedRotate1^[2 * k] (parabolicLineAtNegTwo i t) = parabolicLineAtNegTwo i (t - ↑k * (4 * i))

An even number of trace--2 rotations stays on the same parabolic line and translates its parameter by a multiple of -4i.

theorem BGS.Markoff.iterate_two_mul_add_one_normalizedRotate1_parabolicLineAtNegTwo {R : Type u} [CommRing R] (k : ℕ) (i t : R) : normalizedRotate1^[2 * k + 1] (parabolicLineAtNegTwo i t) = parabolicLineAtNegTwo (-i) (-(t - ↑k * (4 * i)) + 2 * i)

An odd number of trace--2 rotations lands on the opposite parabolic line.

theorem BGS.Markoff.normalizedRotationCycle_card_parabolicLineAtTwo (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (i t : ZMod p) (hi : i ^ 2 = -1) : (normalizedRotationCycle 2 (parabolicLineAtTwo i t)).card = rotationOrder 2

Every point on either trace-2 parabolic line has a full rotation cycle of cardinality p, matching the separately computed unipotent matrix order.

theorem BGS.Markoff.normalizedRotationCycle_card_parabolicLineAtNegTwo (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (i t : ZMod p) (hi : i ^ 2 = -1) : (normalizedRotationCycle (-2) (parabolicLineAtNegTwo i t)).card = rotationOrder (-2)

Every point on either trace--2 parabolic line has a full cycle of cardinality 2p, matching the separately computed matrix order.