Generalized Markov triples

DefinitionGeneralized Markov triple#✓fully proved

For a natural number \(k\), a \(k\)-generalized Markov triple is a triple \((a, b, c)\) of positive integers satisfying the \(k\)-generalized Markov equation \(\mathrm{GME}(k)\):

\[a^2 + b^2 + c^2 + k(bc + ca + ab) = (3 + 3k)abc.\]

For \(k = 0\) these are the classical Markov triples.

public def IsGenMarkovTriple (k a b c : ℕ) : Prop :=
  0 < a ∧ 0 < b ∧ 0 < c ∧
    a ^ 2 + b ^ 2 + c ^ 2 + k * (b * c + c * a + a * b) = (3 + 3 * k) * a * b * c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 1.2.

Used by 15

Used byBound on the number of generalized Markov triples with a given maximum · Vertices of the generalized Markov tree · 2-generalized Markov triples are squares of Markov triples · Unique maximal generalized Markov triple · Generalized Cohn triple · Generalized Markov number · A unique maximum is a generalized Markov number · Generalized Cohn triples give generalized Markov triples · \((1, 1, 1)\) is a generalized Markov triple · The Markov triple \((1, 1, 2)\) · Markov triples with a common characteristic number agree up to order · Generalized Markov triples are pairwise coprime · Vieta jumping identities for generalized Markov triples · Vertices of the wide generalized Cohn tree are generalized Cohn triples · Generalized Markov triples in the wide Markov tree

Theorem\((1, 1, 1)\) is a generalized Markov triple#✓fully proved

For every natural number \(k\), the triple \((1, 1, 1)\) is a \(k\)-generalized Markov triple.

public theorem isGenMarkovTriple_one_one_one (k : ℕ) : IsGenMarkovTriple k 1 1 1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 1.2.

Uses 1

Statement usesGeneralized Markov triple

TheoremThe Markov triple \((1, 1, 2)\)#✓fully proved

The triple \((1, 1, 2)\) is a \(0\)-generalized Markov triple, that is, a classical Markov triple: \(1^2 + 1^2 + 2^2 = 3 \cdot 1 \cdot 1 \cdot 2\).

public theorem isGenMarkovTriple_zero_one_one_two : IsGenMarkovTriple 0 1 1 2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 1.1.

Uses 1

Statement usesGeneralized Markov triple

DefinitionGeneralized Markov number#✓fully proved

Let \(k\) be a natural number. A natural number \(b\) is a \(k\)-generalized Markov number when there are natural numbers \(a\) and \(c\) such that \((a, b, c)\) is a \(k\)-generalized Markov triple.

Since the \(k\)-generalized Markov equation is symmetric in its three variables, this is the same as \(b\) being an entry, in any position, of some \(k\)-generalized Markov triple.

public def IsGenMarkovNumber (k b : ℕ) : Prop :=
  ∃ a c, IsGenMarkovTriple k a b c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 1.2.

Uses 1 · Used by 14

Statement usesGeneralized Markov triple

Used byBound on the number of generalized Markov triples with a given maximum · An even generalized Markov number forces \(k\) to be even · Uniqueness of maximal triples and injectivity of the fraction labeling · Unique maximal triple via the fraction labeling · Uniqueness for odd prime powers \(p^m\) and \(2p^m\) with \(p \nmid k^2 - 4\) · Uniqueness criterion via the congruence \(x^2 + kx + 1 \equiv 0 \pmod{b}\) · Generalized Markov numbers \(p\) and \(2p\) are unique maxima · Uniqueness for prime powers \(p^m\) and \(2p^m\) under conditions on \(k\) · Generalized Cohn matrices · A unique maximum is a generalized Markov number · Uniqueness for Markov numbers \(p^m\) and \(2p^m\) with \(p\) an odd prime · Uniqueness criterion for classical Markov numbers · Generalized Markov numbers divisible by \(4\) · Discriminant condition for prime-power generalized Markov numbers

DefinitionUnique maximal generalized Markov triple#✓fully proved

Let \(k\) and \(b\) be natural numbers. The number \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order if there is a \(k\)-generalized Markov triple \((a, b, c)\) with \(a \le b\) and \(c \le b\), and every \(k\)-generalized Markov triple \((a', b, c')\) with \(a' \le b\) and \(c' \le b\) satisfies \((a', c') = (a, c)\) or \((a', c') = (c, a)\).

public def HasUniqueMaxGenMarkovTriple (k b : ℕ) : Prop :=
  ∃ a c, IsGenMarkovTriple k a b c ∧ a ≤ b ∧ c ≤ b ∧
    ∀ a' c', IsGenMarkovTriple k a' b c' → a' ≤ b → c' ≤ b →
      (a' = a ∧ c' = c) ∨ (a' = c ∧ c' = a)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Conjecture 1.8.

Uses 1 · Used by 9

Statement usesGeneralized Markov triple

Used byUniqueness of maximal triples and injectivity of the fraction labeling · Unique maximal triple via the fraction labeling · Uniqueness for odd prime powers \(p^m\) and \(2p^m\) with \(p \nmid k^2 - 4\) · Uniqueness criterion via the congruence \(x^2 + kx + 1 \equiv 0 \pmod{b}\) · Generalized Markov numbers \(p\) and \(2p\) are unique maxima · Uniqueness for prime powers \(p^m\) and \(2p^m\) under conditions on \(k\) · A unique maximum is a generalized Markov number · Uniqueness for Markov numbers \(p^m\) and \(2p^m\) with \(p\) an odd prime · Uniqueness criterion for classical Markov numbers

TheoremA unique maximum is a generalized Markov number#✓fully proved

Let \(k\) and \(b\) be natural numbers. If \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order, then \(b\) is a \(k\)-generalized Markov number.

public theorem HasUniqueMaxGenMarkovTriple.isGenMarkovNumber {k b : ℕ}
    (h : HasUniqueMaxGenMarkovTriple k b) : IsGenMarkovNumber k b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Conjecture 1.8.

Uses 3

Statement usesUnique maximal generalized Markov triple · Generalized Markov number

Proof usesGeneralized Markov triple

DefinitionNumber of solutions of \(x^2 + kx + 1 \equiv 0 \pmod b\)#✓fully proved

For natural numbers \(k\) and \(b\), this is the number of integers \(x\) with \(0 \le x < b\) such that \(b\) divides \(x^2 + kx + 1\). For \(b = 0\) it is \(0\).

public def genMarkovCongruenceCount (k b : ℕ) : ℕ :=
  ((range b).filter fun x => b ∣ x ^ 2 + k * x + 1).card

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.5.

Used by 5

Used byAt most two solutions of \(x^2 + kx + 1 \equiv 0\) modulo a prime · At most two solutions of \(x^2 + kx + 1 \equiv 0\) modulo an odd prime power · The congruence \(x^2 + 1 \equiv 0 \pmod 5\) has two solutions · Uniqueness criterion via the congruence \(x^2 + kx + 1 \equiv 0 \pmod{b}\) · Uniqueness criterion for classical Markov numbers

TheoremThe congruence \(x^2 + 1 \equiv 0 \pmod 5\) has two solutions#✓fully proved

Exactly two integers \(x\) with \(0 \le x < 5\) satisfy \(x^2 + 1 \equiv 0 \pmod 5\).

They are \(x = 2\) and \(x = 3\).

public theorem genMarkovCongruenceCount_zero_five : genMarkovCongruenceCount 0 5 = 2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.2.

Uses 1

Statement usesNumber of solutions of \(x^2 + kx + 1 \equiv 0 \pmod b\)

TheoremUniqueness criterion via the congruence \(x^2 + kx + 1 \equiv 0 \pmod{b}\)#●ready to prove

Let \(k\) be a natural number and let \(b\) be a \(k\)-generalized Markov number with \(b \ne 1\) and \(b \ne k + 2\). If the congruence \(x^2 + kx + 1 \equiv 0 \pmod{b}\) has at most two solutions \(x\) with \(0 \le x < b\), then \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order.

public theorem_wanted hasUniqueMaxGenMarkovTriple_of_congruenceCount_le_two {k b : ℕ}
    (hb : IsGenMarkovNumber k b) (hb1 : b ≠ 1) (hbk : b ≠ k + 2)
    (hcount : genMarkovCongruenceCount k b ≤ 2) : HasUniqueMaxGenMarkovTriple k b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.5.

Uses 3

Statement usesUnique maximal generalized Markov triple · Generalized Markov number · Number of solutions of \(x^2 + kx + 1 \equiv 0 \pmod b\)

TheoremGeneralized Markov numbers \(p\) and \(2p\) are unique maxima#●ready to prove

Let \(k\) be a natural number and \(p\) a prime. If \(b\) is a \(k\)-generalized Markov number with \(b = p\) or \(b = 2p\), then \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order.

public theorem_wanted hasUniqueMaxGenMarkovTriple_prime {k b p : ℕ} (hb : IsGenMarkovNumber k b)
    (hp : p.Prime) (hbp : b = p ∨ b = 2 * p) : HasUniqueMaxGenMarkovTriple k b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.6.

Uses 2

Statement usesUnique maximal generalized Markov triple · Generalized Markov number

TheoremUniqueness for prime powers \(p^m\) and \(2p^m\) under conditions on \(k\)#●ready to prove

Let \(k\) and \(m\) be natural numbers with \(m \ge 2\) and let \(p\) be a prime. Suppose that \(k = 2\); or that \(k \ge 4\) is even and \(p^2\) divides neither \(k/2 + 1\) nor \(k/2 - 1\); or that \(k\) is odd and \(p^2\) divides neither \(k + 2\) nor \(k - 2\) in \(\mathbb{Z}\). If \(b\) is a \(k\)-generalized Markov number with \(b = p^m\) or \(b = 2p^m\), then \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order.

public theorem_wanted hasUniqueMaxGenMarkovTriple_prime_pow {k b p m : ℕ}
    (hb : IsGenMarkovNumber k b) (hp : p.Prime) (hm : 2 ≤ m) (hbp : b = p ^ m ∨ b = 2 * p ^ m)
    (hk : k = 2 ∨ (4 ≤ k ∧ Even k ∧ ¬ p ^ 2 ∣ k / 2 + 1 ∧ ¬ p ^ 2 ∣ k / 2 - 1) ∨
      (Odd k ∧ ¬ (p : ℤ) ^ 2 ∣ (k : ℤ) + 2 ∧ ¬ (p : ℤ) ^ 2 ∣ (k : ℤ) - 2)) :
    HasUniqueMaxGenMarkovTriple k b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.7.

Uses 2

Statement usesUnique maximal generalized Markov triple · Generalized Markov number

TheoremUniqueness for odd prime powers \(p^m\) and \(2p^m\) with \(p \nmid k^2 - 4\)#●ready to prove

Let \(k\) and \(m\) be natural numbers with \(m \ge 2\), and let \(p\) be an odd prime that does not divide \(k^2 - 4\) in \(\mathbb{Z}\). If \(b\) is a \(k\)-generalized Markov number with \(b = p^m\) or \(b = 2p^m\), then \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order.

public theorem_wanted hasUniqueMaxGenMarkovTriple_odd_prime_pow {k b p m : ℕ}
    (hb : IsGenMarkovNumber k b) (hp : p.Prime) (hp2 : p ≠ 2) (hm : 2 ≤ m)
    (hbp : b = p ^ m ∨ b = 2 * p ^ m) (hk : ¬ (p : ℤ) ∣ (k : ℤ) ^ 2 - 4) :
    HasUniqueMaxGenMarkovTriple k b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 4.10.

Uses 2

Statement usesUnique maximal generalized Markov triple · Generalized Markov number

TheoremBound on the number of generalized Markov triples with a given maximum#●ready to prove

Let \(k\) be a natural number such that either \(k \ge 4\) is even and \(k/2 + 1\) and \(k/2 - 1\) are squarefree, or \(k\) is odd and the integers \(k + 2\) and \(k - 2\) are squarefree. Let \(b\) be a \(k\)-generalized Markov number that is not divisible by \(4\), and suppose that the number \(n\) of odd primes dividing \(b\) is at least \(1\); equivalently, \(b = p_1^{a_1} \cdots p_n^{a_n}\) or \(b = 2 p_1^{a_1} \cdots p_n^{a_n}\) for distinct odd primes \(p_1, \dots, p_n\) with \(n \ge 1\). Then there are at most \(2^{n-1}\) pairs of natural numbers \((a, c)\) with \(a \le c \le b\) such that \((a, b, c)\) is a \(k\)-generalized Markov triple; that is, \(b\) is the maximum of at most \(2^{n-1}\) such triples up to order.

public theorem_wanted card_maxGenMarkovTriples_le {k b : ℕ}
    (hk : (4 ≤ k ∧ Even k ∧ Squarefree (k / 2 + 1) ∧ Squarefree (k / 2 - 1)) ∨
      (Odd k ∧ Squarefree ((k : ℤ) + 2) ∧ Squarefree ((k : ℤ) - 2)))
    (hb : IsGenMarkovNumber k b) (hb4 : ¬ 4 ∣ b)
    (hn : 1 ≤ (b.primeFactors.filter (· ≠ 2)).card) :
    ((range (b + 1) ×ˢ range (b + 1)).filter fun q =>
        q.1 ≤ q.2 ∧ IsGenMarkovTriple k q.1 b q.2).card ≤
      2 ^ ((b.primeFactors.filter (· ≠ 2)).card - 1)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 4.20.

Uses 2

Statement usesGeneralized Markov number · Generalized Markov triple

TheoremGeneralized Markov triples are pairwise coprime#●ready to prove

If \((a, b, c)\) is a \(k\)-generalized Markov triple, then \(\gcd(a, b) = \gcd(b, c) = \gcd(a, c) = 1\).

public theorem_wanted IsGenMarkovTriple.pairwise_coprime {k a b c : ℕ}
    (h : IsGenMarkovTriple k a b c) :
    Nat.Coprime a b ∧ Nat.Coprime b c ∧ Nat.Coprime a c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 2.3 (citing Gyoda and Matsushita, Corollary 8).

Uses 1

Statement usesGeneralized Markov triple

TheoremThe generalized Markov equation and the generalized second Markov equation#●ready to prove

Let \(k \in \mathbb{N}\) and let \(a, b, c\) be rational numbers. Put \(x = (3 + 3k)a - k\), \(y = (3 + 3k)b - k\) and \(z = (3 + 3k)c - k\). Then \(a^2 + b^2 + c^2 + k(bc + ca + ab) = (3 + 3k)abc\) if and only if \(x^2 + y^2 + z^2 + (k^2 + 2k)(x + y + z) + 2k^3 + 3k^2 = xyz\). The first equation is the \(k\)-generalized Markov equation \(\mathrm{GME}(k)\) and the second the \(k\)-generalized second Markov equation \(\mathrm{GSME}(k)\).

public theorem_wanted genMarkov_iff_genSecondMarkov (k : ℕ) (a b c : ℚ) :
    a ^ 2 + b ^ 2 + c ^ 2 + k * (b * c + c * a + a * b) = (3 + 3 * k) * a * b * c ↔
      let x := (3 + 3 * k) * a - k
      let y := (3 + 3 * k) * b - k
      let z := (3 + 3 * k) * c - k
      x ^ 2 + y ^ 2 + z ^ 2 + ((k : ℚ) ^ 2 + 2 * k) * (x + y + z) + 2 * (k : ℚ) ^ 3 +
          3 * (k : ℚ) ^ 2 = x * y * z

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 2.4.

TheoremVieta jumping for the second generalized Markov equation#●ready to prove

Let \(k\) be a natural number and let \(a, b, c\) be integers with

\[a^2 + b^2 + c^2 + (k^2 + 2k)(a + b + c) + 2k^3 + 3k^2 = abc.\]

Then the triples \((a, ab - c - k^2 - 2k, b)\) and \((b, bc - a - k^2 - 2k, c)\) satisfy the same equation.

public theorem_wanted genSecondMarkov_vieta (k : ℕ) {a b c : ℤ}
    (h : a ^ 2 + b ^ 2 + c ^ 2 + ((k : ℤ) ^ 2 + 2 * k) * (a + b + c) + 2 * (k : ℤ) ^ 3 +
      3 * (k : ℤ) ^ 2 = a * b * c) :
    (let c' := a * b - c - (k : ℤ) ^ 2 - 2 * k;
      a ^ 2 + c' ^ 2 + b ^ 2 + ((k : ℤ) ^ 2 + 2 * k) * (a + c' + b) + 2 * (k : ℤ) ^ 3 +
        3 * (k : ℤ) ^ 2 = a * c' * b) ∧
    (let a' := b * c - a - (k : ℤ) ^ 2 - 2 * k;
      b ^ 2 + a' ^ 2 + c ^ 2 + ((k : ℤ) ^ 2 + 2 * k) * (b + a' + c) + 2 * (k : ℤ) ^ 3 +
        3 * (k : ℤ) ^ 2 = b * a' * c)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 2.6.

TheoremTrace identities in \(\mathrm{SL}(2, \mathbb{Z})\)#●ready to prove

For all \(A, B \in \mathrm{SL}(2, \mathbb{Z})\) we have \(\operatorname{tr} A = \operatorname{tr} A^{-1}\), \(\operatorname{tr}(AB) = \operatorname{tr} A \cdot \operatorname{tr} B - \operatorname{tr}(AB^{-1})\), and \(A^2 = (\operatorname{tr} A) A - I\), where \(I\) is the identity matrix.

public theorem_wanted specialLinearGroup_two_trace_identities
    (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
    Matrix.trace (A : Matrix (Fin 2) (Fin 2) ℤ) =
        Matrix.trace ((A⁻¹ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Matrix (Fin 2) (Fin 2) ℤ) ∧
      Matrix.trace ((A * B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
          Matrix (Fin 2) (Fin 2) ℤ) =
        Matrix.trace (A : Matrix (Fin 2) (Fin 2) ℤ) * Matrix.trace (B : Matrix (Fin 2) (Fin 2) ℤ) -
          Matrix.trace ((A * B⁻¹ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
            Matrix (Fin 2) (Fin 2) ℤ) ∧
      (A : Matrix (Fin 2) (Fin 2) ℤ) ^ 2 =
        Matrix.trace (A : Matrix (Fin 2) (Fin 2) ℤ) • (A : Matrix (Fin 2) (Fin 2) ℤ) - 1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 3.6 (citing Aigner, Lemma 4.2).

TheoremAt most two solutions of \(x^2 + kx + 1 \equiv 0\) modulo a prime#●ready to prove

For every prime \(p\) and every \(k \in \mathbb{N}\), at most two integers \(x\) with \(0 \le x < p\) satisfy \(x^2 + kx + 1 \equiv 0 \pmod p\).

public theorem_wanted genMarkovCongruenceCount_prime_le_two {p : ℕ} (hp : p.Prime) (k : ℕ) :
    genMarkovCongruenceCount k p ≤ 2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.9.

Uses 1

Statement usesNumber of solutions of \(x^2 + kx + 1 \equiv 0 \pmod b\)

TheoremAt most two solutions of \(x^2 + kx + 1 \equiv 0\) modulo an odd prime power#●ready to prove

Let \(p\) be an odd prime, let \(m \ge 2\) and let \(k \in \mathbb{N}\) with \(k^2 - 4 \not\equiv 0 \pmod p\). Then at most two integers \(x\) with \(0 \le x < p^m\) satisfy \(x^2 + kx + 1 \equiv 0 \pmod{p^m}\).

public theorem_wanted genMarkovCongruenceCount_prime_pow_le_two {p m k : ℕ} (hp : p.Prime)
    (hp2 : p ≠ 2) (hm : 2 ≤ m) (hk : ¬ (p : ℤ) ∣ (k : ℤ) ^ 2 - 4) :
    genMarkovCongruenceCount k (p ^ m) ≤ 2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.11.

Uses 1

Statement usesNumber of solutions of \(x^2 + kx + 1 \equiv 0 \pmod b\)

TheoremAn even generalized Markov number forces \(k\) to be even#●ready to prove

Let \(k\) be a natural number. If some \(k\)-generalized Markov number \(b\) is even, then \(k\) is even.

public theorem_wanted even_of_even_genMarkovNumber {k b : ℕ} (hb : IsGenMarkovNumber k b)
    (he : Even b) : Even k

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.13.

Uses 1

Statement usesGeneralized Markov number

TheoremGeneralized Markov numbers divisible by \(4\)#●ready to prove

Let \(k\) be a natural number. If some \(k\)-generalized Markov number is divisible by \(4\), then \(k \equiv 2 \pmod{4}\).

public theorem_wanted mod_four_eq_two_of_four_dvd_genMarkovNumber {k b : ℕ}
    (hb : IsGenMarkovNumber k b) (h4 : 4 ∣ b) : k % 4 = 2

Sources

• Only the first claim of Proposition 4.14 is stated; its "in particular" parity consequence is omitted because its displayed fraction is garbled in the record.
• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 4.14.

Uses 1

Statement usesGeneralized Markov number

TheoremLarge odd primes do not divide \(k^2 - 4\)#●ready to prove

Let \(p\) be an odd prime and \(k\) a natural number. If either \(k \ge 4\) is even and \(p > k/2 + 1\), or \(k\) is odd and \(p > k + 2\), then \(p\) does not divide \(k^2 - 4\).

public theorem_wanted not_dvd_sq_sub_four_of_large_prime {k p : ℕ} (hp : p.Prime)
    (hp2 : p ≠ 2) (h : (4 ≤ k ∧ Even k ∧ k / 2 + 1 < p) ∨ (Odd k ∧ k + 2 < p)) :
    ¬ (p : ℤ) ∣ (k : ℤ) ^ 2 - 4

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 4.15.

TheoremDiscriminant condition for prime-power generalized Markov numbers#●ready to prove

Let \(p\) be an odd prime and \(m \ge 2\), and suppose that some \(k\)-generalized Markov number \(b\) equals \(p^m\) or \(2p^m\). Suppose moreover that either \(k \ge 4\) is even and \(p^2\) divides neither \(k/2 + 1\) nor \(k/2 - 1\), or \(k\) is odd and \(p^2\) divides neither \(k + 2\) nor \(k - 2\). Then \(p\) does not divide \(k^2 - 4\).

As printed (without the Markov-number hypothesis) Proposition 4.16 is false: \(k = 4\), \(p = 3\) satisfy the divisibility conditions (\(9 \nmid 3\), \(9 \nmid 1\)) but \(3 \mid 12\); the paper's proof assumes \(b = p^m\) is a \(k\)-generalized Markov number and uses \(m \ge 2\).

public theorem_wanted not_dvd_sq_sub_four_of_genMarkovNumber_prime_pow {k p m b : ℕ}
    (hp : p.Prime) (hp2 : p ≠ 2) (hm : 2 ≤ m) (hb : IsGenMarkovNumber k b)
    (hbp : b = p ^ m ∨ b = 2 * p ^ m)
    (hk : (4 ≤ k ∧ Even k ∧ ¬ p ^ 2 ∣ k / 2 + 1 ∧ ¬ p ^ 2 ∣ k / 2 - 1) ∨
      (Odd k ∧ ¬ (p : ℤ) ^ 2 ∣ (k : ℤ) + 2 ∧ ¬ (p : ℤ) ^ 2 ∣ (k : ℤ) - 2)) :
    ¬ (p : ℤ) ∣ (k : ℤ) ^ 2 - 4

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 4.16 and its proof.

Uses 1

Statement usesGeneralized Markov number

Theorem2-generalized Markov triples are squares of Markov triples#●ready to prove

If \((a, b, c)\) is a Markov triple, that is, a \(0\)-generalized Markov triple, then \((a^2, b^2, c^2)\) is a \(2\)-generalized Markov triple. Conversely, for every \(2\)-generalized Markov triple \((A, B, C)\) there is a Markov triple \((a, b, c)\) with \(A = a^2\), \(B = b^2\) and \(C = c^2\).

public theorem_wanted genMarkovTriple_two_iff_sq :
    (∀ a b c : ℕ, IsGenMarkovTriple 0 a b c → IsGenMarkovTriple 2 (a ^ 2) (b ^ 2) (c ^ 2)) ∧
      ∀ A B C : ℕ, IsGenMarkovTriple 2 A B C →
        ∃ a b c : ℕ, A = a ^ 2 ∧ B = b ^ 2 ∧ C = c ^ 2 ∧ IsGenMarkovTriple 0 a b c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 4.17 (citing Gyoda and Matsushita, Theorem 2.9).

Uses 1

Statement usesGeneralized Markov triple

TheoremUniqueness criterion for classical Markov numbers#●ready to prove

Let \(b \ne 1, 2\) be a Markov number (a \(0\)-generalized Markov number). If the congruence \(x^2 + 1 \equiv 0 \pmod{b}\) has at most two solutions \(x\) with \(0 \le x < b\), then \(b\) is the maximum of a unique Markov triple up to order.

public theorem_wanted markov_hasUniqueMaxTriple_of_congruenceCount_le_two {b : ℕ}
    (hb : IsGenMarkovNumber 0 b) (hb1 : b ≠ 1) (hb2 : b ≠ 2)
    (hcount : genMarkovCongruenceCount 0 b ≤ 2) : HasUniqueMaxGenMarkovTriple 0 b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.2 (citing Aigner, Corollary 3.17).

Uses 3

Statement usesUnique maximal generalized Markov triple · Generalized Markov number · Number of solutions of \(x^2 + kx + 1 \equiv 0 \pmod b\)

TheoremUniqueness for Markov numbers \(p^m\) and \(2p^m\) with \(p\) an odd prime#●ready to prove

Let \(p\) be an odd prime and \(m \ge 1\). If \(b = p^m\) or \(b = 2p^m\) is a Markov number (a \(0\)-generalized Markov number), then \(b\) is the maximum of a unique Markov triple up to order.

public theorem_wanted markov_hasUniqueMaxTriple_odd_prime_pow {b p m : ℕ}
    (hb : IsGenMarkovNumber 0 b) (hp : p.Prime) (hp2 : p ≠ 2) (hm : 1 ≤ m)
    (hbp : b = p ^ m ∨ b = 2 * p ^ m) : HasUniqueMaxGenMarkovTriple 0 b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.3 (citing Aigner, Corollary 3.20).

Uses 2

Statement usesUnique maximal generalized Markov triple · Generalized Markov number

TheoremMarkov triples with a common characteristic number agree up to order#●ready to prove

Let \(m \ge 5\) and let \((m, m_2, m_3)\) and \((m, n_2, n_3)\) be Markov triples (that is, \(0\)-generalized Markov triples) with \(m_2, m_3, n_2, n_3 \le m\). Suppose some integer \(x\) with \(0 < x < m\) satisfies \(m_2 x \equiv \pm m_3 \pmod{m}\) and \(n_2 x \equiv \pm n_3 \pmod{m}\), where the two signs are chosen independently. Then \((m_2, m_3) = (n_2, n_3)\) or \((m_2, m_3) = (n_3, n_2)\).

public theorem_wanted markov_eq_of_characteristic_number_eq {m m₂ m₃ n₂ n₃ x : ℕ}
    (hm : 5 ≤ m) (h₁ : IsGenMarkovTriple 0 m m₂ m₃) (h₂ : IsGenMarkovTriple 0 m n₂ n₃)
    (hm₁ : m₂ ≤ m ∧ m₃ ≤ m) (hm₂ : n₂ ≤ m ∧ n₃ ≤ m) (hx : 0 < x ∧ x < m)
    (hu₁ : (m : ℤ) ∣ m₂ * x - m₃ ∨ (m : ℤ) ∣ m₂ * x + m₃)
    (hu₂ : (m : ℤ) ∣ n₂ * x - n₃ ∨ (m : ℤ) ∣ n₂ * x + n₃) :
    (m₂ = n₂ ∧ m₃ = n₃) ∨ (m₂ = n₃ ∧ m₃ = n₂)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 1.11 (citing Aigner, Proposition 3.15).

Uses 1

Statement usesGeneralized Markov triple

DefinitionVieta jumping of generalized Markov triples#✓fully proved

For a natural number \(k\), the left Vieta jumping sends a triple \((a, b, c)\) of natural numbers to \((a, \lfloor (a^2 + kab + b^2)/c \rfloor, b)\) and the right Vieta jumping sends it to \((b, \lfloor (b^2 + kbc + c^2)/a \rfloor, c)\), where division by \(0\) gives \(0\). The left jumping is indexed by the boolean value false and the right one by true.

public def genMarkovVieta (k : ℕ) : Bool → ℕ × ℕ × ℕ → ℕ × ℕ × ℕ
  | false, (a, b, c) => (a, (a ^ 2 + k * a * b + b ^ 2) / c, b)
  | true, (a, b, c) => (b, (b ^ 2 + k * b * c + c ^ 2) / a, c)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Used by 4

Used byCohn steps reach every classical Cohn triple whose middle entry is largest · Cohn steps reach every generalized Cohn triple whose middle entry is largest · The wide generalized Markov tree · Children in the wide generalized Markov tree are Vieta jumpings

DefinitionThe wide generalized Markov tree#✓fully proved

Fix a natural number \(k\). The wide \(k\)-generalized Markov tree \(\mathrm{WMT}(k)\) is the binary tree of triples of natural numbers with root \((1, 1, 1)\) in which a vertex \((a, b, c)\) has left child \((a, \lfloor (a^2 + kab + b^2)/c \rfloor, b)\) and right child \((b, \lfloor (b^2 + kbc + c^2)/a \rfloor, c)\), the left and right Vieta jumpings. For a path \(w\), a finite sequence of left and right steps, the vertex of \(\mathrm{WMT}(k)\) at \(w\) is the triple reached from the root by taking the steps of \(w\) in order; the empty path gives the root.

The quotients are divisions of natural numbers, rounded down, with division by \(0\) giving \(0\).

public def wideGenMarkovTree (k : ℕ) (w : List Bool) : ℕ × ℕ × ℕ :=
  w.foldl (fun t d => genMarkovVieta k d t) (1, 1, 1)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Uses 1 · Used by 4

Statement usesVieta jumping of generalized Markov triples

Used byGeneralized Markov tree · Vertices of the wide generalized Cohn tree are generalized Cohn triples · Children in the wide generalized Markov tree are Vieta jumpings · Generalized Markov triples in the wide Markov tree

DefinitionGeneralized Markov tree#✓fully proved

For a natural number \(k\) and a finite sequence \(w\) of left and right steps, the vertex of the \(k\)-generalized Markov tree \(MT(k)\) at \(w\) is the vertex of the wide \(k\)-generalized Markov tree \(WMT(k)\) reached from its root by one left step followed by the steps of \(w\) in order. Thus \(MT(k)\) is the full subtree of \(WMT(k)\) rooted at the left child of the root.

public def genMarkovTree (k : ℕ) (w : List Bool) : ℕ × ℕ × ℕ :=
  wideGenMarkovTree k (false :: w)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Uses 1 · Used by 11

Statement usesThe wide generalized Markov tree

Used byVertices of the generalized Cohn tree are Cohn triples over the Markov tree · Shape of the generalized Cohn matrices for \(\ell = -k\) · The characteristic number is less than \(m_t/2 - k\) · The characteristic number solves \(m_r x \equiv m_s \pmod{m_t}\) · The characteristic number solves \(x^2 + kx + 1 \equiv 0 \pmod{m_t}\) · Vertices of the generalized Markov tree · Root of the generalized Markov tree · Left child of the root of the classical Markov tree · Vertices of the second generalized Markov tree · Fraction labeling of generalized Markov numbers · The fraction \(1/1\) labels \(k + 2\)

TheoremChildren in the wide generalized Markov tree are Vieta jumpings#✓fully proved

For every natural number \(k\), every path \(w\) and every direction \(d\) (left or right), the vertex of the wide \(k\)-generalized Markov tree \(\mathrm{WMT}(k)\) at the path \(w\) followed by one step in direction \(d\) is the image of the vertex at \(w\) under the Vieta jumping in direction \(d\).

public theorem wideGenMarkovTree_append_singleton (k : ℕ) (w : List Bool) (d : Bool) :
    wideGenMarkovTree k (w ++ [d]) = genMarkovVieta k d (wideGenMarkovTree k w)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Uses 2

Statement usesVieta jumping of generalized Markov triples · The wide generalized Markov tree

TheoremRoot of the generalized Markov tree#✓fully proved

For every natural number \(k\), the root of the \(k\)-generalized Markov tree \(MT(k)\), its vertex at the empty path, is \((1, k + 2, 1)\).

public theorem genMarkovTree_nil (k : ℕ) : genMarkovTree k [] = (1, k + 2, 1)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 4.

Uses 1 · Used by 1

Statement usesGeneralized Markov tree

Used byThe fraction \(1/1\) labels \(k + 2\)

TheoremLeft child of the root of the classical Markov tree#✓fully proved

For \(k = 0\), the vertex of the Markov tree \(MT(0)\) reached from the root by one left step is \((1, 5, 2)\).

public theorem genMarkovTree_zero_false : genMarkovTree 0 [false] = (1, 5, 2)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Uses 1

Statement usesGeneralized Markov tree

TheoremGeneralized Markov triples in the wide Markov tree#●ready to prove

Let \(k\) be a natural number. Every vertex of the wide \(k\)-generalized Markov tree \(\mathrm{WMT}(k)\) is a \(k\)-generalized Markov triple. Moreover, every \(k\)-generalized Markov triple \((a, b, c)\) with \(a < b\) and \(c < b\) is the vertex of \(\mathrm{WMT}(k)\) at exactly one path that starts with a left step, and at exactly one path that starts with a right step.

public theorem_wanted wideGenMarkovTree_isGenMarkovTriple_and_twice (k : ℕ) :
    (∀ w, IsGenMarkovTriple k (wideGenMarkovTree k w).1 (wideGenMarkovTree k w).2.1
      (wideGenMarkovTree k w).2.2) ∧
    ∀ a b c, IsGenMarkovTriple k a b c → a < b → c < b →
      (∃! w, wideGenMarkovTree k (false :: w) = (a, b, c)) ∧
        ∃! w, wideGenMarkovTree k (true :: w) = (a, b, c)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 2.1 (citing Gyoda and Matsushita, Theorem 1).

Uses 2

Statement usesGeneralized Markov triple · The wide generalized Markov tree

TheoremVertices of the generalized Markov tree#●ready to prove

For every natural number \(k\), every vertex of the \(k\)-generalized Markov tree \(MT(k)\) is a \(k\)-generalized Markov triple, and for every \(k\)-generalized Markov triple \((a, b, c)\) with \(a < b\) and \(c < b\) there is exactly one path \(w\) such that the vertex of \(MT(k)\) at \(w\) is \((a, b, c)\).

public theorem_wanted genMarkovTree_isGenMarkovTriple_and_once (k : ℕ) :
    (∀ w, IsGenMarkovTriple k (genMarkovTree k w).1 (genMarkovTree k w).2.1
      (genMarkovTree k w).2.2) ∧
    ∀ a b c, IsGenMarkovTriple k a b c → a < b → c < b → ∃! w, genMarkovTree k w = (a, b, c)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 2.2.

Uses 2

Statement usesGeneralized Markov triple · Generalized Markov tree

TheoremVieta jumping identities for generalized Markov triples#●ready to prove

If \((a, b, c)\) is a \(k\)-generalized Markov triple, then, as integers, \(a^2 + kab + b^2 = c\,((3 + 3k)ab - c - k(a + b))\) and \(b^2 + kbc + c^2 = a\,((3 + 3k)bc - a - k(b + c))\).

public theorem_wanted IsGenMarkovTriple.vieta_eq {k a b c : ℕ} (h : IsGenMarkovTriple k a b c) :
    ((a : ℤ) ^ 2 + k * a * b + b ^ 2 = c * ((3 + 3 * k) * a * b - c - k * (a + b))) ∧
      ((b : ℤ) ^ 2 + k * b * c + c ^ 2 = a * ((3 + 3 * k) * b * c - a - k * (b + c)))

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2 (display after Corollary 2.2).

Uses 1

Statement usesGeneralized Markov triple

DefinitionInduced solution of the generalized second Markov equation#✓fully proved

For a natural number \(k\), a triple \((a, b, c)\) of integers is an induced positive solution of the \(k\)-generalized second Markov equation \(\mathrm{GSME}(k)\) when \(a, b, c > 0\),

\[a^2 + b^2 + c^2 + (k^2 + 2k)(a + b + c) + 2k^3 + 3k^2 = abc,\]

and \(3 + 3k\) divides each of \(a + k\), \(b + k\) and \(c + k\).

Equivalently, \((a + k)/(3 + 3k)\), \((b + k)/(3 + 3k)\) and \((c + k)/(3 + 3k)\) are integers; they are automatically positive since \(a, b, c > 0\).

public def IsInducedGenSecondMarkovSolution (k : ℕ) (a b c : ℤ) : Prop :=
  0 < a ∧ 0 < b ∧ 0 < c ∧
    a ^ 2 + b ^ 2 + c ^ 2 + ((k : ℤ) ^ 2 + 2 * k) * (a + b + c) + 2 * (k : ℤ) ^ 3 +
      3 * (k : ℤ) ^ 2 = a * b * c ∧
    (3 + 3 * (k : ℤ)) ∣ a + k ∧ (3 + 3 * (k : ℤ)) ∣ b + k ∧ (3 + 3 * (k : ℤ)) ∣ c + k

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Used by 3

Used byVertices of the second generalized Markov tree · The root induced solution of the generalized second Markov equation · Vieta jumping preserves induced solutions of the generalized second Markov equation

TheoremThe root induced solution of the generalized second Markov equation#✓fully proved

For every natural number \(k\), the triple \((3 + 2k, 3 + 2k, 3 + 2k)\), the image of \((1, 1, 1)\) under \(x \mapsto (3 + 3k)x - k\), is an induced positive solution of the \(k\)-generalized second Markov equation \(\mathrm{GSME}(k)\).

public theorem isInducedGenSecondMarkovSolution_root (k : ℕ) :
    IsInducedGenSecondMarkovSolution k (3 + 2 * k) (3 + 2 * k) (3 + 2 * k)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 2.

Uses 1

Statement usesInduced solution of the generalized second Markov equation

TheoremVieta jumping preserves induced solutions of the generalized second Markov equation#●ready to prove

If \((a, b, c)\) is an induced solution of the \(k\)-generalized second Markov equation \(\mathrm{GSME}(k)\), then so are \((a, ab - c - k^2 - 2k, b)\) and \((b, bc - a - k^2 - 2k, c)\).

public theorem_wanted IsInducedGenSecondMarkovSolution.vieta {k : ℕ} {a b c : ℤ}
    (h : IsInducedGenSecondMarkovSolution k a b c) :
    IsInducedGenSecondMarkovSolution k a (a * b - c - (k : ℤ) ^ 2 - 2 * k) b ∧
      IsInducedGenSecondMarkovSolution k b (b * c - a - (k : ℤ) ^ 2 - 2 * k) c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 2.7.

Uses 1

Statement usesInduced solution of the generalized second Markov equation

TheoremVertices of the second generalized Markov tree#●ready to prove

For a natural number \(k\), let \(SMT(k)\) be the tree obtained from the \(k\)-generalized Markov tree \(MT(k)\) by replacing each vertex \((a, b, c)\) with the integer triple \(((3 + 3k)a - k, (3 + 3k)b - k, (3 + 3k)c - k)\). Every vertex of \(SMT(k)\) is an induced solution of the \(k\)-generalized second Markov equation, and for every induced solution \((a, b, c)\) with \(a < b\) and \(c < b\) there is exactly one path \(w\) such that the vertex of \(SMT(k)\) at \(w\) is \((a, b, c)\).

public theorem_wanted genSecondMarkovTree_induced_and_once (k : ℕ) :
    (∀ w, IsInducedGenSecondMarkovSolution k ((3 + 3 * k) * ((genMarkovTree k w).1 : ℤ) - k)
      ((3 + 3 * k) * ((genMarkovTree k w).2.1 : ℤ) - k)
      ((3 + 3 * k) * ((genMarkovTree k w).2.2 : ℤ) - k)) ∧
    ∀ a b c, IsInducedGenSecondMarkovSolution k a b c → a < b → c < b →
      ∃! w, ((3 + 3 * k) * ((genMarkovTree k w).1 : ℤ) - k,
        (3 + 3 * k) * ((genMarkovTree k w).2.1 : ℤ) - k,
        (3 + 3 * k) * ((genMarkovTree k w).2.2 : ℤ) - k) = (a, b, c)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 2.8.

Uses 2

Statement usesInduced solution of the generalized second Markov equation · Generalized Markov tree

DefinitionThe matrix \(S\) of the generalized Cohn triple relation#✓fully proved

For a natural number \(k\), \(S\) is the \(2 \times 2\) integer matrix

\[S = \begin{pmatrix} k & 0 \\ 3k^2 + 3k & k \end{pmatrix}.\]

It is the matrix in the relation \(Q = PR - S\) that defines \(k\)-generalized Cohn triples.

public def genCohnS (k : ℕ) : Matrix (Fin 2) (Fin 2) ℤ :=
  !![(k : ℤ), 0; 3 * (k : ℤ) ^ 2 + 3 * k, k]

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Definition 3.2.

Used by 6

Used byThe matrix \(S\) vanishes for \(k = 0\) · One step of the wide generalized Cohn tree · Generalized Cohn triple · Generalized Cohn triples give generalized Markov triples · Parent triples of a generalized Cohn triple · Children of a generalized Cohn triple

TheoremThe matrix \(S\) vanishes for \(k = 0\)#✓fully proved

For \(k = 0\), the matrix \(S\) of the generalized Cohn triple relation is the zero \(2 \times 2\) matrix, so the relation \(Q = PR - S\) reduces to the classical Cohn relation \(Q = PR\).

public theorem genCohnS_zero : genCohnS 0 = 0

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 1.3.

Uses 1

Statement usesThe matrix \(S\) of the generalized Cohn triple relation

DefinitionGeneralized Cohn matrices#✓fully proved

Let \(k\) be a natural number. An integer \(2 \times 2\) matrix \(P = (p_{ij})\) is a \(k\)-generalized Cohn matrix if \(\det P = 1\), its entry \(p_{12}\) is a \(k\)-generalized Markov number, and its trace equals \((3 + 3k) p_{12} - k\).

public def IsGenCohnMatrix (k : ℕ) (P : Matrix (Fin 2) (Fin 2) ℤ) : Prop :=
  P.det = 1 ∧ ∃ n : ℕ, P 0 1 = n ∧ IsGenMarkovNumber k n ∧ P.trace = (3 + 3 * k) * n - k

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Definition 3.1.

Uses 1 · Used by 3

Statement usesGeneralized Markov number

Used byGeneralized Cohn triple · Generalized Cohn triples give generalized Markov triples · A product identity for generalized Cohn matrices

DefinitionGeneralized Cohn triple#✓fully proved

Let \(k\) be a natural number and let \(S\) be the integer matrix with rows \((k, 0)\) and \((3k^2 + 3k, k)\). A triple \((P, Q, R)\) of integer \(2 \times 2\) matrices is a \(k\)-generalized Cohn triple associated with natural numbers \((a, b, c)\) when \(P\), \(Q\) and \(R\) are \(k\)-generalized Cohn matrices, \(Q = PR - S\), the \((1, 2)\)-entries of \(P\), \(Q\) and \(R\) are \(a\), \(b\) and \(c\) respectively, and \((a, b, c)\) is a \(k\)-generalized Markov triple.

public def IsGenCohnTriple (k : ℕ) (P Q R : Matrix (Fin 2) (Fin 2) ℤ) (a b c : ℕ) : Prop :=
  IsGenCohnMatrix k P ∧ IsGenCohnMatrix k Q ∧ IsGenCohnMatrix k R ∧ Q = P * R - genCohnS k ∧
    P 0 1 = a ∧ Q 0 1 = b ∧ R 0 1 = c ∧ IsGenMarkovTriple k a b c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Definition 3.2.

Uses 3 · Used by 10

Statement usesGeneralized Cohn matrices · Generalized Markov triple · The matrix \(S\) of the generalized Cohn triple relation

Used byCohn steps reach every classical Cohn triple whose middle entry is largest · Cohn triples sit at a unique vertex of a Cohn tree · Vertices of the generalized Cohn tree are Cohn triples over the Markov tree · Cohn steps reach every generalized Cohn triple whose middle entry is largest · Generalized Cohn triples associated with \((1, 1, 1)\) · Generalized Cohn triples give generalized Markov triples · Generalized Cohn triples with largest middle entry lie in wide generalized Cohn trees · Parent triples of a generalized Cohn triple · Children of a generalized Cohn triple · Vertices of the wide generalized Cohn tree are generalized Cohn triples

TheoremGeneralized Cohn triples give generalized Markov triples#✓fully proved

Let \(k\) be a natural number. If \((P, Q, R)\) is a \(k\)-generalized Cohn triple associated with \((a, b, c)\), then \((a, b, c)\) is a \(k\)-generalized Markov triple.

public theorem IsGenCohnTriple.isGenMarkovTriple {k : ℕ} {P Q R : Matrix (Fin 2) (Fin 2) ℤ}
    {a b c : ℕ} (h : IsGenCohnTriple k P Q R a b c) : IsGenMarkovTriple k a b c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Definition 3.2.

Uses 4

Statement usesGeneralized Cohn triple · Generalized Markov triple

Proof usesGeneralized Cohn matrices · The matrix \(S\) of the generalized Cohn triple relation

DefinitionThe matrix \(P_{1;\ell}\)#✓fully proved

For a natural number \(k\) and an integer \(\ell\), \(P_{1;\ell}\) is the integer \(2 \times 2\) matrix with first row \((\ell, 1)\) and second row \((-\ell^2 + 2k\ell + 3\ell - 1, -\ell + 2k + 3)\).

public def genCohnP1 (k : ℕ) (ℓ : ℤ) : Matrix (Fin 2) (Fin 2) ℤ :=
  !![ℓ, 1; -ℓ ^ 2 + 2 * k * ℓ + 3 * ℓ - 1, -ℓ + 2 * k + 3]

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Used by 4

Used byThe matrices \(P_{1;\ell}\), \(Q_{1;\ell}\) and \(R_{1;\ell}\) have determinant \(1\) · Generalized Cohn triples associated with \((1, 1, 1)\) · The wide generalized Cohn tree · Children in the wide generalized Cohn tree

DefinitionThe matrix \(Q_{1;\ell}\)#✓fully proved

For a natural number \(k\) and an integer \(\ell\), \(Q_{1;\ell}\) is the \(2 \times 2\) integer matrix

\[\begin{pmatrix} k + \ell + 1 & 1 \\ k^2 - \ell^2 + 3k + \ell + 1 & k - \ell + 2 \end{pmatrix}.\]

public def genCohnQ1 (k : ℕ) (ℓ : ℤ) : Matrix (Fin 2) (Fin 2) ℤ :=
  !![k + ℓ + 1, 1; (k : ℤ) ^ 2 - ℓ ^ 2 + 3 * k + ℓ + 1, k - ℓ + 2]

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Used by 4

Used byThe matrices \(P_{1;\ell}\), \(Q_{1;\ell}\) and \(R_{1;\ell}\) have determinant \(1\) · Generalized Cohn triples associated with \((1, 1, 1)\) · The wide generalized Cohn tree · Children in the wide generalized Cohn tree

DefinitionThe matrix \(R_{1;\ell}\)#✓fully proved

For a natural number \(k\) and an integer \(\ell\), \(R_{1;\ell}\) is the \(2 \times 2\) integer matrix

\[\begin{pmatrix} 2k + \ell + 2 & 1 \\ -\ell^2 - 2k\ell + 2k - \ell + 1 & -\ell + 1 \end{pmatrix}.\]

public def genCohnR1 (k : ℕ) (ℓ : ℤ) : Matrix (Fin 2) (Fin 2) ℤ :=
  !![2 * k + ℓ + 2, 1; -ℓ ^ 2 - 2 * k * ℓ + 2 * k - ℓ + 1, -ℓ + 1]

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Used by 4

Used byThe matrices \(P_{1;\ell}\), \(Q_{1;\ell}\) and \(R_{1;\ell}\) have determinant \(1\) · Generalized Cohn triples associated with \((1, 1, 1)\) · The wide generalized Cohn tree · Children in the wide generalized Cohn tree

TheoremThe matrices \(P_{1;\ell}\), \(Q_{1;\ell}\) and \(R_{1;\ell}\) have determinant \(1\)#✓fully proved

For every natural number \(k\) and every integer \(\ell\), the \(2 \times 2\) integer matrices \(P_{1;\ell}\), \(Q_{1;\ell}\) and \(R_{1;\ell}\) (which depend on \(k\)) all have determinant \(1\).

public theorem genCohnPQR1_det (k : ℕ) (ℓ : ℤ) :
    (genCohnP1 k ℓ).det = 1 ∧ (genCohnQ1 k ℓ).det = 1 ∧ (genCohnR1 k ℓ).det = 1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Uses 3

Statement usesThe matrix \(P_{1;\ell}\) · The matrix \(Q_{1;\ell}\) · The matrix \(R_{1;\ell}\)

DefinitionOne step of the wide generalized Cohn tree#✓fully proved

Fix a natural number \(k\) and let \(S\) be the matrix of the \(k\)-generalized Cohn triple relation. On triples \((P, Q, R)\) of \(2 \times 2\) integer matrices, the left step (encoded by the Boolean false) sends \((P, Q, R)\) to its left child \((P, PQ - S, Q)\), and the right step (encoded by true) sends it to its right child \((Q, QR - S, R)\).

public def genCohnStep (k : ℕ) : Bool →
    Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ →
      Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ
  | false, (P, Q, _) => (P, P * Q - genCohnS k, Q)
  | true, (_, Q, R) => (Q, Q * R - genCohnS k, R)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Uses 1 · Used by 4

Statement usesThe matrix \(S\) of the generalized Cohn triple relation

Used byCohn steps reach every classical Cohn triple whose middle entry is largest · Paths of generalized Cohn steps · Cohn steps reach every generalized Cohn triple whose middle entry is largest · Children in the wide generalized Cohn tree

DefinitionPaths of generalized Cohn steps#✓fully proved

Fix a natural number \(k\) and let \(S\) be the integer \(2 \times 2\) matrix with rows \((k, 0)\) and \((3k^2 + 3k, k)\). For a triple \(T\) of integer \(2 \times 2\) matrices and a path \(w\), a finite sequence of left and right moves, this is the triple obtained from \(T\) by applying the moves of \(w\) in order, where a left move sends \((P, Q, R)\) to \((P, PQ - S, Q)\) and a right move sends \((P, Q, R)\) to \((Q, QR - S, R)\).

public def genCohnPath (k : ℕ)
    (T : Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ)
    (w : List Bool) :
    Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ :=
  w.foldl (fun T d => genCohnStep k d T) T

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.10.

Uses 1 · Used by 3

Statement usesOne step of the wide generalized Cohn tree

Used byCohn steps reach every classical Cohn triple whose middle entry is largest · Cohn steps reach every generalized Cohn triple whose middle entry is largest · The wide generalized Cohn tree

DefinitionThe wide generalized Cohn tree#✓fully proved

Fix a natural number \(k\) and an integer \(\ell\), and let \(S = \begin{pmatrix} k & 0 \\ 3k^2 + 3k & k \end{pmatrix}\). The wide \(k\)-generalized Cohn tree \(\mathrm{WGCT}(k, \ell)\) is the binary tree of triples of \(2 \times 2\) integer matrices whose root is \((P_{1;\ell}, Q_{1;\ell}, R_{1;\ell})\), where

\[P_{1;\ell}=\begin{pmatrix}\ell & 1\\ -\ell^2+2k\ell+3\ell-1 & -\ell+2k+3\end{pmatrix},\]

\[Q_{1;\ell}=\begin{pmatrix}k+\ell+1 & 1\\ k^2-\ell^2+3k+\ell+1 & k-\ell+2\end{pmatrix},\]

\[R_{1;\ell}=\begin{pmatrix}2k+\ell+2 & 1\\ -\ell^2-2k\ell+2k-\ell+1 & -\ell+1\end{pmatrix},\]

and in which a vertex \((P, Q, R)\) has left child \((P, PQ - S, Q)\) and right child \((Q, QR - S, R)\). For a path \(w\), a finite sequence of left and right steps, the vertex of \(\mathrm{WGCT}(k, \ell)\) at \(w\) is the triple reached from the root by taking the steps of \(w\) in order; the empty path gives the root.

public def wideGenCohnTree (k : ℕ) (ℓ : ℤ) (w : List Bool) :
    Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ :=
  genCohnPath k (genCohnP1 k ℓ, genCohnQ1 k ℓ, genCohnR1 k ℓ) w

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Uses 4 · Used by 5

Statement usesThe matrix \(P_{1;\ell}\) · Paths of generalized Cohn steps · The matrix \(Q_{1;\ell}\) · The matrix \(R_{1;\ell}\)

Used byThe \(k\)-generalized Cohn tree · Generalized Cohn triples with largest middle entry lie in wide generalized Cohn trees · Children in the wide generalized Cohn tree · Vertices of the wide generalized Cohn tree are generalized Cohn triples · Distinct paths give distinct middle matrices in the wide generalized Cohn tree

DefinitionThe \(k\)-generalized Cohn tree#✓fully proved

For \(k \in \mathbb{N}\) and \(\ell \in \mathbb{Z}\), the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, \ell)\) is the full subtree of the wide \(k\)-generalized Cohn tree \(\mathrm{WGCT}(k, \ell)\) rooted at the left child of its root. For a finite sequence \(w\) of left and right moves, this is the vertex of \(\mathrm{GCT}(k, \ell)\) reached from its root along \(w\), that is, the vertex of \(\mathrm{WGCT}(k, \ell)\) reached from the root of \(\mathrm{WGCT}(k, \ell)\) by one left move followed by the moves of \(w\).

public def genCohnTree (k : ℕ) (ℓ : ℤ) (w : List Bool) :
    Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ × Matrix (Fin 2) (Fin 2) ℤ :=
  wideGenCohnTree k ℓ (false :: w)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Uses 1 · Used by 7

Statement usesThe wide generalized Cohn tree

Used byCohn triples sit at a unique vertex of a Cohn tree · Vertices of the generalized Cohn tree are Cohn triples over the Markov tree · Positive corner entry of the generalized Cohn tree for \(\ell = -k\) · Shape of the generalized Cohn matrices for \(\ell = -k\) · Middle matrices of the generalized Cohn tree are distinct · Fraction labels of generalized Cohn matrices · The middle matrix of the root of \(\mathrm{GCT}(k, \ell)\) has label \(1/1\)

TheoremChildren in the wide generalized Cohn tree#✓fully proved

Let \(k\) be a natural number, \(\ell\) an integer, and \(S\) the integer matrix with rows \((k, 0)\) and \((3k^2 + 3k, k)\). For every path \(w\) in the wide \(k\)-generalized Cohn tree \(\mathrm{WGCT}(k, \ell)\), if \((P, Q, R)\) is the vertex at \(w\), then the vertex at \(w\) followed by a left step is \((P, PQ - S, Q)\) and the vertex at \(w\) followed by a right step is \((Q, QR - S, R)\); that is, each child is obtained from its parent by one generalized Cohn step.

public theorem wideGenCohnTree_append_singleton (k : ℕ) (ℓ : ℤ) (w : List Bool) (d : Bool) :
    wideGenCohnTree k ℓ (w ++ [d]) = genCohnStep k d (wideGenCohnTree k ℓ w)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.1.

Uses 5

Statement usesOne step of the wide generalized Cohn tree · The wide generalized Cohn tree

Proof usesThe matrix \(P_{1;\ell}\) · The matrix \(Q_{1;\ell}\) · The matrix \(R_{1;\ell}\)

TheoremCohn steps reach every classical Cohn triple whose middle entry is largest#●ready to prove

Call a \(0\)-generalized Cohn triple a Cohn triple; for \(k = 0\) the matrix \(S\) of the generalized Cohn relation is zero, so the relation reads \(Q = PR\). Call \((P, Q, R) \mapsto (P, PQ, Q)\) the left step and \((P, Q, R) \mapsto (Q, QR, R)\) the right step. First, if \((P, Q, R)\) is a Cohn triple associated with \((a, b, c)\) and \(a \le b\), \(c \le b\), then \((P, Q, R)\) is obtained by applying finitely many left and right steps to some Cohn triple associated with \((1, 1, 1)\). Second, if \((P, Q, R)\) is a Cohn triple associated with \((a, b, c)\), then the \((1, 2)\)-entries of the left step \((P, PQ, Q)\) are \((a, \lfloor (a^2 + b^2)/c \rfloor, b)\) and those of the right step \((Q, QR, R)\) are \((b, \lfloor (b^2 + c^2)/a \rfloor, c)\): on \((1, 2)\)-entries the steps are the left and right Vieta jumpings of the Markov triple \((a, b, c)\).

public theorem_wanted cohnTriple_reachable :
    (∀ P Q R a b c, IsGenCohnTriple 0 P Q R a b c → a ≤ b → c ≤ b →
      ∃ P₀ Q₀ R₀ w, IsGenCohnTriple 0 P₀ Q₀ R₀ 1 1 1 ∧ genCohnPath 0 (P₀, Q₀, R₀) w = (P, Q, R)) ∧
    ∀ P Q R a b c d, IsGenCohnTriple 0 P Q R a b c →
      (genCohnStep 0 d (P, Q, R)).1 0 1 = (genMarkovVieta 0 d (a, b, c)).1 ∧
        (genCohnStep 0 d (P, Q, R)).2.1 0 1 = (genMarkovVieta 0 d (a, b, c)).2.1 ∧
        (genCohnStep 0 d (P, Q, R)).2.2 0 1 = (genMarkovVieta 0 d (a, b, c)).2.2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.9 (citing Aigner, Theorem 4.7).

Uses 4

Statement usesGeneralized Cohn triple · Paths of generalized Cohn steps · One step of the wide generalized Cohn tree · Vieta jumping of generalized Markov triples

TheoremCohn steps reach every generalized Cohn triple whose middle entry is largest#●ready to prove

Let \(k \in \mathbb{N}\) and let \(S\) be the integer matrix with rows \((k, 0)\) and \((3k^2 + 3k, k)\). Call \((P, Q, R) \mapsto (P, PQ - S, Q)\) the left step and \((P, Q, R) \mapsto (Q, QR - S, R)\) the right step. First, if \((P, Q, R)\) is a \(k\)-generalized Cohn triple associated with \((a, b, c)\) and \(a \le b\), \(c \le b\), then \((P, Q, R)\) is obtained by applying finitely many left and right steps to some \(k\)-generalized Cohn triple associated with \((1, 1, 1)\). Second, if \((P, Q, R)\) is a \(k\)-generalized Cohn triple associated with \((a, b, c)\), then the \((1, 2)\)-entries of the left step \((P, PQ - S, Q)\) are \((a, \lfloor (a^2 + kab + b^2)/c \rfloor, b)\) and those of the right step \((Q, QR - S, R)\) are \((b, \lfloor (b^2 + kbc + c^2)/a \rfloor, c)\): on \((1, 2)\)-entries the steps are the left and right Vieta jumpings of \((a, b, c)\).

public theorem_wanted genCohnTriple_reachable (k : ℕ) :
    (∀ P Q R a b c, IsGenCohnTriple k P Q R a b c → a ≤ b → c ≤ b →
      ∃ P₀ Q₀ R₀ w, IsGenCohnTriple k P₀ Q₀ R₀ 1 1 1 ∧ genCohnPath k (P₀, Q₀, R₀) w = (P, Q, R)) ∧
    ∀ P Q R a b c d, IsGenCohnTriple k P Q R a b c →
      (genCohnStep k d (P, Q, R)).1 0 1 = (genMarkovVieta k d (a, b, c)).1 ∧
        (genCohnStep k d (P, Q, R)).2.1 0 1 = (genMarkovVieta k d (a, b, c)).2.1 ∧
        (genCohnStep k d (P, Q, R)).2.2 0 1 = (genMarkovVieta k d (a, b, c)).2.2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 1.10.

Uses 4

Statement usesGeneralized Cohn triple · Paths of generalized Cohn steps · One step of the wide generalized Cohn tree · Vieta jumping of generalized Markov triples

TheoremGeneralized Cohn triples associated with \((1, 1, 1)\)#●ready to prove

Let \(k\) be a natural number. For an integer \(\ell\), let \(P_{1;\ell}\) be the integer matrix with rows \((\ell, 1)\) and \((-\ell^2 + 2k\ell + 3\ell - 1, -\ell + 2k + 3)\), let \(Q_{1;\ell}\) be the one with rows \((k + \ell + 1, 1)\) and \((k^2 - \ell^2 + 3k + \ell + 1, k - \ell + 2)\), and let \(R_{1;\ell}\) be the one with rows \((2k + \ell + 2, 1)\) and \((-\ell^2 - 2k\ell + 2k - \ell + 1, -\ell + 1)\). Then for every integer \(\ell\), \((P_{1;\ell}, Q_{1;\ell}, R_{1;\ell})\) is a \(k\)-generalized Cohn triple associated with \((1, 1, 1)\). Conversely, if \((P, Q, R)\) is a \(k\)-generalized Cohn triple associated with \((1, 1, 1)\), then there is an integer \(\ell\) with \(P = P_{1;\ell}\), \(Q = Q_{1;\ell}\) and \(R = R_{1;\ell}\).

public theorem_wanted isGenCohnTriple_one_iff (k : ℕ) :
    (∀ ℓ, IsGenCohnTriple k (genCohnP1 k ℓ) (genCohnQ1 k ℓ) (genCohnR1 k ℓ) 1 1 1) ∧
    ∀ P Q R, IsGenCohnTriple k P Q R 1 1 1 →
      ∃ ℓ, P = genCohnP1 k ℓ ∧ Q = genCohnQ1 k ℓ ∧ R = genCohnR1 k ℓ

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 3.4.

Uses 4

Statement usesGeneralized Cohn triple · The matrix \(P_{1;\ell}\) · The matrix \(Q_{1;\ell}\) · The matrix \(R_{1;\ell}\)

TheoremChildren of a generalized Cohn triple#●ready to prove

Let \(k\) be a natural number, let \(S\) be the integer matrix with rows \((k, 0)\) and \((3k^2 + 3k, k)\), and let \((P, Q, R)\) be a \(k\)-generalized Cohn triple associated with \((a, b, c)\). Then \((P, PQ - S, Q)\) is a \(k\)-generalized Cohn triple associated with \((a, \lfloor (a^2 + kab + b^2)/c \rfloor, b)\), and \((Q, QR - S, R)\) is a \(k\)-generalized Cohn triple associated with \((b, \lfloor (b^2 + kbc + c^2)/a \rfloor, c)\).

public theorem_wanted IsGenCohnTriple.step {k a b c : ℕ} {P Q R : Matrix (Fin 2) (Fin 2) ℤ}
    (h : IsGenCohnTriple k P Q R a b c) :
    IsGenCohnTriple k P (P * Q - genCohnS k) Q a ((a ^ 2 + k * a * b + b ^ 2) / c) b ∧
      IsGenCohnTriple k Q (Q * R - genCohnS k) R b ((b ^ 2 + k * b * c + c ^ 2) / a) c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 3.5.

Uses 2

Statement usesGeneralized Cohn triple · The matrix \(S\) of the generalized Cohn triple relation

TheoremA product identity for generalized Cohn matrices#●ready to prove

Let \(k\) be a natural number, let \(M\) be a \(k\)-generalized Cohn matrix, and let \(E\) be the \(2 \times 2\) integer matrix whose only nonzero entry is \(3 + 3k\), in row \(2\) and column \(1\). Then \(MEM = (\operatorname{tr} M + k)M + E\) and \(M^{-1} E M^{-1} = -(\operatorname{tr} M^{-1} + k)M^{-1} + E\).

public theorem_wanted IsGenCohnMatrix.mul_E_mul {k : ℕ} {M : Matrix (Fin 2) (Fin 2) ℤ}
    (hM : IsGenCohnMatrix k M) :
    M * !![0, 0; 3 + 3 * (k : ℤ), 0] * M =
        (M.trace + (k : ℤ)) • M + !![0, 0; 3 + 3 * (k : ℤ), 0] ∧
      M⁻¹ * !![0, 0; 3 + 3 * (k : ℤ), 0] * M⁻¹ =
        (-(M⁻¹.trace + (k : ℤ))) • M⁻¹ + !![0, 0; 3 + 3 * (k : ℤ), 0]

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 3.7.

Uses 1

Statement usesGeneralized Cohn matrices

TheoremVertices of the wide generalized Cohn tree are generalized Cohn triples#●ready to prove

Let \(k\) be a natural number. For every integer \(\ell\) and every path \(w\), the vertex of the wide \(k\)-generalized Cohn tree \(\mathrm{WGCT}(k, \ell)\) at \(w\) is a \(k\)-generalized Cohn triple associated with the vertex of the wide \(k\)-generalized Markov tree \(\mathrm{WMT}(k)\) at \(w\). Moreover, every \(k\)-generalized Markov triple \((a, b, c)\) with \(a \le b\) and \(c \le b\) has an associated \(k\)-generalized Cohn triple.

public theorem_wanted wideGenCohnTree_isGenCohnTriple (k : ℕ) (ℓ : ℤ) :
    (∀ w, IsGenCohnTriple k (wideGenCohnTree k ℓ w).1 (wideGenCohnTree k ℓ w).2.1
      (wideGenCohnTree k ℓ w).2.2 (wideGenMarkovTree k w).1 (wideGenMarkovTree k w).2.1
      (wideGenMarkovTree k w).2.2) ∧
    ∀ a b c, IsGenMarkovTriple k a b c → a ≤ b → c ≤ b → ∃ P Q R, IsGenCohnTriple k P Q R a b c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 3.9.

Uses 4

Statement usesGeneralized Cohn triple · Generalized Markov triple · The wide generalized Cohn tree · The wide generalized Markov tree

TheoremGeneralized Cohn triples with largest middle entry lie in wide generalized Cohn trees#●ready to prove

Let \(k\) be a natural number and let \((P, Q, R)\) be a \(k\)-generalized Cohn triple associated with \((a, b, c)\), where \(a \le b\) and \(c \le b\). Then there are an integer \(\ell\) and a path \(w\) such that \((P, Q, R)\) is the vertex of the wide \(k\)-generalized Cohn tree \(\mathrm{WGCT}(k, \ell)\) reached along \(w\).

public theorem_wanted IsGenCohnTriple.mem_wideGenCohnTree {k a b c : ℕ}
    {P Q R : Matrix (Fin 2) (Fin 2) ℤ} (h : IsGenCohnTriple k P Q R a b c) (hab : a ≤ b)
    (hcb : c ≤ b) : ∃ ℓ w, wideGenCohnTree k ℓ w = (P, Q, R)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 3.10.

Uses 2

Statement usesGeneralized Cohn triple · The wide generalized Cohn tree

TheoremParent triples of a generalized Cohn triple#●ready to prove

Let \(k\) be a natural number and let \(S\) be the integer matrix with rows \((k, 0)\) and \((3k^2 + 3k, k)\). Let \((P, Q, R)\) be a \(k\)-generalized Cohn triple associated with \((a, b, c)\), and let \(b' = \lfloor (a^2 + kac + c^2)/b \rfloor\). Then \((P, R, P^{-1}(R + S))\) is a \(k\)-generalized Cohn triple associated with \((a, c, b')\), and \(((P + S)R^{-1}, P, R)\) is a \(k\)-generalized Cohn triple associated with \((b', a, c)\).

public theorem_wanted IsGenCohnTriple.parent {k a b c : ℕ} {P Q R : Matrix (Fin 2) (Fin 2) ℤ}
    (h : IsGenCohnTriple k P Q R a b c) :
    IsGenCohnTriple k P R (P⁻¹ * (R + genCohnS k)) a c ((a ^ 2 + k * a * c + c ^ 2) / b) ∧
      IsGenCohnTriple k ((P + genCohnS k) * R⁻¹) P R ((a ^ 2 + k * a * c + c ^ 2) / b) a c

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 3.11.

Uses 2

Statement usesGeneralized Cohn triple · The matrix \(S\) of the generalized Cohn triple relation

TheoremDistinct paths give distinct middle matrices in the wide generalized Cohn tree#●ready to prove

For every natural number \(k\) and every integer \(\ell\), if the vertices \((P, Q, R)\) and \((P', Q', R')\) of the wide \(k\)-generalized Cohn tree \(\mathrm{WGCT}(k, \ell)\) at paths \(w\) and \(w'\) (finite sequences of left and right steps) satisfy \(Q = Q'\), then \(w = w'\).

public theorem_wanted wideGenCohnTree_snd_injective (k : ℕ) (ℓ : ℤ) :
    Function.Injective fun w => (wideGenCohnTree k ℓ w).2.1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Theorem 3.13.

Uses 1

Statement usesThe wide generalized Cohn tree

TheoremVertices of the generalized Cohn tree are Cohn triples over the Markov tree#●ready to prove

For every natural number \(k\), every integer \(\ell\) and every path \(w\) (a finite sequence of left and right steps), the vertex \((P, Q, R)\) of the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, \ell)\) at \(w\) is a \(k\)-generalized Cohn triple associated with the vertex \((a, b, c)\) of the \(k\)-generalized Markov tree \(\mathrm{MT}(k)\) at the same path \(w\).

The source phrases this as the canonical graph isomorphism \(\mathrm{GCT}(k, \ell) \to \mathrm{MT}(k)\).

public theorem_wanted genCohnTree_isGenCohnTriple (k : ℕ) (ℓ : ℤ) (w : List Bool) :
    IsGenCohnTriple k (genCohnTree k ℓ w).1 (genCohnTree k ℓ w).2.1 (genCohnTree k ℓ w).2.2
      (genMarkovTree k w).1 (genMarkovTree k w).2.1 (genMarkovTree k w).2.2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 3.15.

Uses 3

Statement usesGeneralized Cohn triple · The \(k\)-generalized Cohn tree · Generalized Markov tree

TheoremMiddle matrices of the generalized Cohn tree are distinct#●ready to prove

For every natural number \(k\) and every integer \(\ell\), vertices of the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, \ell)\) at different paths have different middle matrices.

public theorem_wanted genCohnTree_snd_injective (k : ℕ) (ℓ : ℤ) :
    Function.Injective fun w => (genCohnTree k ℓ w).2.1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 3.16.

Uses 1

Statement usesThe \(k\)-generalized Cohn tree

TheoremCohn triples sit at a unique vertex of a Cohn tree#●ready to prove

Let \((P, Q, R)\) be a \(k\)-generalized Cohn triple associated with \((a, b, c)\), where \(b > \max\{a, c\}\). Then there is exactly one pair \((\ell, w)\) of an integer \(\ell\) and a path \(w\) (a finite sequence of left and right moves) such that \((P, Q, R)\) is the vertex of the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, \ell)\) reached along \(w\).

public theorem_wanted IsGenCohnTriple.existsUnique_mem_genCohnTree {k a b c : ℕ}
    {P Q R : Matrix (Fin 2) (Fin 2) ℤ} (h : IsGenCohnTriple k P Q R a b c) (hab : a < b)
    (hcb : c < b) : ∃! p : ℤ × List Bool, genCohnTree k p.1 p.2 = (P, Q, R)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 3.17.

Uses 2

Statement usesGeneralized Cohn triple · The \(k\)-generalized Cohn tree

DefinitionThe Farey tree#✓fully proved

Write a fraction \(n/d\), with \(n\) and \(d\) natural numbers, for the pair \((n, d)\), so that \(1/0\) stands for \(\infty\). The Farey tree \(\mathrm{FT}\) is the infinite binary tree of triples of fractions with root \((0/1, 1/1, 1/0)\) in which a vertex \((a/b, c/d, e/f)\) has left child \((a/b, (a+c)/(b+d), c/d)\) and right child \((c/d, (c+e)/(d+f), e/f)\). For a path \(w\), a finite sequence of left and right moves, this gives the vertex of \(\mathrm{FT}\) reached from the root by making the moves of \(w\) in order.

public def fareyTree (w : List Bool) : (ℕ × ℕ) × (ℕ × ℕ) × (ℕ × ℕ) :=
  w.foldl (fun T d => match d, T with
    | false, (x, y, _) => (x, (x.1 + y.1, x.2 + y.2), y)
    | true, (_, y, z) => (y, (y.1 + z.1, y.2 + z.2), z)) ((0, 1), (1, 1), (1, 0))

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.2.

Used by 11

Used byLeft child of the root of the Farey tree · Basic properties of the Farey tree · Positive corner entry of the generalized Cohn tree for \(\ell = -k\) · Shape of the generalized Cohn matrices for \(\ell = -k\) · The characteristic number is less than \(m_t/2 - k\) · The characteristic number solves \(m_r x \equiv m_s \pmod{m_t}\) · The characteristic number solves \(x^2 + kx + 1 \equiv 0 \pmod{m_t}\) · Fraction labels of generalized Cohn matrices · The middle matrix of the root of \(\mathrm{GCT}(k, \ell)\) has label \(1/1\) · Fraction labeling of generalized Markov numbers · The fraction \(1/1\) labels \(k + 2\)

TheoremLeft child of the root of the Farey tree#✓fully proved

The left child of the root \((0/1, 1/1, 1/0)\) of the Farey tree is \((0/1, 1/2, 1/1)\).

public theorem fareyTree_false : fareyTree [false] = ((0, 1), (1, 2), (1, 1))

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 4.

Uses 1

Statement usesThe Farey tree

DefinitionFarey triples#✓fully proved

Write a pair \((a, b)\) of natural numbers as the fraction \(a/b\), so that \(1/0\) is allowed. Three such fractions \((a/b, c/d, e/f)\) form a Farey triple if \(\gcd(a, b) = \gcd(c, d) = \gcd(e, f) = 1\) and

\[|ad - bc| = |cf - de| = |eb - fa| = 1,\]

where the differences are taken in \(\mathbb{Z}\).

The paper's printed condition writes \(d/e\) for \(e/f\).

public def IsFareyTriple (x y z : ℕ × ℕ) : Prop :=
  Nat.Coprime x.1 x.2 ∧ Nat.Coprime y.1 y.2 ∧ Nat.Coprime z.1 z.2 ∧
    |(x.1 : ℤ) * y.2 - x.2 * y.1| = 1 ∧ |(y.1 : ℤ) * z.2 - y.2 * z.1| = 1 ∧
    |(z.1 : ℤ) * x.2 - z.2 * x.1| = 1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.2.

Used by 2

Used byBasic properties of the Farey tree · The triple \((0/1, 1/1, 1/0)\) is a Farey triple

TheoremThe triple \((0/1, 1/1, 1/0)\) is a Farey triple#✓fully proved

The fractions \(0/1\), \(1/1\) and \(1/0\), given as the pairs of natural numbers \((0, 1)\), \((1, 1)\) and \((1, 0)\), form a Farey triple.

This triple is the root of the Farey tree.

public theorem isFareyTriple_root : IsFareyTriple (0, 1) (1, 1) (1, 0)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.2.

Uses 1

Statement usesFarey triples

TheoremBasic properties of the Farey tree#●ready to prove

Write a fraction \(a/b\), with \(a\) and \(b\) natural numbers, for the pair \((a, b)\), so that \(1/0\) stands for \(\infty\), and compare fractions by cross multiplication: \(a/b < c/d\) means \(ad < cb\). (1) If \((a/b, c/d, e/f)\) is a Farey triple, then so are \((a/b, (a+c)/(b+d), c/d)\) and \((c/d, (c+e)/(d+f), e/f)\); and the vertex of the Farey tree reached along every path is a Farey triple. (2) For all coprime positive natural numbers \(a\) and \(b\) there is exactly one path along which the vertex of the Farey tree has second entry \(a/b\). (3) Every vertex \((a/b, c/d, e/f)\) of the Farey tree satisfies \(a/b < c/d < e/f\).

public theorem_wanted fareyTree_properties :
    (∀ x y z, IsFareyTriple x y z →
      IsFareyTriple x (x.1 + y.1, x.2 + y.2) y ∧ IsFareyTriple y (y.1 + z.1, y.2 + z.2) z) ∧
    (∀ w, IsFareyTriple (fareyTree w).1 (fareyTree w).2.1 (fareyTree w).2.2) ∧
    (∀ a b : ℕ, 0 < a → 0 < b → Nat.Coprime a b → ∃! w, (fareyTree w).2.1 = (a, b)) ∧
    ∀ w, (fareyTree w).1.1 * (fareyTree w).2.1.2 < (fareyTree w).2.1.1 * (fareyTree w).1.2 ∧
      (fareyTree w).2.1.1 * (fareyTree w).2.2.2 < (fareyTree w).2.2.1 * (fareyTree w).2.1.2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 3.22 (citing Aigner, Section 3.2).

Uses 2

Statement usesFarey triples · The Farey tree

DefinitionFraction labels of generalized Cohn matrices#✓fully proved

Let \(k\) be a natural number and \(\ell\) an integer, and write a pair \((a, b)\) of natural numbers as the fraction \(a/b\). An integer \(2 \times 2\) matrix \(C\) is labeled by the fraction \(q\), written \(C = C_q(k, \ell)\), if there is a path \(w\) from the root such that, for one of the three positions (first, second or third), \(C\) is the entry in that position of the vertex of the generalized Cohn tree \(\mathrm{GCT}(k, \ell)\) at \(w\) and \(q\) is the entry in that position of the vertex of the Farey tree at \(w\).

The paper labels only second entries; here first and third entries carry the labels of the vertex where they were created, which gives \(C_{0/1}\) and \(C_{1/0}\).

public def IsGenCohnLabel (k : ℕ) (ℓ : ℤ) (q : ℕ × ℕ) (C : Matrix (Fin 2) (Fin 2) ℤ) : Prop :=
  ∃ w, ((fareyTree w).1 = q ∧ (genCohnTree k ℓ w).1 = C) ∨
    ((fareyTree w).2.1 = q ∧ (genCohnTree k ℓ w).2.1 = C) ∨
    ((fareyTree w).2.2 = q ∧ (genCohnTree k ℓ w).2.2 = C)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.2.

Uses 2 · Used by 2

Statement usesThe Farey tree · The \(k\)-generalized Cohn tree

Used byThe Cohn labeling is injective and increasing · The middle matrix of the root of \(\mathrm{GCT}(k, \ell)\) has label \(1/1\)

TheoremThe middle matrix of the root of \(\mathrm{GCT}(k, \ell)\) has label \(1/1\)#✓fully proved

For every natural number \(k\) and every integer \(\ell\), the second entry of the root vertex of the generalized Cohn tree \(\mathrm{GCT}(k, \ell)\) is labeled by the fraction \(1/1\), that is, it is \(C_{1/1}(k, \ell)\).

public theorem isGenCohnLabel_one (k : ℕ) (ℓ : ℤ) :
    IsGenCohnLabel k ℓ (1, 1) (genCohnTree k ℓ []).2.1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 3.2.

Uses 3

Statement usesFraction labels of generalized Cohn matrices · The \(k\)-generalized Cohn tree

Proof usesThe Farey tree

TheoremThe Cohn labeling is injective and increasing#●ready to prove

Fix a natural number \(k\) and an integer \(\ell\). Write fractions \(a/b\), with \(a\) and \(b\) natural numbers, as pairs \((a, b)\), compared by cross multiplication (\(a/b < c/d\) means \(ad < cb\)), and write \(C = C_q(k, \ell)\) when the matrix \(C\) carries the fraction label \(q\) in the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, \ell)\). For an integer \(2 \times 2\) matrix \(M = (m_{ij})\) let \(I_M = m_{11}/m_{12} \in \mathbb{Q}\). (1) If \(C = C_q(k, \ell)\) and \(C = C_{q'}(k, \ell)\), then \(q = q'\). (2) If \(C = C_q(k, \ell)\), \(C' = C_{q'}(k, \ell)\) and \(q < q'\), then \(I_C < I_{C'}\).

public theorem_wanted genCohnLabel_injective_index_strictMono (k : ℕ) (ℓ : ℤ) :
    (∀ q q' C, IsGenCohnLabel k ℓ q C → IsGenCohnLabel k ℓ q' C → q = q') ∧
    ∀ q q' C C', IsGenCohnLabel k ℓ q C → IsGenCohnLabel k ℓ q' C' → q.1 * q'.2 < q'.1 * q.2 →
      (C 0 0 : ℚ) / C 0 1 < (C' 0 0 : ℚ) / C' 0 1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 3.23.

Uses 1

Statement usesFraction labels of generalized Cohn matrices

DefinitionFraction labeling of generalized Markov numbers#✓fully proved

Let \(k\) be a natural number. Write a fraction \(n/d\) as the pair \((n, d)\) of natural numbers, with \(1/0\) standing for \(\infty\). Let \(FT\) be the Farey tree and \(MT(k)\) the \(k\)-generalized Markov tree, with vertices of both indexed by finite paths of left and right steps from the root. A natural number \(m\) carries the label \(q\), written \(m = m_q\), when there are a path \(w\) and a position \(i \in \{1, 2, 3\}\) such that the \(i\)-th entry of the vertex of \(FT\) at \(w\) is \(q\) and the \(i\)-th entry of the vertex of \(MT(k)\) at \(w\) is \(m\).

On fractions in \([0, 1]\) this gives \(m_{0/1} = 1\), \(m_{1/1} = k + 2\) and, for \(t \in (0, 1)\), the number \(m_t\) of Gyoda and Maruyama.

public def IsGenMarkovLabel (k : ℕ) (q : ℕ × ℕ) (m : ℕ) : Prop :=
  ∃ w, ((fareyTree w).1 = q ∧ (genMarkovTree k w).1 = m) ∨
    ((fareyTree w).2.1 = q ∧ (genMarkovTree k w).2.1 = m) ∨
    ((fareyTree w).2.2 = q ∧ (genMarkovTree k w).2.2 = m)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 4.

Uses 2 · Used by 3

Statement usesThe Farey tree · Generalized Markov tree

Used byUniqueness of maximal triples and injectivity of the fraction labeling · Unique maximal triple via the fraction labeling · The fraction \(1/1\) labels \(k + 2\)

TheoremThe fraction \(1/1\) labels \(k + 2\)#✓fully proved

For every natural number \(k\), the number \(k + 2\) carries the label \(1/1\) in the fraction labeling of \(k\)-generalized Markov numbers, that is, \(m_{1/1} = k + 2\).

public theorem isGenMarkovLabel_one (k : ℕ) : IsGenMarkovLabel k (1, 1) (k + 2)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Section 4.

Uses 4

Statement usesFraction labeling of generalized Markov numbers

Proof usesThe Farey tree · Generalized Markov tree · Root of the generalized Markov tree

TheoremUnique maximal triple via the fraction labeling#●ready to prove

Let \(k\) be a natural number and \(b\) a \(k\)-generalized Markov number. Then \(b\) is the maximum of a unique \(k\)-generalized Markov triple up to order if and only if there is exactly one pair \((n, d)\) of natural numbers with \(n \le d\) such that \(b\) is a label of the fraction \(n/d\) in the fraction labeling of \(k\)-generalized Markov numbers.

public theorem_wanted hasUniqueMaxGenMarkovTriple_iff_existsUnique_label {k b : ℕ}
    (hb : IsGenMarkovNumber k b) :
    HasUniqueMaxGenMarkovTriple k b ↔ ∃! q : ℕ × ℕ, q.1 ≤ q.2 ∧ IsGenMarkovLabel k q b

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Proposition 4.1.

Uses 3

Statement usesUnique maximal generalized Markov triple · Fraction labeling of generalized Markov numbers · Generalized Markov number

TheoremUniqueness of maximal triples and injectivity of the fraction labeling#●ready to prove

For every natural number \(k\), the following are equivalent: every \(k\)-generalized Markov number is the maximum of a unique \(k\)-generalized Markov triple up to order (Conjecture 1.8 for \(k\)); and the fraction labeling of \(k\)-generalized Markov numbers is injective on \([0, 1]\), that is, whenever \((n, d)\) and \((n', d')\) are pairs of natural numbers with \(n \le d\) and \(n' \le d'\) and a number \(m\) is a label of both \(n/d\) and \(n'/d'\), then \((n, d) = (n', d')\).

public theorem_wanted genMarkovUniqueness_iff_label_injective (k : ℕ) :
    (∀ b, IsGenMarkovNumber k b → HasUniqueMaxGenMarkovTriple k b) ↔
      ∀ q q' m, q.1 ≤ q.2 → q'.1 ≤ q'.2 → IsGenMarkovLabel k q m → IsGenMarkovLabel k q' m →
        q = q'

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 4.2.

Uses 3

Statement usesUnique maximal generalized Markov triple · Fraction labeling of generalized Markov numbers · Generalized Markov number

DefinitionCharacteristic number#✓fully proved

For natural numbers \(m_r\), \(m_t\), \(m_s\), a natural number \(x\) is a characteristic number of \((m_r, m_t, m_s)\) when \(0 < x < m_t/2\) and \(m_r x \equiv \pm m_s \pmod{m_t}\), that is, \(m_t\) divides \(m_r x - m_s\) or \(m_r x + m_s\) in \(\mathbb{Z}\).

public def IsGenMarkovCharNumber (mr mt ms x : ℕ) : Prop :=
  0 < x ∧ 2 * x < mt ∧ ((mt : ℤ) ∣ mr * x - ms ∨ (mt : ℤ) ∣ mr * x + ms)

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Definition 4.3.

Used by 5

Used byShape of the generalized Cohn matrices for \(\ell = -k\) · The characteristic number is less than \(m_t/2 - k\) · The characteristic number solves \(m_r x \equiv m_s \pmod{m_t}\) · The characteristic number solves \(x^2 + kx + 1 \equiv 0 \pmod{m_t}\) · Characteristic number of \((1, 5, 2)\)

TheoremCharacteristic number of \((1, 5, 2)\)#✓fully proved

The number \(2\) is a characteristic number of \((m_r, m_t, m_s) = (1, 5, 2)\): indeed \(0 < 2 < 5/2\) and \(1 \cdot 2 \equiv 2 \pmod 5\).

public theorem isGenMarkovCharNumber_one_five_two : IsGenMarkovCharNumber 1 5 2 2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Definition 4.3.

Uses 1

Statement usesCharacteristic number

TheoremPositive corner entry of the generalized Cohn tree for \(\ell = -k\)#●ready to prove

Let \(k\) be a natural number and \(w\) a path, and suppose that the middle fraction \(n/d\) of the vertex of the Farey tree at \(w\) satisfies \(0 < n < d\). Then the \((1,1)\)-entry of the middle matrix of the vertex of the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, -k)\) at \(w\) is positive.

public theorem_wanted genCohnTree_neg_snd_entry_pos (k : ℕ) (w : List Bool)
    (ht : 0 < (fareyTree w).2.1.1) (ht1 : (fareyTree w).2.1.1 < (fareyTree w).2.1.2) :
    0 < (genCohnTree k (-k) w).2.1 0 0

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.4.

Uses 2

Statement usesThe Farey tree · The \(k\)-generalized Cohn tree

TheoremShape of the generalized Cohn matrices for \(\ell = -k\)#●ready to prove

Let \(k\) be a natural number and \(w\) a path, and suppose that the middle fraction \(n/d\) of the vertex of the Farey tree at \(w\) satisfies \(0 < n < d\). Let \((a, b, c)\) be the vertex of the \(k\)-generalized Markov tree \(\mathrm{MT}(k)\) at \(w\), and let \(C\) be the middle matrix of the vertex of the \(k\)-generalized Cohn tree \(\mathrm{GCT}(k, -k)\) at \(w\). Then there is a natural number \(u\) that is a characteristic number of \((a, b, c)\) such that \(C_{11} = u\), \(C_{12} = b\) and \(C_{22} = (3 + 3k)b - u - k\).

public theorem_wanted genCohnTree_neg_snd_eq (k : ℕ) (w : List Bool)
    (ht : 0 < (fareyTree w).2.1.1) (ht1 : (fareyTree w).2.1.1 < (fareyTree w).2.1.2) :
    ∃ u, IsGenMarkovCharNumber (genMarkovTree k w).1 (genMarkovTree k w).2.1
        (genMarkovTree k w).2.2 u ∧
      (genCohnTree k (-k) w).2.1 0 0 = u ∧
      (genCohnTree k (-k) w).2.1 0 1 = (genMarkovTree k w).2.1 ∧
      (genCohnTree k (-k) w).2.1 1 1 = (3 + 3 * k) * ((genMarkovTree k w).2.1 : ℤ) - u - k

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.5.

Uses 4

Statement usesCharacteristic number · The Farey tree · The \(k\)-generalized Cohn tree · Generalized Markov tree

TheoremThe characteristic number solves \(m_r x \equiv m_s \pmod{m_t}\)#●ready to prove

Let \(k \in \mathbb{N}\), let \(w\) be a finite sequence of left and right moves, let \((r, t, s)\) be the vertex of the Farey tree at \(w\), and let \((m_r, m_t, m_s)\) be the vertex of the \(k\)-generalized Markov tree \(\mathrm{MT}(k)\) at \(w\). Write \(t = n/d\). If \(0 < n < d\) and \(u\) is a characteristic number of \((m_r, m_t, m_s)\), then \(m_t\) divides \(m_r u - m_s\) in \(\mathbb{Z}\), that is, \(m_r u \equiv m_s \pmod{m_t}\).

Of the two congruences \(m_r x \equiv \pm m_s \pmod{m_t}\) allowed in the definition of a characteristic number, the one with the plus sign holds.

public theorem_wanted genMarkovCharNumber_dvd_sub (k : ℕ) (w : List Bool)
    (ht : 0 < (fareyTree w).2.1.1) (ht1 : (fareyTree w).2.1.1 < (fareyTree w).2.1.2) (u : ℕ)
    (hu : IsGenMarkovCharNumber (genMarkovTree k w).1 (genMarkovTree k w).2.1
      (genMarkovTree k w).2.2 u) :
    ((genMarkovTree k w).2.1 : ℤ) ∣ (genMarkovTree k w).1 * u - (genMarkovTree k w).2.2

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Corollary 4.6.

Uses 3

Statement usesCharacteristic number · The Farey tree · Generalized Markov tree

TheoremThe characteristic number solves \(x^2 + kx + 1 \equiv 0 \pmod{m_t}\)#●ready to prove

Let \(k \in \mathbb{N}\), let \(w\) be a finite sequence of left and right moves, let \((r, t, s)\) be the vertex of the Farey tree at \(w\), and let \((m_r, m_t, m_s)\) be the vertex of the \(k\)-generalized Markov tree \(\mathrm{MT}(k)\) at \(w\). Write \(t = n/d\). If \(0 < n < d\) and \(u\) is a characteristic number of \((m_r, m_t, m_s)\), then \(m_t\) divides \(u^2 + ku + 1\), that is, \(u^2 + ku + 1 \equiv 0 \pmod{m_t}\).

public theorem_wanted genMarkovCharNumber_sq_add (k : ℕ) (w : List Bool)
    (ht : 0 < (fareyTree w).2.1.1) (ht1 : (fareyTree w).2.1.1 < (fareyTree w).2.1.2) (u : ℕ)
    (hu : IsGenMarkovCharNumber (genMarkovTree k w).1 (genMarkovTree k w).2.1
      (genMarkovTree k w).2.2 u) :
    (genMarkovTree k w).2.1 ∣ u ^ 2 + k * u + 1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.7.

Uses 3

Statement usesCharacteristic number · The Farey tree · Generalized Markov tree

TheoremThe characteristic number is less than \(m_t/2 - k\)#●ready to prove

Let \(k \in \mathbb{N}\), let \(w\) be a finite sequence of left and right moves, let \((r, t, s)\) be the vertex of the Farey tree at \(w\), and let \((m_r, m_t, m_s)\) be the vertex of the \(k\)-generalized Markov tree \(\mathrm{MT}(k)\) at \(w\). Write \(t = n/d\). If \(0 < n < d\) and \(u\) is a characteristic number of \((m_r, m_t, m_s)\), then \(2(u + k) < m_t\), that is, \(u + k < m_t/2\).

public theorem_wanted genMarkovCharNumber_add_lt (k : ℕ) (w : List Bool)
    (ht : 0 < (fareyTree w).2.1.1) (ht1 : (fareyTree w).2.1.1 < (fareyTree w).2.1.2) (u : ℕ)
    (hu : IsGenMarkovCharNumber (genMarkovTree k w).1 (genMarkovTree k w).2.1
      (genMarkovTree k w).2.2 u) :
    2 * (u + k) < (genMarkovTree k w).2.1

Sources

• Y. Gyoda and S. Maruyama, Uniqueness Theorem of Generalized Markov Numbers That Are Prime Powers, INTEGERS 26 (2026), Article A91, Lemma 4.8.

Uses 3

Statement usesCharacteristic number · The Farey tree · Generalized Markov tree

40 fully proved45 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.