Divisibility of Markoff orbit cardinalities

This file formalizes Daniel E. Martin's elementary proof of the Markoff-graph corollary of Chen's theorem. Piecewise Penner weights sum to one at every punctured Markoff point, while the weight in coordinate i pairs to one across the i-th Vieta involution. Reindexing a finite Vieta-invariant set by those involutions then forces its cardinality to vanish in the ground field. Over ZMod p, this says that p divides the cardinality.

The result is stated only for 3 < p. This is the range used in Martin's proof and is necessary: at p = 3 the eight points with all coordinates in {1, -1} form one Vieta component.

noncomputable def BGS.Markoff.pennerWeights {F : Type u} [Field F] (x : Point F) : Point F

Martin's piecewise Penner weights in the original Markoff coordinates.

Equations

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

noncomputable def BGS.Markoff.puncturedPennerWeights {F : Type u} [Field F] (x : PuncturedMarkoffSurface F) : Point F

Penner weights restricted to the punctured Markoff surface.

Equations

• BGS.Markoff.puncturedPennerWeights x = BGS.Markoff.pennerWeights ↑↑x

theorem BGS.Markoff.puncturedPennerWeights_sum_eq_one {F : Type u} [Field F] (htwo : 2 ≠ 0) (hthree : 3 ≠ 0) (x : PuncturedMarkoffSurface F) : (puncturedPennerWeights x).x1 + (puncturedPennerWeights x).x2 + (puncturedPennerWeights x).x3 = 1

The three Penner weights at a punctured Markoff point sum to one.

theorem BGS.Markoff.puncturedPennerWeight_first_add_vieta1_eq_one {F : Type u} [Field F] (htwo : 2 ≠ 0) (hthree : 3 ≠ 0) (x : PuncturedMarkoffSurface F) : (puncturedPennerWeights x).x1 + (puncturedPennerWeights ((vieta1PuncturedPerm F) x)).x1 = 1

The first Penner weight pairs to one across the first Vieta involution.

theorem BGS.Markoff.puncturedPennerWeight_second_add_vieta2_eq_one {F : Type u} [Field F] (htwo : 2 ≠ 0) (hthree : 3 ≠ 0) (x : PuncturedMarkoffSurface F) : (puncturedPennerWeights x).x2 + (puncturedPennerWeights ((vieta2PuncturedPerm F) x)).x2 = 1

The second Penner weight pairs to one across the second Vieta involution.

theorem BGS.Markoff.puncturedPennerWeight_third_add_vieta3_eq_one {F : Type u} [Field F] (htwo : 2 ≠ 0) (hthree : 3 ≠ 0) (x : PuncturedMarkoffSurface F) : (puncturedPennerWeights x).x3 + (puncturedPennerWeights ((vieta3PuncturedPerm F) x)).x3 = 1

The third Penner weight pairs to one across the third Vieta involution.

theorem BGS.Markoff.card_cast_eq_zero_of_vieta_invariant {F : Type u} [Field F] (htwo : 2 ≠ 0) (hthree : 3 ≠ 0) (C : Finset (PuncturedMarkoffSurface F)) (hC1 : ∀ (x : PuncturedMarkoffSurface F), (vieta1PuncturedPerm F) x ∈ C ↔ x ∈ C) (hC2 : ∀ (x : PuncturedMarkoffSurface F), (vieta2PuncturedPerm F) x ∈ C ↔ x ∈ C) (hC3 : ∀ (x : PuncturedMarkoffSurface F), (vieta3PuncturedPerm F) x ∈ C ↔ x ∈ C) : ↑C.card = 0

A finite punctured Markoff set invariant under all three Vieta involutions has cardinality zero in the ground field.

theorem BGS.Markoff.prime_dvd_puncturedGammaOrbit_ncard (p : ℕ) [Fact (Nat.Prime p)] (hpThree : 3 < p) (x : PuncturedMarkoffSurface (ZMod p)) : p ∣ (puncturedGammaOrbit x).ncard

Every Gamma orbit on the punctured Markoff surface over ZMod p has cardinality divisible by p once 3 < p.