Permutiples

DefinitionPermutiples with a given digit permutation#✓fully proved

Let \(n\), \(b\) and \(d_0, \dots, d_k\) be natural numbers and let \(\sigma\) be a permutation of \(\{0, \dots, k\}\). The numeral \((d_k, \dots, d_0)_b\) is an \((n, b, \sigma)\)-permutiple when \(d_j < b\) for every \(j\) and

\[\sum_{j=0}^k d_j b^j = n \sum_{j=0}^k d_{\sigma(j)} b^j,\]

that is, \((d_k, \dots, d_0)_b = n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\).

public def IsPermutiple (n b : ℕ) {k : ℕ} (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) :
    Prop :=
  (∀ j, d j < b) ∧ ∑ j, d j * b ^ (j : ℕ) = n * ∑ j, d (σ j) * b ^ (j : ℕ)

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Definition 1 (from Holt, Some general results and open questions on palintiple numbers).

Used by 10

Used byEvery permutiple has a cycle-preserving digit permutation · \(87912\) is a \((4, 10)\)-permutiple by digit reversal · Permutiple strings · The permutiple string of \(87912 = 4 \cdot 21978\) · Holt's residue condition for rearranged permutiples · Carry bound for permutiples · Carry relation for permutiples · Edge condition for permutiples · Permutiple graphs are unions of simple cycles of the mother graph · Edges of a permutiple's graph lie on cycles of the mother graph

DefinitionCarries of a permutiple multiplication#✓fully proved

Let \(n\), \(b\) and \(d_0, \dots, d_k\) be natural numbers and let \(\sigma\) be a permutation of \(\{0, \dots, k\}\). The carries of the single-digit multiplication \(n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\), where \((e_k, \dots, e_0)_b\) denotes the base-\(b\) numeral \(\sum_{j=0}^{k} e_j b^j\), are the natural numbers \(c_0, c_1, c_2, \dots\) defined by \(c_0 = 0\), \(c_{j+1} = \lfloor (n d_{\sigma(j)} + c_j) / b \rfloor\) for \(0 \le j \le k\), and \(c_{j+1} = 0\) for \(j > k\). Division by \(b = 0\) is taken to give \(0\).

public def permutipleCarry (n b : ℕ) {k : ℕ} (d : Fin (k + 1) → ℕ)
    (σ : Equiv.Perm (Fin (k + 1))) : ℕ → ℕ
  | 0 => 0
  | j + 1 => if h : j < k + 1 then (n * d (σ ⟨j, h⟩) + permutipleCarry n b d σ j) / b else 0

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Section 2.

Used by 3

Used byCarry bound for permutiples · Carry relation for permutiples · First two carries of a permutiple multiplication

TheoremFirst two carries of a permutiple multiplication#✓fully proved

Let \(n\), \(b\) and \(d_0, \dots, d_k\) be natural numbers, let \(\sigma\) be a permutation of \(\{0, \dots, k\}\), and write \((e_k, \dots, e_0)_b\) for the base-\(b\) numeral \(\sum_{j=0}^{k} e_j b^j\). The carries \(c_0, c_1, \dots\) of the single-digit multiplication \(n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\), defined by \(c_0 = 0\) and \(c_{j+1} = \lfloor (n d_{\sigma(j)} + c_j) / b \rfloor\) for \(0 \le j \le k\), satisfy \(c_0 = 0\) and \(c_1 = \lfloor n d_{\sigma(0)} / b \rfloor\), where division by \(b = 0\) is taken to give \(0\).

public theorem permutipleCarry_zero_one (n b : ℕ) {k : ℕ} (d : Fin (k + 1) → ℕ)
    (σ : Equiv.Perm (Fin (k + 1))) :
    permutipleCarry n b d σ 0 = 0 ∧ permutipleCarry n b d σ 1 = n * d (σ 0) / b

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Section 2.

Uses 1

Statement usesCarries of a permutiple multiplication

Theorem\(87912\) is a \((4, 10)\)-permutiple by digit reversal#✓fully proved

The numeral \((d_4, d_3, d_2, d_1, d_0)_{10} = 87912\) is a \((4, 10, \sigma)\)-permutiple, where \(\sigma\) is the reversal \(j \mapsto 4 - j\) of \(\{0, \dots, 4\}\); that is, \(87912 = 4 \cdot 21978\), and \(21978\) has the digits of \(87912\) in reverse order.

public theorem isPermutiple_87912 :
    IsPermutiple 4 10 (k := 4) ![2, 1, 9, 7, 8] Fin.revPerm

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Introduction.

Uses 1 · Used by 1

Statement usesPermutiples with a given digit permutation

Used byThe permutiple string of \(87912 = 4 \cdot 21978\)

TheoremCarry relation for permutiples#●ready to prove

Let \(n\) and \(b \ge 2\) be natural numbers, let \(\sigma\) be a permutation of \(\{0, \dots, k\}\), and let \((d_k, \dots, d_0)_b\) be an \((n, b, \sigma)\)-permutiple, where \((e_k, \dots, e_0)_b\) denotes the base-\(b\) numeral \(\sum_{j=0}^{k} e_j b^j\). Let \(c_0, c_1, \dots\) be the carries of the multiplication \(n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\). Then for every \(0 \le j \le k\),

\[b\, c_{j+1} - c_j = n\, d_{\sigma(j)} - d_j,\]

with both sides computed in the integers.

public theorem_wanted permutipleCarry_relation (n b : ℕ) (hb : 2 ≤ b) {k : ℕ}
    (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ)
    (j : Fin (k + 1)) :
    (b : ℤ) * permutipleCarry n b d σ (j + 1) - permutipleCarry n b d σ j =
      (n : ℤ) * d (σ j) - d j

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Theorem 1, quoting Holt's earlier paper; restated as Theorem 1 of Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13.

Uses 2

Statement usesPermutiples with a given digit permutation · Carries of a permutiple multiplication

TheoremCarry bound for permutiples#●ready to prove

Let \(n\) and \(b \ge 2\) be natural numbers, let \(\sigma\) be a permutation of \(\{0, \dots, k\}\), and let \((d_k, \dots, d_0)_b\) be an \((n, b, \sigma)\)-permutiple, where \((e_k, \dots, e_0)_b\) denotes the base-\(b\) numeral \(\sum_{j=0}^{k} e_j b^j\). Let \(c_0, c_1, \dots\) be the carries of the multiplication \(n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\). Then for every \(0 \le j \le k\) we have \(c_j \le n - 1\) if \(n \ge 1\), and \(c_j = 0\) if \(n = 0\).

public theorem_wanted permutipleCarry_le (n b : ℕ) (hb : 2 ≤ b) {k : ℕ} (d : Fin (k + 1) → ℕ)
    (σ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ) (j : Fin (k + 1)) :
    permutipleCarry n b d σ j ≤ n - 1

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Theorem 2, quoting Holt's earlier paper; restated as Theorem 2 of Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13.

Uses 2

Statement usesPermutiples with a given digit permutation · Carries of a permutiple multiplication

TheoremHolt's residue condition for rearranged permutiples#●ready to prove

Let \(n \ge 1\) and \(b \ge 2\) be natural numbers, let \(d_0, \dots, d_k\) be natural numbers, and write \((e_k, \dots, e_0)_b\) for the base-\(b\) numeral \(\sum_{j=0}^{k} e_j b^j\). Let \(\sigma\), \(\pi\) and \(\tau\) be permutations of \(\{0, \dots, k\}\). If \((d_k, \dots, d_0)_b\) is an \((n, b, \sigma)\)-permutiple and \((d_{\pi(k)}, \dots, d_{\pi(0)})_b\) is an \((n, b, \tau)\)-permutiple, then for every \(0 \le j \le k\)

\[\lambda\bigl(d_j + (b - n)\, d_{\pi(\tau(\pi^{-1}(j)))}\bigr) \le n - 1,\]

where \(\lambda(x)\) is the least non-negative residue of the integer \(x\) modulo \(b\) (the difference \(b - n\) is taken in the integers and may be negative).

The hypothesis \(n \ge 1\) is needed: for \(n = 0\) the only permutiples have all digits zero and the bound would read \(0 \le -1\).

public theorem_wanted permutiple_basePerm_residue_le (n b : ℕ) (hn : 1 ≤ n) (hb : 2 ≤ b)
    {k : ℕ} (d : Fin (k + 1) → ℕ) (σ π τ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ)
    (hq : IsPermutiple n b (d ∘ π) τ) (j : Fin (k + 1)) :
    ((d j : ℤ) + ((b : ℤ) - n) * d ((π * τ * π⁻¹) j)) % b ≤ n - 1

Sources

• B. V. Holt, A Method for Finding All Permutiples with a Fixed Set of Digits from a Single Known Example, INTEGERS 24 (2024), Article A88, Theorem 3.

Uses 1

Statement usesPermutiples with a given digit permutation

DefinitionEdge set of the graph of a numeral#✓fully proved

Let \(b\) be a base, let \(d_0, \dots, d_k\) be natural numbers, the digits of the base-\(b\) numeral \((d_k, \dots, d_0)_b = \sum_{j=0}^{k} d_j b^j\), and let \(\sigma\) be a permutation of \(\{0, \dots, k\}\). The graph \(G\) of these digits with digit permutation \(\sigma\) has edge set

\[E = \{(d_j, d_{\sigma(j)}) : 0 \le j \le k\},\]

a finite set of ordered pairs of natural numbers; it does not depend on \(b\).

The vertices of \(G\) are all base-\(b\) digits, so \(G\) is determined by its edge set.

public def permutipleGraphEdges {k : ℕ} (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) :
    Finset (ℕ × ℕ) :=
  Finset.univ.image fun j => (d j, d (σ j))

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Definition 3 (the graph of a permutiple).

Used by 3

Used byGraph of the permutiple 87912 · Conjugate rearrangements have the same graph · Permutiple graphs are unions of simple cycles of the mother graph

TheoremGraph of the permutiple 87912#✓fully proved

Let \((d_0, d_1, d_2, d_3, d_4) = (2, 1, 9, 7, 8)\) be the decimal digits of \(87912\), from the units digit up, and let \(\sigma\) be the reversal \(\sigma(j) = 4 - j\) of \(\{0, \dots, 4\}\). The edge set \(\{(d_j, d_{\sigma(j)}) : 0 \le j \le 4\}\) of the graph of these digits with digit permutation \(\sigma\) is exactly \(\{(2, 8), (1, 7), (9, 9), (7, 1), (8, 2)\}\): the edges \(8 \rightleftarrows 2\) and \(7 \rightleftarrows 1\) and a loop at \(9\).

Here \(87912 = 4 \cdot 21978\), and \(21978\) is \(87912\) with its digits reversed.

public theorem permutipleGraphEdges_87912 :
    permutipleGraphEdges (k := 4) ![2, 1, 9, 7, 8] Fin.revPerm =
      {(2, 8), (1, 7), (9, 9), (7, 1), (8, 2)}

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Figure 1.

Uses 1

Statement usesEdge set of the graph of a numeral

DefinitionEdges of the mother graph#✓fully proved

Let \(n\) and \(b\) be natural numbers. For natural numbers \(x\) and \(y\), the pair \((x, y)\) is an edge of the \((n, b)\)-mother graph \(M\) when \(x < b\), \(y < b\) and

\[\lambda(x + (b - n) y) \le n - 1,\]

where \(\lambda(z)\) is the least non-negative residue of the integer \(z\) modulo \(b\), and \(b - n\) and \(n - 1\) are computed in the integers.

public def IsMotherGraphEdge (n b x y : ℕ) : Prop :=
  x < b ∧ y < b ∧ ((x : ℤ) + ((b : ℤ) - n) * y) % b ≤ (n : ℤ) - 1

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Definition 4 (the mother graph).

Used by 12

Used byEvery mother-graph edge induces a carry transition · Transitions of the Hoey-Sloane machine · Hoey-Sloane transitions are transitions of the machine · Hoey–Sloane words · The string \((0,0)(2,3)(1,2)(3,1)\) lies in the \((2, 4)\)-Hoey–Sloane language · Cycles of the mother graph · Sample edges of the \((4, 10)\)-mother graph · An edge and a non-edge of the \((2, 4)\)-mother graph · Inputs of a permutiple string lie on mother-graph cycles · A word in the \((4, 10)\)-Hoey-Sloane language · Permutiple graphs are unions of simple cycles of the mother graph · Edges of a permutiple's graph lie on cycles of the mother graph

TheoremAn edge and a non-edge of the \((2, 4)\)-mother graph#✓fully proved

In the \((2, 4)\)-mother graph, the pair \((0, 2)\) is an edge, since \(\lambda(0 + (4 - 2) \cdot 2) = \lambda(4) = 0 \le 1\), and the pair \((0, 1)\) is not an edge, since \(\lambda(0 + (4 - 2) \cdot 1) = \lambda(2) = 2 > 1\), where \(\lambda\) is the least non-negative residue modulo \(4\).

public theorem isMotherGraphEdge_two_four :
    IsMotherGraphEdge 2 4 0 2 ∧ ¬ IsMotherGraphEdge 2 4 0 1

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Definition 4 and Example 1.

Uses 1

Statement usesEdges of the mother graph

DefinitionCarries of the Hoey–Sloane machine#✓fully proved

Let \(n\) and \(b\) be natural numbers and let \((d_0, \hat d_0)(d_1, \hat d_1) \cdots (d_k, \hat d_k)\) be an input string of pairs of natural numbers. The carries \(c_0, c_1, c_2, \dots\) of the \((n, b)\)-Hoey–Sloane machine on this string are the integers given by \(c_0 = 0\),

\[c_{j+1} = \left\lfloor \frac{n \hat d_j - d_j + c_j}{b} \right\rfloor \quad (0 \le j \le k)\]

and \(c_{j+1} = 0\) for \(j > k\), where division by \(b = 0\) gives \(0\).

The machine has a transition from the state \(c_j\) on the input \((d_j, \hat d_j)\) when this division is exact.

public def hoeySloaneCarry (n b : ℕ) {k : ℕ} (d dh : Fin (k + 1) → ℕ) : ℕ → ℤ
  | 0 => 0
  | j + 1 =>
    if h : j < k + 1 then
      ((n : ℤ) * dh ⟨j, h⟩ - d ⟨j, h⟩ + hoeySloaneCarry n b d dh j) / b
    else 0

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Section 4, Equation (2) (the Hoey-Sloane machine).

Used by 3

Used byCarries of the \((2, 4)\)-Hoey–Sloane machine on \((0,0)(2,3)(1,2)(3,1)\) · Hoey–Sloane words · The string \((0,0)(2,3)(1,2)(3,1)\) lies in the \((2, 4)\)-Hoey–Sloane language

TheoremCarries of the \((2, 4)\)-Hoey–Sloane machine on \((0,0)(2,3)(1,2)(3,1)\)#✓fully proved

On the input string \((d_0, \hat d_0)(d_1, \hat d_1)(d_2, \hat d_2)(d_3, \hat d_3) = (0,0)(2,3)(1,2)(3,1)\), the carries \(c_0, c_1, c_2, c_3, c_4\) of the \((2, 4)\)-Hoey–Sloane machine are \(0, 0, 1, 1, 0\).

This is the \((2, 4)\)-permutiple string of \((3, 1, 2, 0)_4 = 216 = 2 \cdot 108 = 2 \cdot (1, 2, 3, 0)_4\).

public theorem hoeySloaneCarry_two_four_example :
    (List.range 5).map (hoeySloaneCarry 2 4 (k := 3) ![0, 2, 1, 3] ![0, 3, 2, 1]) =
      [0, 0, 1, 1, 0]

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Example 1.

Uses 1

Statement usesCarries of the Hoey–Sloane machine

DefinitionHoey–Sloane words#✓fully proved

Let \(n\) and \(b\) be natural numbers. An input string \((d_0, \hat d_0) \cdots (d_k, \hat d_k)\) of pairs of natural numbers belongs to the language \(L\) of the \((n, b)\)-Hoey–Sloane machine when, with \(c_0, \dots, c_{k+1}\) the carries of the machine on this string, every input \((d_j, \hat d_j)\) is an edge of the \((n, b)\)-mother graph, \(b\) divides \(n \hat d_j - d_j + c_j\) for every \(0 \le j \le k\), and \(c_{k+1} = 0\).

So the walk starts in the state \(c_0 = 0\), every transition is an exact division, and the walk ends in the state \(0\).

public def IsHoeySloaneWord (n b : ℕ) {k : ℕ} (d dh : Fin (k + 1) → ℕ) : Prop :=
  (∀ j, IsMotherGraphEdge n b (d j) (dh j)) ∧
    (∀ j : Fin (k + 1), (b : ℤ) ∣ (n : ℤ) * dh j - d j + hoeySloaneCarry n b d dh j) ∧
      hoeySloaneCarry n b d dh (k + 1) = 0

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Section 4 (the language L and L-walks).

Uses 2 · Used by 2

Statement usesEdges of the mother graph · Carries of the Hoey–Sloane machine

Used byHoey–Sloane words with permuted digits are unions of cycles · The string \((0,0)(2,3)(1,2)(3,1)\) lies in the \((2, 4)\)-Hoey–Sloane language

TheoremThe string \((0,0)(2,3)(1,2)(3,1)\) lies in the \((2, 4)\)-Hoey–Sloane language#✓fully proved

The input string \((d_0, \hat d_0) \cdots (d_3, \hat d_3) = (0,0)(2,3)(1,2)(3,1)\) belongs to the language \(L\) of the \((2, 4)\)-Hoey–Sloane machine.

This is the \((2, 4)\)-permutiple string of \((3, 1, 2, 0)_4 = 216 = 2 \cdot 108 = 2 \cdot (1, 2, 3, 0)_4\).

public theorem isHoeySloaneWord_two_four_example :
    IsHoeySloaneWord 2 4 (k := 3) ![0, 2, 1, 3] ![0, 3, 2, 1]

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Example 1.

Uses 3

Statement usesHoey–Sloane words

Proof usesEdges of the mother graph · Carries of the Hoey–Sloane machine

TheoremConjugate rearrangements have the same graph#●ready to prove

Let \(d_0, \dots, d_k\) be natural numbers and let \(\pi_1, \pi_2, \tau_1, \tau_2\) be permutations of \(\{0, \dots, k\}\) with \(\pi_1 \tau_1 \pi_1^{-1} = \pi_2 \tau_2 \pi_2^{-1}\). Then the graph of the digits \(d_{\pi_1(0)}, \dots, d_{\pi_1(k)}\) with digit permutation \(\tau_1\) and the graph of the digits \(d_{\pi_2(0)}, \dots, d_{\pi_2(k)}\) with digit permutation \(\tau_2\) have the same edge set:

\[\{(d_{\pi_1(j)}, d_{\pi_1(\tau_1(j))}) : 0 \le j \le k\} = \{(d_{\pi_2(j)}, d_{\pi_2(\tau_2(j))}) : 0 \le j \le k\}.\]

The source assumes, for a base \(b\) and a multiplier \(n\) with \(1 < n < b\), that \((d_{\pi_1(k)}, \dots, d_{\pi_1(0)})_b\) is an \((n, b, \tau_1)\)-permutiple and that \((d_{\pi_2(k)}, \dots, d_{\pi_2(0)})_b\) is an \((n, b, \tau_2)\)-permutiple, together with a base permutiple \((d_k, \dots, d_0)_b\); these hypotheses are not needed.

public theorem_wanted permutipleGraphEdges_eq_of_conj {k : ℕ} (d : Fin (k + 1) → ℕ)
    (π₁ π₂ τ₁ τ₂ : Equiv.Perm (Fin (k + 1))) (hconj : π₁ * τ₁ * π₁⁻¹ = π₂ * τ₂ * π₂⁻¹) :
    permutipleGraphEdges (d ∘ π₁) τ₁ = permutipleGraphEdges (d ∘ π₂) τ₂

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Theorem 4.

Uses 1

Statement usesEdge set of the graph of a numeral

TheoremEvery permutiple has a cycle-preserving digit permutation#●ready to prove

Let \(n\), \(b\) and \(d_0, \dots, d_k\) be natural numbers and let \(\sigma\) be a permutation of \(\{0, \dots, k\}\) such that \((d_k, \dots, d_0)_b\) is an \((n, b, \sigma)\)-permutiple. Then there is a permutation \(\hat\sigma\) of \(\{0, \dots, k\}\) such that \((d_k, \dots, d_0)_b\) is also an \((n, b, \hat\sigma)\)-permutiple and the digits along each cycle of \(\hat\sigma\) are distinct: for all \(j \in \{0, \dots, k\}\) and all \(i \ge 0\), if \(d_{\hat\sigma^i(j)} = d_j\) then \(\hat\sigma^i(j) = j\).

Unlike the paper, no assumption \(1 < n < b\) is made.

public theorem_wanted exists_cyclePreserving_permutiple (n b : ℕ) {k : ℕ}
    (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ) :
    ∃ σ' : Equiv.Perm (Fin (k + 1)), IsPermutiple n b d σ' ∧
      ∀ (j : Fin (k + 1)) (i : ℕ), d ((σ' ^ i) j) = d j → (σ' ^ i) j = j

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Theorem 5, with Definition 5 (cycle-preserving permutations).

Uses 1

Statement usesPermutiples with a given digit permutation

TheoremPermutiple graphs are unions of simple cycles of the mother graph#●ready to prove

Let \(n \ge 1\) and \(b \ge 2\) be natural numbers, let \(\sigma\) be a permutation of \(\{0, \dots, k\}\), and let \((d_k, \dots, d_0)_b\) be an \((n, b, \sigma)\)-permutiple, where \((e_k, \dots, e_0)_b\) denotes the base-\(b\) numeral \(\sum_{j=0}^{k} e_j b^j\). Let \(E = \{(d_j, d_{\sigma(j)}) : 0 \le j \le k\}\) be the edge set of its graph. Then every pair in \(E\) is an edge of the \((n, b)\)-mother graph, and every \(e \in E\) lies on a directed cycle with distinct vertices all of whose edges are in \(E\): there are \(m \ge 0\) and pairwise distinct natural numbers \(v_0, \dots, v_m\) such that, with indices taken modulo \(m + 1\), \((v_i, v_{i+1}) \in E\) for every \(0 \le i \le m\) and \(e = (v_i, v_{i+1})\) for some \(i\).

public theorem_wanted permutipleGraphEdges_union_cycles (n b : ℕ) (hn : 1 ≤ n) (hb : 2 ≤ b)
    {k : ℕ} (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ) :
    (∀ e ∈ permutipleGraphEdges d σ, IsMotherGraphEdge n b e.1 e.2) ∧
      ∀ e ∈ permutipleGraphEdges d σ, ∃ (m : ℕ) (v : Fin (m + 1) → ℕ), Function.Injective v ∧
        (∀ i, (v i, v (finRotate (m + 1) i)) ∈ permutipleGraphEdges d σ) ∧
          ∃ i, e = (v i, v (finRotate (m + 1) i))

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Theorem 6, with Definition 6 (permutiple classes and their graphs).

Uses 3

Statement usesEdges of the mother graph · Permutiples with a given digit permutation · Edge set of the graph of a numeral

TheoremHoey–Sloane words with permuted digits are unions of cycles#●ready to prove

Let \(n \ge 1\) and \(b \ge 2\) be natural numbers, and let \(s = (d_0, \hat d_0) \cdots (d_k, \hat d_k)\) be an input string in the language \(L\) of the \((n, b)\)-Hoey–Sloane machine such that \(\hat d_j = d_{\sigma(j)}\) for all \(j\), for some permutation \(\sigma\) of \(\{0, \dots, k\}\). Let \(E = \{(d_j, \hat d_j) : 0 \le j \le k\}\) be the set of inputs of \(s\). Then every \(e \in E\) lies on a directed cycle with edges in \(E\): there are \(m \ge 0\) and pairwise distinct natural numbers \(v_0, \dots, v_m\) such that \((v_i, v_{i+1}) \in E\) for all \(0 \le i \le m\), with indices taken modulo \(m + 1\), and \(e = (v_i, v_{i+1})\) for some \(i\).

public theorem_wanted hoeySloaneWord_inputs_union_cycles (n b : ℕ) (hn : 1 ≤ n) (hb : 2 ≤ b)
    {k : ℕ} (d dh : Fin (k + 1) → ℕ) (hs : IsHoeySloaneWord n b d dh)
    (σ : Equiv.Perm (Fin (k + 1))) (hσ : dh = d ∘ σ) :
    ∀ e ∈ Finset.univ.image (fun j => (d j, dh j)), ∃ (m : ℕ) (v : Fin (m + 1) → ℕ),
      Function.Injective v ∧
        (∀ i, (v i, v (finRotate (m + 1) i)) ∈ Finset.univ.image (fun j => (d j, dh j))) ∧
          ∃ i, e = (v i, v (finRotate (m + 1) i))

Sources

• B. V. Holt, Finding Permutiples of a Known Base and Multiplier, INTEGERS 25 (2025), Article A13, Corollary 1.

Uses 1

Statement usesHoey–Sloane words

TheoremSample edges of the \((4, 10)\)-mother graph#✓fully proved

In the \((4, 10)\)-mother graph, \((2, 8)\) and \((9, 9)\) are edges and \((2, 1)\) is not. With \(\lambda\) the least non-negative residue modulo ten, \(\lambda(2 + 6 \cdot 8) = 0 \le 3\) and \(\lambda(9 + 6 \cdot 9) = 3 \le 3\), while \(\lambda(2 + 6 \cdot 1) = 8 > 3\).

public theorem isMotherGraphEdge_four_ten :
    IsMotherGraphEdge 4 10 2 8 ∧ IsMotherGraphEdge 4 10 9 9 ∧ ¬ IsMotherGraphEdge 4 10 2 1

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 4 and Example 1.

Uses 1

Statement usesEdges of the mother graph

DefinitionTransitions of the Hoey-Sloane machine#✓fully proved

Let \(n\), \(b\), \(c_1\), \(c_2\), \(d_1\) and \(d_2\) be natural numbers. The input \(e = (d_1, d_2)\) moves state \(c_1\) to state \(c_2\) in one transition of the \((n, b)\)-Hoey-Sloane machine \(\Gamma\) when \(c_1 < n\), \(c_2 < n\), \((d_1, d_2)\) is an edge of the \((n, b)\)-mother graph, and \(b c_2 - c_1 = n d_2 - d_1\) in the integers (Equation (1)).

public def IsHoeySloaneStep (n b c₁ c₂ : ℕ) (e : ℕ × ℕ) : Prop :=
  c₁ < n ∧ c₂ < n ∧ IsMotherGraphEdge n b e.1 e.2 ∧ (b : ℤ) * c₂ - c₁ = (n : ℤ) * e.2 - e.1

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3, Equation (1).

Uses 1 · Used by 4

Statement usesEdges of the mother graph

Used byRuns of the Hoey-Sloane machine · Hoey-Sloane transitions are transitions of the machine · Uniqueness of Hoey-Sloane transitions · A word in the \((4, 10)\)-Hoey-Sloane language

DefinitionRuns of the Hoey-Sloane machine#✓fully proved

Let \(n\), \(b\), \(c\) and \(c'\) be natural numbers and let \(s = e_1 e_2 \cdots e_m\) be a finite string of inputs, each a pair of natural numbers. The \((n, b)\)-Hoey-Sloane machine can go from state \(c\) to state \(c'\) reading \(s\) from left to right when there are natural numbers \(c_0, c_1, \dots, c_m\) with \(c_0 = c\) and \(c_m = c'\) such that, for each \(1 \le i \le m\), the input \(e_i\) moves state \(c_{i-1}\) to state \(c_i\) in one transition of the \((n, b)\)-Hoey-Sloane machine. For the empty string (\(m = 0\)) this says \(c = c'\).

public def IsHoeySloaneRun (n b : ℕ) : ℕ → List (ℕ × ℕ) → ℕ → Prop
  | c, [], c' => c = c'
  | c, e :: s, c' => ∃ c₂, IsHoeySloaneStep n b c c₂ e ∧ IsHoeySloaneRun n b c₂ s c'

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3.

Uses 1 · Used by 2

Statement usesTransitions of the Hoey-Sloane machine

Used byLanguage of the Hoey–Sloane machine · A word in the \((4, 10)\)-Hoey-Sloane language

DefinitionLanguage of the Hoey–Sloane machine#✓fully proved

For natural numbers \(n\) and \(b\), the language \(L\) of the \((n, b)\)-Hoey–Sloane machine is the set of strings \(s\) of pairs of natural numbers such that the machine, reading \(s\) from left to right, can go from state \(0\) to state \(0\). In particular the empty string belongs to \(L\).

public def hoeySloaneLanguage (n b : ℕ) : Set (List (ℕ × ℕ)) :=
  {s | IsHoeySloaneRun n b 0 s 0}

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3.

Uses 1 · Used by 3

Statement usesRuns of the Hoey-Sloane machine

Used byPermutiple strings · The permutiple string of \(87912 = 4 \cdot 21978\) · A word in the \((4, 10)\)-Hoey-Sloane language

TheoremA word in the \((4, 10)\)-Hoey-Sloane language#✓fully proved

The input string \((2, 8)(1, 7)(9, 9)(7, 1)(8, 2)\) belongs to the language of the \((4, 10)\)-Hoey-Sloane machine: reading it from left to right, the machine can go from state \(0\) to state \(0\).

Writing \(87912 = (d_4, \dots, d_0)_{10}\) and letting \(\sigma\) be the digit reversal \(\sigma(j) = 4 - j\), so that \(87912 = 4 \cdot (d_{\sigma(4)}, \dots, d_{\sigma(0)})_{10}\) is \(4 \cdot 21978\), the inputs are the pairs \((d_j, d_{\sigma(j)})\) for \(j = 0, \dots, 4\); an accepting run passes through the states \(0, 3, 3, 3, 0, 0\).

public theorem mem_hoeySloaneLanguage_87912 :
    [(2, 8), (1, 7), (9, 9), (7, 1), (8, 2)] ∈ hoeySloaneLanguage 4 10

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3 and Example 2.

Uses 4 · Used by 1

Statement usesLanguage of the Hoey–Sloane machine

Proof usesRuns of the Hoey-Sloane machine · Transitions of the Hoey-Sloane machine · Edges of the mother graph

Used byThe permutiple string of \(87912 = 4 \cdot 21978\)

DefinitionPermutiple strings#✓fully proved

Let \(n\) and \(b\) be natural numbers, and for natural numbers \(a_0, \dots, a_k\) write \((a_k, \dots, a_0)_b = \sum_{j=0}^{k} a_j b^j\). A string \(s\) of inputs (pairs of natural numbers) is an \((n, b)\)-permutiple string when it belongs to the language \(L\) of the \((n, b)\)-Hoey-Sloane machine and there are a natural number \(k\), natural numbers \(d_0, \dots, d_k\) and a permutation \(\sigma\) of \(\{0, \dots, k\}\) such that \((d_k, \dots, d_0)_b\) is an \((n, b, \sigma)\)-permutiple, that is, every \(d_j\) is less than \(b\) and \((d_k, \dots, d_0)_b = n (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\), and \(s = (d_0, d_{\sigma(0)})(d_1, d_{\sigma(1)}) \cdots (d_k, d_{\sigma(k)})\).

public def IsPermutipleString (n b : ℕ) (s : List (ℕ × ℕ)) : Prop :=
  s ∈ hoeySloaneLanguage n b ∧
    ∃ (k : ℕ) (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))),
      IsPermutiple n b d σ ∧ s = List.ofFn fun j => (d j, d (σ j))

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3.

Uses 2 · Used by 4

Statement usesPermutiples with a given digit permutation · Language of the Hoey–Sloane machine

Used by\(L\)-Eulerian criterion for permutiple strings · Eulerian circuits through zero yield permutiple strings · The permutiple string of \(87912 = 4 \cdot 21978\) · Inputs of a permutiple string lie on mother-graph cycles

TheoremThe permutiple string of \(87912 = 4 \cdot 21978\)#✓fully proved

The string of inputs \((2, 8)(1, 7)(9, 9)(7, 1)(8, 2)\) is a \((4, 10)\)-permutiple string. It is produced by the \((4, 10)\)-permutiple \(87912 = 4 \cdot 21978\), whose multiplication reverses the digits.

public theorem isPermutipleString_87912 :
    IsPermutipleString 4 10 [(2, 8), (1, 7), (9, 9), (7, 1), (8, 2)]

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3 and Table 1.

Uses 5

Statement usesPermutiple strings

Proof usesPermutiples with a given digit permutation · Language of the Hoey–Sloane machine · \(87912\) is a \((4, 10)\)-permutiple by digit reversal · A word in the \((4, 10)\)-Hoey-Sloane language

DefinitionEdge list of a closed walk#✓fully proved

For a list \([v_0, \dots, v_{r-1}]\) of natural numbers, read as the vertex list of a closed walk, the edge list is \([(v_0, v_1), \dots, (v_{r-2}, v_{r-1}), (v_{r-1}, v_0)]\): each vertex is paired with the next one, and the last vertex with the first. A single vertex \([v_0]\) gives the loop \([(v_0, v_0)]\), and the empty list gives the empty edge list.

public def cycleEdges (vs : List ℕ) : List (ℕ × ℕ) :=
  vs.zip (vs.rotate 1)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 5 (cycles of M).

Used by 3

Used byEdges of the closed walks \(2 \to 8 \to 2\) and \(9 \to 9\) · Multiset union of cycle edges · Cycles of the mother graph

TheoremEdges of the closed walks \(2 \to 8 \to 2\) and \(9 \to 9\)#✓fully proved

The closed walk with vertex list \([2, 8]\) has edge list \([(2, 8), (8, 2)]\), and the closed walk with vertex list \([9]\) (a loop at \(9\)) has edge list \([(9, 9)]\).

public theorem cycleEdges_examples :
    cycleEdges [2, 8] = [(2, 8), (8, 2)] ∧ cycleEdges [9] = [(9, 9)]

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Example 2.

Uses 1

Statement usesEdge list of a closed walk

DefinitionCycles of the mother graph#✓fully proved

Let \(n\) and \(b\) be natural numbers. A list \([v_0, \dots, v_{r-1}]\) of natural numbers is a (directed) cycle of the \((n, b)\)-mother graph when it is nonempty, has no repeated entry, and each of its edges \((v_0, v_1), \dots, (v_{r-2}, v_{r-1}), (v_{r-1}, v_0)\) is an edge of the \((n, b)\)-mother graph. In particular a one-element list \([v]\) is a cycle when \((v, v)\) is an edge of the mother graph.

public def IsMotherGraphCycle (n b : ℕ) (vs : List ℕ) : Prop :=
  vs ≠ [] ∧ vs.Nodup ∧ ∀ e ∈ cycleEdges vs, IsMotherGraphEdge n b e.1 e.2

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 5 (cycles of M).

Uses 2 · Used by 2

Statement usesEdges of the mother graph · Edge list of a closed walk

Used by\(L\)-Eulerian criterion for permutiple strings · Eulerian circuits through zero yield permutiple strings

DefinitionMultiset union of cycle edges#✓fully proved

For a multiset \(I\) of lists of natural numbers, each read as the vertex list of a closed walk, write \(C_j\) for the edge list of \(j \in I\). The multiset union \(C_I = \biguplus_{j \in I} C_j\) is the multiset of all these edges, counted with multiplicity: each list \(j\) contributes its edges as often as \(j\) occurs in \(I\).

public def cycleUnion (cs : Multiset (List ℕ)) : Multiset (ℕ × ℕ) :=
  cs.bind fun vs => (cycleEdges vs : Multiset (ℕ × ℕ))

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 2.3 (multiset cycle union C_I).

Uses 1 · Used by 3

Statement usesEdge list of a closed walk

Used by\(L\)-Eulerian criterion for permutiple strings · Eulerian circuits through zero yield permutiple strings · Multi-image union of a multiset of cycles

DefinitionHoey–Sloane transition of a digit pair#✓fully proved

For natural numbers \(n\) and \(b\) and a pair \(e = (d_1, d_2)\) of natural numbers, the multi-edge of the \((n, b)\)-Hoey–Sloane multigraph carrying the label \(e\) is \((c_1, c_2)\), where \(c_1 = \lambda(d_1 + (b - n) d_2)\) with \(\lambda\) the least non-negative residue modulo \(b\) (computed in the integers), and \(c_2 = \lfloor (n d_2 - d_1 + c_1) / b \rfloor\), replaced by \(0\) when negative. For \(b = 0\) the conventions are \(x \bmod 0 = x\) and \(x / 0 = 0\), and \(c_1\) is likewise replaced by \(0\) when negative.

For an edge \(e\) of the \((n, b)\)-mother graph with \(1 < n < b\), the source shows that \((c_1, c_2)\) is the unique solution of \(b c_2 - c_1 = n d_2 - d_1\) with \(0 \le c_1, c_2 \le n - 1\), that is, the transition of the Hoey–Sloane machine with input \(e\).

public def hoeySloaneTransition (n b : ℕ) (e : ℕ × ℕ) : ℕ × ℕ :=
  let c₁ : ℤ := ((e.1 : ℤ) + ((b : ℤ) - n) * e.2) % b
  (c₁.toNat, (((n : ℤ) * e.2 - e.1 + c₁) / b).toNat)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 6 and the proof of Theorem 6.

Used by 3

Used byTwo multi-edges of the \((4, 10)\)-Hoey–Sloane multigraph · Hoey-Sloane transitions are transitions of the machine · Multi-image union of a multiset of cycles

TheoremTwo multi-edges of the \((4, 10)\)-Hoey–Sloane multigraph#✓fully proved

In the \((4, 10)\)-Hoey–Sloane multigraph the label \((2, 8)\) sits on the multi-edge from state \(0\) to state \(3\), and the label \((1, 7)\) sits on the loop at state \(3\): the Hoey–Sloane transition sends \((2, 8)\) to \((0, 3)\) and \((1, 7)\) to \((3, 3)\).

public theorem hoeySloaneTransition_four_ten :
    hoeySloaneTransition 4 10 (2, 8) = (0, 3) ∧ hoeySloaneTransition 4 10 (1, 7) = (3, 3)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 6 and Figure 4.

Uses 1

Statement usesHoey–Sloane transition of a digit pair

DefinitionMulti-image union of a multiset of cycles#✓fully proved

Let \(n\) and \(b\) be natural numbers and let \(I\) be a multiset of vertex lists. Let \(C_I\) be the multiset cycle union of \(I\): the multiset sum, over the lists in \(I\), of their edges, where a nonempty list \([v_0, \dots, v_{r-1}]\) has the edges \((v_0, v_1), \dots, (v_{r-2}, v_{r-1}), (v_{r-1}, v_0)\) and the empty list has none. The multi-image union \(\Delta_I\) is the multiset obtained by replacing each edge \(e = (d_1, d_2)\) of \(C_I\), with its multiplicity, by the multi-edge \((c_1, c_2)\) of the \((n, b)\)-Hoey-Sloane multigraph that carries the label \(e\): \(c_1 = \lambda(d_1 + (b - n) d_2)\), where \(\lambda\) is the least non-negative residue modulo \(b\) computed in the integers (the identity when \(b = 0\)), and \(c_2 = \lfloor (n d_2 - d_1 + c_1) / b \rfloor\) (taken to be \(0\) when \(b = 0\)), with a negative value of \(c_1\) or \(c_2\) replaced by \(0\).

The labels are dropped, since they do not affect in- and out-degrees, connectivity or Eulerian circuits.

public def multiImageUnion (n b : ℕ) (cs : Multiset (List ℕ)) : Multiset (ℕ × ℕ) :=
  (cycleUnion cs).map (hoeySloaneTransition n b)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 7.

Uses 2 · Used by 2

Statement usesMultiset union of cycle edges · Hoey–Sloane transition of a digit pair

Used by\(L\)-Eulerian criterion for permutiple strings · Eulerian circuits through zero yield permutiple strings

DefinitionEulerian circuit through the zero state#✓fully proved

Read a multiset \(D\) of pairs of natural numbers as the multi-edges \((c_1, c_2)\) of a directed multigraph. Then \(D\) has an Eulerian circuit beginning and ending with the zero state when there is a nonempty list of pairs whose multiset of entries is \(D\) (so it uses every multi-edge exactly once), in which each multi-edge ends where the next one begins, the first one starts at \(0\) and the last one ends at \(0\).

public def HasEulerianCircuitFromZero (D : Multiset (ℕ × ℕ)) : Prop :=
  ∃ w : List (ℕ × ℕ), w ≠ [] ∧ (w : Multiset (ℕ × ℕ)) = D ∧
    w.IsChain (fun x y => x.2 = y.1) ∧ w.head?.map Prod.fst = some 0 ∧
    w.getLast?.map Prod.snd = some 0

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Theorem 7 (hypothesis).

Used by 1

Used byEulerian circuits through zero yield permutiple strings

Definition\(L\)-Eulerian multigraphs#✓fully proved

Let \(D\) be a finite multiset of multi-edges \((x, y)\) between natural numbers, and call a number a vertex of \(D\) when it is an endpoint of some multi-edge in \(D\). The multigraph \(D\) is \(L\)-Eulerian when \(0\) is a vertex of \(D\), every vertex \(u\) of \(D\) reaches every vertex \(v\) of \(D\) along a (possibly empty) directed path of multi-edges in \(D\), and for every natural number \(c\) the number of multi-edges in \(D\) ending at \(c\) equals the number of multi-edges in \(D\) starting at \(c\), counted with multiplicity.

public def IsLEulerian (D : Multiset (ℕ × ℕ)) : Prop :=
  (∃ x ∈ D, x.1 = 0 ∨ x.2 = 0) ∧
    (∀ u v, (∃ x ∈ D, x.1 = u ∨ x.2 = u) → (∃ x ∈ D, x.1 = v ∨ x.2 = v) →
      Relation.ReflTransGen (fun x y => (x, y) ∈ D) u v) ∧
    ∀ c, D.countP (fun x => x.2 = c) = D.countP (fun x => x.1 = c)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Section 4 (definition of L-Eulerian, before Corollary 2).

Used by 1

Used by\(L\)-Eulerian criterion for permutiple strings

TheoremEdge condition for permutiples#●ready to prove

Let \(n \ge 1\), \(b\) and \(k\) be natural numbers, let \(\sigma\) be a permutation of \(\{0, \dots, k\}\) and let \((d_k, \dots, d_0)_b\) be an \((n, b, \sigma)\)-permutiple, that is, \(d_i < b\) for all \(i\) and \((d_k, \dots, d_0)_b = n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\). Then for every \(0 \le j \le k\), \(\lambda(d_j + (b - n) d_{\sigma(j)}) \le n - 1\), where \(\lambda\) is the least non-negative residue modulo \(b\) and \(b - n\) is computed in the integers, so it may be negative.

The hypothesis \(n \ge 1\) is needed: for \(n = 0\) the only permutiples have all digits zero and the bound would read \(0 \le -1\).

public theorem_wanted permutiple_edge_residue_le (n b : ℕ) (hn : 1 ≤ n) {k : ℕ}
    (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ)
    (j : Fin (k + 1)) :
    ((d j : ℤ) + ((b : ℤ) - n) * d (σ j)) % b ≤ (n : ℤ) - 1

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Theorem 3, quoting Holt, Finding Permutiples of a Known Base and Multiplier.

Uses 1

Statement usesPermutiples with a given digit permutation

TheoremEdges of a permutiple's graph lie on cycles of the mother graph#●ready to prove

Let \(n \ge 1\), \(b\) and \(k\) be natural numbers, let \(\sigma\) be a permutation of \(\{0, \dots, k\}\) and let \((d_k, \dots, d_0)_b\) be an \((n, b, \sigma)\)-permutiple, that is, \(d_i < b\) for all \(i\) and \((d_k, \dots, d_0)_b = n \cdot (d_{\sigma(k)}, \dots, d_{\sigma(0)})_b\). Its graph has the edges \((d_i, d_{\sigma(i)})\) for \(0 \le i \le k\). Then for every \(0 \le j \le k\), the pair \((d_j, d_{\sigma(j)})\) is an edge of the \((n, b)\)-mother graph, and \(d_j\) is reachable from \(d_{\sigma(j)}\) along edges of the graph of the permutiple (in zero steps when they are equal), so the edge \((d_j, d_{\sigma(j)})\) lies on a directed cycle of that graph.

public theorem_wanted permutiple_graph_isUnion_motherGraphCycles (n b : ℕ) (hn : 1 ≤ n) {k : ℕ}
    (d : Fin (k + 1) → ℕ) (σ : Equiv.Perm (Fin (k + 1))) (hp : IsPermutiple n b d σ)
    (j : Fin (k + 1)) :
    IsMotherGraphEdge n b (d j) (d (σ j)) ∧
      Relation.ReflTransGen (fun u v => ∃ i, d i = u ∧ d (σ i) = v) (d (σ j)) (d j)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Theorem 4, quoting Holt, Finding Permutiples of a Known Base and Multiplier.

Uses 2

Statement usesEdges of the mother graph · Permutiples with a given digit permutation

TheoremUniqueness of Hoey-Sloane transitions#●ready to prove

Let \(n \le b\). If an input \(e\) moves state \(c_1\) to state \(c_2\) and also moves state \(\hat c_1\) to state \(\hat c_2\), each in one transition of the \((n, b)\)-Hoey-Sloane machine, then \(c_1 = \hat c_1\) and \(c_2 = \hat c_2\).

The paper assumes \(1 < n < b\); here it is weakened to \(n \le b\). For \(n > b\) the claim can fail: for \(n = 3\) and \(b = 1\) the input \((0, 0)\) moves \(0\) to \(0\) and also \(1\) to \(1\).

public theorem_wanted isHoeySloaneStep_unique (n b : ℕ) (hnb : n ≤ b) {c₁ c₂ ĉ₁ ĉ₂ : ℕ}
    {e : ℕ × ℕ} (h : IsHoeySloaneStep n b c₁ c₂ e) (ĥ : IsHoeySloaneStep n b ĉ₁ ĉ₂ e) :
    c₁ = ĉ₁ ∧ c₂ = ĉ₂

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Theorem 5.

Uses 1

Statement usesTransitions of the Hoey-Sloane machine

TheoremEvery mother-graph edge induces a carry transition#●ready to prove

Let \(n\) and \(b\) be natural numbers. If \((d_1, d_2)\) is an edge of the \((n, b)\)-mother graph, then there are natural numbers \(c_1\) and \(c_2\) with \(c_1 \le n - 1\) and \(c_2 \le n - 1\) such that \(b c_2 - c_1 = n d_2 - d_1\) as integers.

public theorem_wanted exists_carries_of_isMotherGraphEdge (n b d₁ d₂ : ℕ)
    (h : IsMotherGraphEdge n b d₁ d₂) :
    ∃ c₁ c₂ : ℕ, c₁ ≤ n - 1 ∧ c₂ ≤ n - 1 ∧ (b : ℤ) * c₂ - c₁ = (n : ℤ) * d₂ - d₁

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Theorem 6.

Uses 1

Statement usesEdges of the mother graph

TheoremHoey-Sloane transitions are transitions of the machine#●ready to prove

Let \(1 < n < b\), let \(e = (d_1, d_2)\) be an edge of the \((n, b)\)-mother graph, and let \((c_1, c_2)\) be the Hoey-Sloane transition of \(e\), that is, \(c_1 = \lambda(d_1 + (b - n) d_2)\) and \(c_2 = (n d_2 - d_1 + c_1) / b\), where \(\lambda\) is the least non-negative residue modulo \(b\). Then the input \(e\) moves state \(c_1\) to state \(c_2\) in one transition of the \((n, b)\)-Hoey-Sloane machine.

By the uniqueness of Hoey-Sloane transitions (Theorem 5), it is the only transition labelled by \(e\).

public theorem_wanted isHoeySloaneStep_hoeySloaneTransition (n b : ℕ) (hn : 1 < n) (hnb : n < b)
    (e : ℕ × ℕ) (he : IsMotherGraphEdge n b e.1 e.2) :
    IsHoeySloaneStep n b (hoeySloaneTransition n b e).1 (hoeySloaneTransition n b e).2 e

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Definition 6, from Theorems 5 and 6.

Uses 3

Statement usesTransitions of the Hoey-Sloane machine · Edges of the mother graph · Hoey–Sloane transition of a digit pair

TheoremInputs of a permutiple string lie on mother-graph cycles#●ready to prove

Let \(1 < n < b\) and let \(s\) be an \((n, b)\)-permutiple string. Then every input \((d, \hat d)\) of \(s\) is an edge of the \((n, b)\)-mother graph, and \(\hat d\) reaches \(d\) along a (possibly empty) directed path in the graph whose edges are the inputs of \(s\), so \((d, \hat d)\) lies on a directed cycle of that graph. In this sense the inputs of \(s\) form a union of cycles of the mother graph.

public theorem_wanted isPermutipleString_inputs_isUnion_motherGraphCycles (n b : ℕ) (hn : 1 < n)
    (hnb : n < b) {s : List (ℕ × ℕ)} (hs : IsPermutipleString n b s) (e : ℕ × ℕ)
    (he : e ∈ s) :
    IsMotherGraphEdge n b e.1 e.2 ∧ Relation.ReflTransGen (fun u v => (u, v) ∈ s) e.2 e.1

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Corollary 1, quoting Holt, Finding Permutiples of a Known Base and Multiplier.

Uses 2

Statement usesEdges of the mother graph · Permutiple strings

TheoremEulerian circuits through zero yield permutiple strings#●ready to prove

Let \(1 < n < b\) and let \(I\) be a multiset of cycles of the \((n, b)\)-mother graph, with multiset union of cycle edges \(C_I\) and multi-image union \(\Delta_I\). If \(\Delta_I\) has an Eulerian circuit beginning and ending at the zero state, then there is an \((n, b)\)-permutiple string \(s\) whose multiset of entries is \(C_I\).

public theorem_wanted exists_isPermutipleString_of_hasEulerianCircuitFromZero (n b : ℕ) (hn : 1 < n)
    (hnb : n < b) (cs : Multiset (List ℕ)) (hcs : ∀ vs ∈ cs, IsMotherGraphCycle n b vs)
    (h : HasEulerianCircuitFromZero (multiImageUnion n b cs)) :
    ∃ s : List (ℕ × ℕ), (s : Multiset (ℕ × ℕ)) = cycleUnion cs ∧ IsPermutipleString n b s

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Theorem 7.

Uses 5

Statement usesEulerian circuit through the zero state · Cycles of the mother graph · Permutiple strings · Multiset union of cycle edges · Multi-image union of a multiset of cycles

Theorem\(L\)-Eulerian criterion for permutiple strings#●ready to prove

Let \(1 < n < b\) and let \(I\) be a multiset of cycles of the \((n, b)\)-mother graph, with multiset union of cycle edges \(C_I\) and multi-image union \(\Delta_I\). Then \(\Delta_I\) is \(L\)-Eulerian if and only if there is an \((n, b)\)-permutiple string \(s\) whose multiset of entries is \(C_I\).

public theorem_wanted exists_isPermutipleString_iff_isLEulerian (n b : ℕ) (hn : 1 < n) (hnb : n < b)
    (cs : Multiset (List ℕ)) (hcs : ∀ vs ∈ cs, IsMotherGraphCycle n b vs) :
    (∃ s : List (ℕ × ℕ), (s : Multiset (ℕ × ℕ)) = cycleUnion cs ∧ IsPermutipleString n b s) ↔
      IsLEulerian (multiImageUnion n b cs)

Sources

• Benjamin V. Holt, A Multigraph Characterization of Permutiple Strings, INTEGERS 25 (2025), Article A111, Corollary 2.

Uses 5

Statement uses\(L\)-Eulerian multigraphs · Cycles of the mother graph · Permutiple strings · Multiset union of cycle edges · Multi-image union of a multiset of cycles

28 fully proved15 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.