Descent for positive Markoff triples and Markoff's theorem

Let 1 ≤ a ≤ b ≤ c be integers with a² + b² + c² = 3abc and (a, b, c) ≠ (1, 1, 1). As a quadratic in its last coordinate, the Markoff equation has the roots c and c' = 3ab - c, and the value of that quadratic at b is a² + (2 - 3a) b² ≤ 0. Hence c is the unique largest coordinate and the other root satisfies 0 < c' ≤ b < c, with c' = b only for (1, 1, 2). So the Vieta move in the position of the largest coordinate strictly decreases it, while the other two moves strictly increase it.

Descending along these moves proves Markoff's theorem: every positive Markoff triple is obtained from (1, 1, 1) by a finite word in the Vieta moves R₀, R₁, R₂, with no coordinate permutations. Equivalently, the Markoff graph on the positive triples is connected.

Main results

• TauCeti.three_mul_mul_sub_le_of_markoff, TauCeti.lt_of_markoff, TauCeti.three_mul_mul_sub_lt_of_markoff, TauCeti.three_mul_mul_sub_eq_iff_of_markoff: the descent inequality for an increasing positive Markoff triple.
• TauCeti.markoffVieta_apply_self_lt: the move in the position of a largest coordinate strictly decreases it, unless the triple is (1, 1, 1).
• TauCeti.lt_markoffVieta_apply_self_of_ne: the other two moves strictly increase it.
• TauCeti.mem_positiveMarkoffTriples_iff_exists_foldr: Markoff's theorem, the positive Markoff triples are exactly the words in the moves applied to (1, 1, 1).
• TauCeti.markoffGraph_connected: the Markoff graph is connected.

References

• Y. Zhang, Congruence and uniqueness of certain Markoff numbers, Acta Arith. 128 (2007), §1, Theorem A and the descent inequality after it.
• Y. Zhang, An elementary proof of Markoff conjecture for prime powers, §3. The descent there is on the sum of the coordinates; we descend in the position of the largest coordinate, so no rearrangement of the coordinates is needed.

The descent inequality

theorem TauCeti.three_mul_mul_sub_pos_of_markoff {a b c : ℤ} (h : a ^ 2 + b ^ 2 + c ^ 2 = 3 * a * b * c) (hc : 0 < c) : 0 < 3 * a * b - c

The other root 3ab - c of a Markoff triple with 0 < c is positive.

theorem TauCeti.lt_of_markoff {a b c : ℤ} (h : a ^ 2 + b ^ 2 + c ^ 2 = 3 * a * b * c) (ha : 0 < a) (hab : a ≤ b) (hbc : b ≤ c) (hne : ¬(a = 1 ∧ b = 1 ∧ c = 1)) : b < c

In an increasing positive Markoff triple a ≤ b ≤ c other than (1, 1, 1), the last coordinate is strictly largest.

theorem TauCeti.three_mul_mul_sub_le_of_markoff {a b c : ℤ} (h : a ^ 2 + b ^ 2 + c ^ 2 = 3 * a * b * c) (ha : 0 < a) (hab : a ≤ b) (hbc : b ≤ c) (hne : ¬(a = 1 ∧ b = 1 ∧ c = 1)) : 3 * a * b - c ≤ b

The descent inequality. In an increasing positive Markoff triple a ≤ b ≤ c other than (1, 1, 1), the other root 3ab - c in the last coordinate is at most b.

theorem TauCeti.three_mul_mul_sub_eq_iff_of_markoff {a b c : ℤ} (h : a ^ 2 + b ^ 2 + c ^ 2 = 3 * a * b * c) (ha : 0 < a) (hab : a ≤ b) : 3 * a * b - c = b ↔ a = 1 ∧ b = 1 ∧ c = 2

The other root 3ab - c equals the middle coordinate b only for the triple (1, 1, 2).

theorem TauCeti.three_mul_mul_sub_lt_of_markoff {a b c : ℤ} (h : a ^ 2 + b ^ 2 + c ^ 2 = 3 * a * b * c) (ha : 0 < a) (hb : 0 < b) (hac : a ≤ c) (hbc : b ≤ c) (hne : ¬(a = 1 ∧ b = 1 ∧ c = 1)) : 3 * a * b - c < c

In a positive Markoff triple other than (1, 1, 1) whose last coordinate c is a largest one, the other root 3ab - c in that coordinate is strictly smaller than c.

Descent along the Vieta moves

theorem TauCeti.markoffVieta_apply_self_lt {x : Fin 3 → ℤ} {i : Fin 3} (hx : x ∈ positiveMarkoffTriples) (hmax : ∀ (j : Fin 3), x j ≤ x i) (hne : x ≠ 1) : markoffVieta i x i < x i

Descent. If x_i is a largest coordinate of a positive Markoff triple x ≠ (1, 1, 1), then the Vieta move R_i strictly decreases it.

theorem TauCeti.lt_markoffVieta_apply_self_of_ne {x : Fin 3 → ℤ} {i j : Fin 3} (hpos : ∀ (k : Fin 3), 0 < x k) (hmax : ∀ (k : Fin 3), x k ≤ x i) (hji : j ≠ i) : x i < markoffVieta j x j

If x_i is a largest coordinate of a triple of positive integers, for instance of a positive Markoff triple, the Vieta moves in the other two positions produce a coordinate strictly larger than x_i.

theorem TauCeti.exists_markoffVieta_apply_self_lt {x : Fin 3 → ℤ} (hx : x ∈ positiveMarkoffTriples) (hne : x ≠ 1) : ∃ (i : Fin 3), markoffVieta i x i < x i

Every positive Markoff triple other than (1, 1, 1) has a Vieta move that strictly decreases one of its coordinates.

Markoff's theorem

theorem TauCeti.foldr_markoffVieta_mem_positiveMarkoffTriples (l : List (Fin 3)) : List.foldr markoffVieta 1 l ∈ positiveMarkoffTriples

Every word in the Vieta moves applied to (1, 1, 1) is a positive Markoff triple.

theorem TauCeti.exists_foldr_markoffVieta_eq {x : Fin 3 → ℤ} (hx : x ∈ positiveMarkoffTriples) : ∃ (l : List (Fin 3)), List.foldr markoffVieta 1 l = x

Markoff's theorem. Every positive Markoff triple x is obtained from (1, 1, 1) by a finite word in the Vieta moves: x = R_{i₁} (R_{i₂} ⋯ (R_{i_k} (1, 1, 1))). No coordinate permutation is needed.

theorem TauCeti.mem_positiveMarkoffTriples_iff_exists_foldr {x : Fin 3 → ℤ} : x ∈ positiveMarkoffTriples ↔ ∃ (l : List (Fin 3)), List.foldr markoffVieta 1 l = x

Markoff's theorem, as a characterisation: the positive Markoff triples are exactly the words in the Vieta moves applied to (1, 1, 1).

theorem TauCeti.markoffGraph_connected : markoffGraph.Connected

The integer Markoff graph is connected: every positive Markoff triple is joined to (1, 1, 1) by a path of Vieta moves.

Examples