Josephus problem

DefinitionJosephus survivor function#✓fully proved

For natural numbers \(k\) and \(n\), the Josephus function \(J_k(n)\) is defined by recursion on \(n\): \(J_k(0) = 0\) and \(J_k(n+1) = ((J_k(n) + k - 1) \bmod (n+1)) + 1\), where subtraction of natural numbers is truncated at \(0\).

For \(k \ge 2\) and \(n \ge 1\), \(J_k(n)\) is the one-based position of the sole survivor when every \(k\)-th person is eliminated from a circle of \(n\) people; the value \(J_k(0) = 0\) only anchors the recursion.

public def josephus (k : Nat) : Nat → Nat
  | 0 => 0
  | (n + 1) => ((josephus k n + k - 1) % (n + 1)) + 1

Used by 32

Used byThe survivor is the last entry of the Josephus elimination order · Josephus survivor via iteration from zero · Josephus survivor via the shifted iteration · Logarithmic bounds for the Josephus iteration count · Extremal points of the Josephus function near \(2k - 2\) · The Josephus function has infinitely many fixed points · Fixed points of the Josephus function \(J_3\) · \(13\) is a fixed point of \(J_3\) · High extremal points of the Josephus function \(J_3\) · \(3\) is a high extremal point but not a fixed point of \(J_3\) · Low extremal point of the Josephus function · Linear growth of the Josephus function after a high extremal point · Linear growth of the Josephus function before a wrap-around · The Josephus function at the first wrap-around · Josephus fixed points detected by the next value · The Josephus function just after a fixed point · The Josephus function at one · Range of the Josephus function · Euler recurrence for the Josephus function · Josephus recurrence by number of wrap-arounds · The Josephus function between consecutive fixed points · Enumeration of the positive fixed points of \(J_3\) · Second positive fixed point of the Josephus function for step three · Recurrence for consecutive fixed points of \(J_3\) · The third positive fixed point of \(J_3\) is \(13\) · The first positive fixed point of \(J_3\) is \(1\) · Gaps between consecutive positive fixed points of \(J_3\) · The second gap between positive fixed points of \(J_3\) is \(3\) · Unified recurrences for consecutive high extremal points of \(J_3\) · Successive high extremal points of \(J_3\) · \(4\) is not a high extremal point of \(J_3\) · Linear-step bound at a low extremal point

TheoremThe Josephus function at one#✓fully proved

For every natural number \(k \ge 2\), the Josephus function \(J_k\) for elimination step \(k\) satisfies \(J_k(1) = 1\).

public theorem josephus_one (k : Nat) (_hk : 2 ≤ k) : josephus k 1 = 1

Uses 1

Statement usesJosephus survivor function

TheoremEuler recurrence for the Josephus function#✓fully proved

For all natural numbers \(k \ge 2\) and \(n \ge 1\), the Josephus function \(J_k\) for elimination step \(k\) satisfies \(J_k(n+1) = ((J_k(n) + k - 1) \bmod (n+1)) + 1\).

public theorem josephus_succ (k n : Nat) (_hk : 2 ≤ k) (_hn : 1 ≤ n) :
    josephus k (n + 1) = ((josephus k n + k - 1) % (n + 1)) + 1

Uses 1

Statement usesJosephus survivor function

TheoremRange of the Josephus function#✓fully proved

For all natural numbers \(k \ge 2\) and \(n \ge 1\), the Josephus function \(J_k\) for elimination step \(k\) satisfies \(1 \le J_k(n) \le n\).

public theorem josephus_range (k n : Nat) (_hk : 2 ≤ k) (hn : 1 ≤ n) :
    1 ≤ josephus k n ∧ josephus k n ≤ n

Uses 1

Statement usesJosephus survivor function

DefinitionEnumeration of the positive fixed points of \(J_3\)#✓fully proved

Let \(J_3\) be the Josephus function with step \(3\). For \(\ell \in \mathbb{N}\), \(n_\ell\) is the \(\ell\)-th element, in increasing order and counting from \(\ell = 0\), of the set of natural numbers \(n \ge 1\) with \(J_3(n) = n\). Thus \(n_\ell\) is the paper's \(n_p^{(\ell+1)}\).

If this set has at most \(\ell\) elements, then \(n_\ell = 0\) by convention.

public noncomputable def josephusThreeFixedPoint (ℓ : ℕ) : ℕ :=
  Nat.nth (fun n => 1 ≤ n ∧ josephus 3 n = n) ℓ

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 1 · Used by 9

Statement usesJosephus survivor function

Used byDigit count of consecutive Josephus fixed points · Base-3/2 digits of the next Josephus fixed point, gap zero · Base-3/2 digits of the next Josephus fixed point, gap one · Base-3/2 digits of the next Josephus fixed point, gap at least two · Second positive fixed point of the Josephus function for step three · The third positive fixed point of \(J_3\) is \(13\) · The first positive fixed point of \(J_3\) is \(1\) · Gaps between consecutive positive fixed points of \(J_3\) · The second gap between positive fixed points of \(J_3\) is \(3\)

DefinitionGaps between consecutive positive fixed points of \(J_3\)#✓fully proved

Let \(J_3\) be the Josephus function with step \(3\) and let \(n_\ell\) be the \(\ell\)-th natural number \(n \ge 1\) with \(J_3(n) = n\), in increasing order and counting from \(\ell = 0\). For \(\ell \in \mathbb{N}\), the gap \(g_\ell\) is the number of natural numbers \(n\) with \(n_\ell < n < n_{\ell+1}\) and \(J_3(n) + 1 = n\), that is, the number of pure high extremal points strictly between \(n_\ell\) and \(n_{\ell+1}\). Thus \(g_\ell\) is the paper's \(\bar m_{\ell+1}\).

public noncomputable def josephusThreeGap (ℓ : ℕ) : ℕ :=
  ((Finset.Ioo (josephusThreeFixedPoint ℓ) (josephusThreeFixedPoint (ℓ + 1))).filter
    (fun n => josephus 3 n + 1 = n)).card

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 2 · Used by 5

Statement usesJosephus survivor function · Enumeration of the positive fixed points of \(J_3\)

Used byDigit count of consecutive Josephus fixed points · Base-3/2 digits of the next Josephus fixed point, gap zero · Base-3/2 digits of the next Josephus fixed point, gap one · Base-3/2 digits of the next Josephus fixed point, gap at least two · The second gap between positive fixed points of \(J_3\) is \(3\)

DefinitionBase-3/2 digits#✓fully proved

The base-\(3/2\) digit list of a natural number \(N\), least significant digit first, is defined by recursion on \(N\): the list of \(0\) is empty, and for \(N \ge 1\) it is the digit \(d = 2N \bmod 3\) followed by the base-\(3/2\) digit list of \((2N - d)/3\).

public def baseThreeHalvesDigits : ℕ → List ℕ
  | 0 => []
  | N + 1 =>
    let d := 2 * (N + 1) % 3
    d :: baseThreeHalvesDigits ((2 * (N + 1) - d) / 3)
  termination_by N => N
  decreasing_by omega

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Used by 8

Used byBase-3/2 digits of four · Base-3/2 digits are at most two · Base-3/2 digits of thirteen · Value of the base-3/2 digits · Digit count of consecutive Josephus fixed points · Base-3/2 digits of the next Josephus fixed point, gap zero · Base-3/2 digits of the next Josephus fixed point, gap one · Base-3/2 digits of the next Josephus fixed point, gap at least two

TheoremBase-3/2 digits of four#✓fully proved

The base-\(3/2\) digit list of \(4\), written least significant digit first, is \((2, 1, 2)\); written most significant digit first, this is the paper's \((212)_{3/2}\).

public theorem baseThreeHalvesDigits_four : baseThreeHalvesDigits 4 = [2, 1, 2]

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 1

Statement usesBase-3/2 digits

TheoremBase-3/2 digits of thirteen#✓fully proved

The base-\(3/2\) digit list of \(13\), written least significant digit first, is \((2, 1, 1, 0, 1, 2)\); written most significant digit first, this is the paper's \((210112)_{3/2}\).

public theorem baseThreeHalvesDigits_thirteen :
    baseThreeHalvesDigits 13 = [2, 1, 1, 0, 1, 2]

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 1

Statement usesBase-3/2 digits

TheoremValue of the base-3/2 digits#✓fully proved

For every natural number \(N\), if \((d_0, d_1, \dots, d_{k-1})\) is the base-\(3/2\) digit list of \(N\), least significant digit first, then in \(\mathbb{Q}\)

\[2N = \sum_{i=0}^{k-1} d_i \left(\frac{3}{2}\right)^i.\]

Equivalently, the paper's expansion \(\frac{1}{2} \sum_{i} d_i (3/2)^i\) has value \(N\).

public theorem baseThreeHalvesDigits_value (N : ℕ) :
    2 * (N : ℚ) =
      ∑ i : Fin (baseThreeHalvesDigits N).length,
        (baseThreeHalvesDigits N)[i] * (3 / 2 : ℚ) ^ (i : ℕ)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 1

Statement usesBase-3/2 digits

TheoremBase-3/2 digits are at most two#✓fully proved

For every natural number \(N\), every digit \(d\) in the base-\(3/2\) digit list of \(N\) satisfies \(d < 3\), that is, \(d \in \{0, 1, 2\}\).

public theorem baseThreeHalvesDigits_lt_three (N d : ℕ)
    (hd : d ∈ baseThreeHalvesDigits N) : d < 3

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 1

Statement usesBase-3/2 digits

TheoremThe first positive fixed point of \(J_3\) is \(1\)#✓fully proved

Let \(J_3\) be the Josephus function with step \(3\) and let \(n_\ell\) be the \(\ell\)-th natural number \(n \ge 1\) with \(J_3(n) = n\), in increasing order and counting from \(\ell = 0\). Then \(n_0 = 1\); this is the paper's \(n_p^{(1)}\).

public theorem josephusThreeFixedPoint_zero : josephusThreeFixedPoint 0 = 1

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 2

Statement usesEnumeration of the positive fixed points of \(J_3\)

Proof usesJosephus survivor function

TheoremSecond positive fixed point of the Josephus function for step three#✓fully proved

Let \(J_3\) be the Josephus function with elimination step \(3\). The second smallest positive integer \(n\) with \(J_3(n) = n\) is \(2\); in the zero-indexed enumeration \(n_0 < n_1 < \cdots\) of these fixed points, \(n_1 = 2\), the paper's \(n_p^{(2)}\).

public theorem josephusThreeFixedPoint_one : josephusThreeFixedPoint 1 = 2

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 2 · Used by 1

Statement usesEnumeration of the positive fixed points of \(J_3\)

Proof usesJosephus survivor function

Used byThe second gap between positive fixed points of \(J_3\) is \(3\)

TheoremThe third positive fixed point of \(J_3\) is \(13\)#✓fully proved

Let \(J_3\) be the Josephus function with step \(3\) and let \(n_\ell\) be the \(\ell\)-th natural number \(n \ge 1\) with \(J_3(n) = n\), in increasing order and counting from \(\ell = 0\). Then \(n_2 = 13\); this is the paper's \(n_p^{(3)}\).

public theorem josephusThreeFixedPoint_two : josephusThreeFixedPoint 2 = 13

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 2 · Used by 1

Statement usesEnumeration of the positive fixed points of \(J_3\)

Proof usesJosephus survivor function

Used byThe second gap between positive fixed points of \(J_3\) is \(3\)

TheoremThe second gap between positive fixed points of \(J_3\) is \(3\)#✓fully proved

Let \(J_3\) be the Josephus function with step \(3\), let \(n_\ell\) be the \(\ell\)-th natural number \(n \ge 1\) with \(J_3(n) = n\) (in increasing order, counting from \(\ell = 0\)), and let \(g_\ell\) be the number of natural numbers \(n\) with \(n_\ell < n < n_{\ell+1}\) and \(J_3(n) + 1 = n\). Then \(g_1 = 3\); this is the paper's \(\bar m_2 = 3\).

Here \(n_1 = 2\) and \(n_2 = 13\), and the three pure high extremal points counted are \(3\), \(5\) and \(8\).

public theorem josephusThreeGap_one : josephusThreeGap 1 = 3

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 5

Statement usesGaps between consecutive positive fixed points of \(J_3\)

Proof usesJosephus survivor function · Enumeration of the positive fixed points of \(J_3\) · Second positive fixed point of the Josephus function for step three · The third positive fixed point of \(J_3\) is \(13\)

TheoremBase-3/2 digits of the next Josephus fixed point, gap zero#●ready to prove

Let \(J_3\) be the Josephus function with elimination step \(3\), let \(n_\ell\) be the \(\ell\)-th positive fixed point of \(J_3\) in increasing order (counting from \(\ell = 0\)), and let \(m_\ell\) be the number of integers \(n\) with \(n_\ell < n < n_{\ell+1}\) and \(J_3(n) + 1 = n\) (the pure high extremal points between them). For every \(\ell\), if \(m_\ell = 0\), then the base-\(3/2\) digit list of \(n_{\ell+1}\), least significant digit first, is the digit \(1\) followed by the digit list of \(n_\ell\).

This is part (i) of the cited Theorem 1.

public theorem_wanted josephusThreeFixedPoint_digits_of_gap_zero (ℓ : ℕ) :
    let D := baseThreeHalvesDigits (josephusThreeFixedPoint ℓ)
    let E := baseThreeHalvesDigits (josephusThreeFixedPoint (ℓ + 1))
    let m := josephusThreeGap ℓ
    m = 0 → E = 1 :: D

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 3

Statement usesBase-3/2 digits · Enumeration of the positive fixed points of \(J_3\) · Gaps between consecutive positive fixed points of \(J_3\)

TheoremBase-3/2 digits of the next Josephus fixed point, gap one#●ready to prove

Let \(J_3\) be the Josephus function with elimination step \(3\), let \(n_\ell\) be the \(\ell\)-th positive fixed point of \(J_3\) in increasing order (counting from \(\ell = 0\)), and let \(m_\ell\) be the number of integers \(n\) with \(n_\ell < n < n_{\ell+1}\) and \(J_3(n) + 1 = n\) (the pure high extremal points between them). For every \(\ell\), if \(m_\ell = 1\), then the base-\(3/2\) digit list of \(n_{\ell+1}\), least significant digit first, is the digits \(2, 0\) followed by the digit list of \(n_\ell\).

This is part (ii) of the cited Theorem 1.

public theorem_wanted josephusThreeFixedPoint_digits_of_gap_one (ℓ : ℕ) :
    let D := baseThreeHalvesDigits (josephusThreeFixedPoint ℓ)
    let E := baseThreeHalvesDigits (josephusThreeFixedPoint (ℓ + 1))
    let m := josephusThreeGap ℓ
    m = 1 → E = [2, 0] ++ D

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 3

Statement usesBase-3/2 digits · Enumeration of the positive fixed points of \(J_3\) · Gaps between consecutive positive fixed points of \(J_3\)

TheoremBase-3/2 digits of the next Josephus fixed point, gap at least two#●ready to prove

Let \(J_3\) be the Josephus function with elimination step \(3\), let \(n_\ell\) be the \(\ell\)-th positive fixed point of \(J_3\) in increasing order (counting from \(\ell = 0\)), and let \(m_\ell\) be the number of integers \(n\) with \(n_\ell < n < n_{\ell+1}\) and \(J_3(n) + 1 = n\) (the pure high extremal points between them). For every \(\ell\), if \(m_\ell \ge 2\), then the base-\(3/2\) digit list of \(n_{\ell+1}\), least significant digit first, is the digit \(2\), then \(m_\ell - 1\) digits equal to \(1\), then the digit \(0\), followed by the digit list of \(n_\ell\).

Written most significant digit first, this appends to the digits of \(n_\ell\) a \(0\), then \(m_\ell - 1\) ones, then a \(2\). This is part (iii) of the cited Theorem 1.

public theorem_wanted josephusThreeFixedPoint_digits_of_gap_at_least_two (ℓ : ℕ) :
    let D := baseThreeHalvesDigits (josephusThreeFixedPoint ℓ)
    let E := baseThreeHalvesDigits (josephusThreeFixedPoint (ℓ + 1))
    let m := josephusThreeGap ℓ
    2 ≤ m → E = 2 :: List.replicate (m - 1) 1 ++ 0 :: D

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 3

Statement usesBase-3/2 digits · Enumeration of the positive fixed points of \(J_3\) · Gaps between consecutive positive fixed points of \(J_3\)

TheoremDigit count of consecutive Josephus fixed points#●ready to prove

Let \(J_3\) be the Josephus function with elimination step \(3\), let \(n_\ell\) be the \(\ell\)-th positive fixed point of \(J_3\) in increasing order (counting from \(\ell = 0\)), and let \(m_\ell\) be the number of integers \(n\) with \(n_\ell < n < n_{\ell+1}\) and \(J_3(n) + 1 = n\) (the pure high extremal points between them). For every \(\ell\), the base-\(3/2\) digit list of \(n_{\ell+1}\) has exactly \(m_\ell + 1\) more digits than the base-\(3/2\) digit list of \(n_\ell\).

This is part (iv) of the cited Theorem 1.

public theorem_wanted josephusThreeFixedPoint_digits_length (ℓ : ℕ) :
    let D := baseThreeHalvesDigits (josephusThreeFixedPoint ℓ)
    let E := baseThreeHalvesDigits (josephusThreeFixedPoint (ℓ + 1))
    let m := josephusThreeGap ℓ
    E.length = D.length + m + 1

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, Fixed Points of the Josephus Function via Fractional Base Expansions, INTEGERS 26 (2026), Article A54, Theorem 1.

Uses 3

Statement usesBase-3/2 digits · Enumeration of the positive fixed points of \(J_3\) · Gaps between consecutive positive fixed points of \(J_3\)

DefinitionHigh extremal points of the Josephus function \(J_3\)#✓fully proved

A natural number \(n\) is a high extremal point of the Josephus function \(J_3\) (elimination step \(3\)) when \(n \ge 1\) and either \(J_3(n) = n\) or \(J_3(n) = n - 1\).

public def IsJosephusThreeHighExtremal (n : ℕ) : Prop :=
  1 ≤ n ∧ (josephus 3 n = n ∨ josephus 3 n + 1 = n)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Section 1, Definition (Extremal and Fixed points).

Uses 1 · Used by 4

Statement usesJosephus survivor function

Used by\(3\) is a high extremal point but not a fixed point of \(J_3\) · Unified recurrences for consecutive high extremal points of \(J_3\) · Successive high extremal points of \(J_3\) · \(4\) is not a high extremal point of \(J_3\)

DefinitionFixed points of the Josephus function \(J_3\)#✓fully proved

A natural number \(n\) is a fixed point of the Josephus function \(J_3\) (elimination step \(3\)) when \(n \ge 1\) and \(J_3(n) = n\).

public def IsJosephusThreeFixedPoint (n : ℕ) : Prop :=
  1 ≤ n ∧ josephus 3 n = n

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Section 1, Definition (Extremal and Fixed points).

Uses 1 · Used by 4

Statement usesJosephus survivor function

Used by\(13\) is a fixed point of \(J_3\) · \(3\) is a high extremal point but not a fixed point of \(J_3\) · The Josephus function between consecutive fixed points · Recurrence for consecutive fixed points of \(J_3\)

Theorem\(3\) is a high extremal point but not a fixed point of \(J_3\)#✓fully proved

The number \(3\) is a high extremal point of the Josephus function \(J_3\) (elimination step \(3\)) and is not a fixed point of \(J_3\); indeed \(J_3(3) = 2\).

public theorem isJosephusThreeHighExtremal_three :
    IsJosephusThreeHighExtremal 3 ∧ ¬ IsJosephusThreeFixedPoint 3

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Section 1, Definition (Extremal and Fixed points).

Uses 3

Statement usesFixed points of the Josephus function \(J_3\) · High extremal points of the Josephus function \(J_3\)

Proof usesJosephus survivor function

Theorem\(4\) is not a high extremal point of \(J_3\)#✓fully proved

The number \(4\) is not a high extremal point of the Josephus function \(J_3\) (elimination step \(3\)).

Indeed \(J_3(4) = 1\).

public theorem not_isJosephusThreeHighExtremal_four : ¬ IsJosephusThreeHighExtremal 4

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Section 1, Definition (Extremal and Fixed points).

Uses 2

Statement usesHigh extremal points of the Josephus function \(J_3\)

Proof usesJosephus survivor function

Theorem\(13\) is a fixed point of \(J_3\)#✓fully proved

The number \(13\) is a fixed point of the Josephus function \(J_3\) (elimination step \(3\)), that is, \(J_3(13) = 13\).

It is the third fixed point of \(J_3\), after \(1\) and \(2\); the statement records only that \(13\) is a fixed point.

public theorem isJosephusThreeFixedPoint_thirteen : IsJosephusThreeFixedPoint 13

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Section 2, Table 1.

Uses 2

Statement usesFixed points of the Josephus function \(J_3\)

Proof usesJosephus survivor function

TheoremSuccessive high extremal points of \(J_3\)#●ready to prove

For every natural number \(i\), let \(a\) and \(b\) be the \((i+1)\)-th and \((i+2)\)-th smallest high extremal points of the Josephus function \(J_3\), and put \(f = a - J_3(a)\), \(f' = b - J_3(b)\) and \(r = a \bmod 2\). If \((f, r) = (1, 0)\), then \(2b = 3a + 2\) and \(f' = 0\); if \((f, r) = (1, 1)\), then \(2b = 3a + 1\) and \(f' = 1\); if \((f, r) = (0, 0)\), then \(2b = 3a\) and \(f' = 1\); if \((f, r) = (0, 1)\), then \(2b = 3a + 1\) and \(f' = 0\).

public theorem_wanted josephusThree_highExtremal_succ_cases (i : ℕ) :
    let a := Nat.nth IsJosephusThreeHighExtremal i
    let b := Nat.nth IsJosephusThreeHighExtremal (i + 1)
    (a - josephus 3 a = 1 → a % 2 = 0 → 2 * b = 3 * a + 2 ∧ b - josephus 3 b = 0) ∧
    (a - josephus 3 a = 1 → a % 2 = 1 → 2 * b = 3 * a + 1 ∧ b - josephus 3 b = 1) ∧
    (a - josephus 3 a = 0 → a % 2 = 0 → 2 * b = 3 * a ∧ b - josephus 3 b = 1) ∧
    (a - josephus 3 a = 0 → a % 2 = 1 → 2 * b = 3 * a + 1 ∧ b - josephus 3 b = 0)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Theorem 1.

Uses 2

Statement usesHigh extremal points of the Josephus function \(J_3\) · Josephus survivor function

TheoremUnified recurrences for consecutive high extremal points of \(J_3\)#●ready to prove

For every natural number \(i\), let \(a\) and \(b\) be the \((i+1)\)-th and \((i+2)\)-th smallest high extremal points of the Josephus function \(J_3\). In the integers, put \(r = a \bmod 2\), \(f = a - J_3(a)\) and \(s = \lfloor (3a + 2 - r)/2 \rfloor \bmod 2\). Then

\[2b = 3a + 1 + (1 - r)(2f - 1), \qquad 2J_3(b) = 3a + (2 - 3r)(2f - 1),\]

\[b - J_3(b) = f - (1 - r)(2f - 1), \qquad b \bmod 2 = s - (1 - r)(1 - f)(2s - 1).\]

public theorem_wanted josephusThree_highExtremal_recurrences (i : ℕ) :
    let a := Nat.nth IsJosephusThreeHighExtremal i
    let b := Nat.nth IsJosephusThreeHighExtremal (i + 1)
    let r : ℤ := (a : ℤ) % 2
    let f : ℤ := (a : ℤ) - josephus 3 a
    let s : ℤ := ((3 * (a : ℤ) + 2 - r) / 2) % 2
    2 * (b : ℤ) = 3 * a + 1 + (1 - r) * (2 * f - 1) ∧
      2 * (josephus 3 b : ℤ) = 3 * a + (2 - 3 * r) * (2 * f - 1) ∧
      (b : ℤ) - josephus 3 b = f - (1 - r) * (2 * f - 1) ∧
      (b : ℤ) % 2 = s - (1 - r) * (1 - f) * (2 * s - 1)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Lemma 1.

Uses 2

Statement usesHigh extremal points of the Josephus function \(J_3\) · Josephus survivor function

TheoremRecurrence for consecutive fixed points of \(J_3\)#●ready to prove

For every natural number \(\ell\), let \(a\) and \(b\) be the \((\ell+1)\)-th and \((\ell+2)\)-th smallest fixed points of the Josephus function \(J_3\), and let \(m = \nu_2(3a + 2)\) be the \(2\)-adic valuation of \(3a + 2\). Then exactly \(m\) natural numbers \(n\) with \(a < n < b\) satisfy \(J_3(n) = n - 1\) (the pure high extremal points between \(a\) and \(b\)), and \(2^{m+1} b + 2^m = 3^m (3a + 2)\), that is, \(b = (3^m (3a + 2) - 2^m) / 2^{m+1}\).

public theorem_wanted josephusThree_fixedPoint_recurrence (ℓ : ℕ) :
    let a := Nat.nth IsJosephusThreeFixedPoint ℓ
    let b := Nat.nth IsJosephusThreeFixedPoint (ℓ + 1)
    ((Finset.Ioo a b).filter (fun n => josephus 3 n + 1 = n)).card =
        padicValNat 2 (3 * a + 2) ∧
      2 ^ (padicValNat 2 (3 * a + 2) + 1) * b + 2 ^ padicValNat 2 (3 * a + 2) =
        3 ^ padicValNat 2 (3 * a + 2) * (3 * a + 2)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Theorem 2.

Uses 2

Statement usesFixed points of the Josephus function \(J_3\) · Josephus survivor function

TheoremThe Josephus function between consecutive fixed points#●ready to prove

For every natural number \(\ell\), let \(a\) and \(b\) be the \((\ell+1)\)-th and \((\ell+2)\)-th smallest fixed points of the Josephus function \(J_3\), and let \(m = \nu_2(3a + 2)\) be the \(2\)-adic valuation of \(3a + 2\). For every natural number \(n\) with \(a + 1 \le n \le b\), put \(\mathfrak{m} = \lceil \log_{3/2}((2n + 1)/(3a + 2)) \rceil\); then, in the real numbers,

\[J_3(n) = 3n + 1 - \left(\tfrac{2}{3}\right)^{m - \mathfrak{m}} (2b + 1).\]

public theorem_wanted josephusThree_eq_of_mem_fixedPoint_interval (ℓ n : ℕ)
    (hn₁ : Nat.nth IsJosephusThreeFixedPoint ℓ + 1 ≤ n)
    (hn₂ : n ≤ Nat.nth IsJosephusThreeFixedPoint (ℓ + 1)) :
    (josephus 3 n : ℝ) =
      3 * n + 1 -
        (2 / 3 : ℝ) ^
            ((padicValNat 2 (3 * Nat.nth IsJosephusThreeFixedPoint ℓ + 2) : ℤ) -
              ⌈Real.logb (3 / 2)
                ((2 * n + 1) / (3 * Nat.nth IsJosephusThreeFixedPoint ℓ + 2))⌉) *
          (2 * Nat.nth IsJosephusThreeFixedPoint (ℓ + 1) + 1)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, On the Recurrence Formula for Fixed Points of the Josephus Function, INTEGERS 24 (2024), Article A115, Theorem 3.

Uses 2

Statement usesFixed points of the Josephus function \(J_3\) · Josephus survivor function

DefinitionLow extremal point of the Josephus function#✓fully proved

For natural numbers \(k\) and \(m\), the point \(m\) is a low extremal point of the Josephus function \(J_k\) if \(1 \le J_k(m) \le k - 1\), where \(k - 1\) is truncated at \(0\).

def IsLowExtremal (k m : ℕ) : Prop :=
  1 ≤ MetaMathlibExt.josephus k m ∧
    MetaMathlibExt.josephus k m ≤ k - 1

Uses 1 · Used by 2

Statement usesJosephus survivor function

Used byExtremal points of the Josephus function near \(2k - 2\) · High extremal point of the Josephus function

DefinitionHigh extremal point of the Josephus function#✓fully proved

For natural numbers \(k\) and \(m\), the point \(m\) is a high extremal point of the Josephus function \(J_k\) if \(m + 1\) is a low extremal point of \(J_k\), that is, if \(1 \le J_k(m + 1) \le k - 1\).

def IsHighExtremal (k m : ℕ) : Prop := IsLowExtremal k (m + 1)

Uses 1 · Used by 2

Statement usesLow extremal point of the Josephus function

Used byExtremal points of the Josephus function near \(2k - 2\) · Linear growth of the Josephus function after a high extremal point

TheoremJosephus recurrence by number of wrap-arounds#●ready to prove

Let \(k \ge 2\) and \(n \ge 1\) be natural numbers, let \(J_k\) be the Josephus function and write \(p = J_k(n)\). If \(\ell\) is a natural number with \(\ell(n+1) + 1 \le p + k \le (\ell+1)(n+1)\), then \(J_k(n+1) = p + k - \ell(n+1)\).

theorem_wanted josephus_succ_eq_sub (k n ℓ : ℕ) (hk : 2 ≤ k)
    (hn : 1 ≤ n)
    (h : ℓ * (n + 1) + 1 ≤ MetaMathlibExt.josephus k n + k ∧
      MetaMathlibExt.josephus k n + k ≤ (ℓ + 1) * (n + 1)) :
    MetaMathlibExt.josephus k (n + 1) =
      MetaMathlibExt.josephus k n + k - ℓ * (n + 1)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Theorem 2.

Uses 1

Statement usesJosephus survivor function

TheoremThe Josephus function just after a fixed point#●ready to prove

Let \(k \ge 2\) and \(n_p \ge 1\) be natural numbers with \(J_k(n_p) = n_p\), where \(J_k\) is the Josephus function. Then \(J_k(n_p + 1)\) is determined as follows: (i) if \(k \le n_p + 1\), then \(J_k(n_p + 1) = k - 1\); (ii) if \(k = \ell(n_p + 1) + 1\) for some natural number \(\ell \ge 1\), then \(J_k(n_p + 1) = n_p + 1\); (iii) if \(k = \ell(n_p + 1) + k_1\) for some natural numbers \(\ell \ge 1\) and \(k_1\) with \(2 \le k_1 \le n_p\), then \(J_k(n_p + 1) = k_1 - 1\); (iv) if \(k = (\ell + 1)(n_p + 1)\) for some natural number \(\ell \ge 1\), then \(J_k(n_p + 1) = n_p\).

theorem_wanted josephus_fixed_succ_cases (k np : ℕ)
    (hk : 2 ≤ k) (hnp : 1 ≤ np)
    (hfix : MetaMathlibExt.josephus k np = np) :
    (k ≤ np + 1 → MetaMathlibExt.josephus k (np + 1) = k - 1) ∧
    (∀ ℓ : ℕ, 1 ≤ ℓ → k = ℓ * (np + 1) + 1 →
      MetaMathlibExt.josephus k (np + 1) = np + 1) ∧
    (∀ ℓ k1 : ℕ, 1 ≤ ℓ → 2 ≤ k1 → k1 ≤ np →
      k = ℓ * (np + 1) + k1 →
        MetaMathlibExt.josephus k (np + 1) = k1 - 1) ∧
    (∀ ℓ : ℕ, 1 ≤ ℓ → k = (ℓ + 1) * (np + 1) →
      MetaMathlibExt.josephus k (np + 1) = np)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Proposition 4.

Uses 1

Statement usesJosephus survivor function

TheoremJosephus fixed points detected by the next value#●ready to prove

Let \(k \ge 2\) and \(n_p\) be natural numbers with \(n_p \ge k - 1\), and let \(J_k\) be the Josephus function. Then \(J_k(n_p) = n_p\) if and only if \(J_k(n_p + 1) = k - 1\).

theorem_wanted josephus_eq_self_iff (k np : ℕ) (hk : 2 ≤ k)
    (hnp : k - 1 ≤ np) :
    MetaMathlibExt.josephus k np = np ↔
      MetaMathlibExt.josephus k (np + 1) = k - 1

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Proposition 4.

Uses 1

Statement usesJosephus survivor function

TheoremLinear growth of the Josephus function before a wrap-around#●ready to prove

Let \(k \ge 2\), \(n \ge 1\) and \(m\) be natural numbers, let \(J_k\) be the Josephus function and write \(p = J_k(n)\). If \(p + km \le n + m\), then \(J_k(n + m) = p + km\).

theorem_wanted josephus_add_eq_of_le (k n m : ℕ) (hk : 2 ≤ k)
    (hn : 1 ≤ n)
    (h : MetaMathlibExt.josephus k n + k * m ≤ n + m) :
    MetaMathlibExt.josephus k (n + m) =
      MetaMathlibExt.josephus k n + k * m

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Lemma 6.

Uses 1

Statement usesJosephus survivor function

TheoremThe Josephus function at the first wrap-around#●ready to prove

Let \(k \ge 2\), \(n \ge 1\) and \(m\) be natural numbers and let \(J_k\) be the Josephus function. Suppose that \(m\) is the least natural number with \(J_k(n) + km > n + m\), and that moreover \(J_k(n) + km \le 2(n + m)\). Then \(J_k(n + m) = J_k(n) + km - (n + m)\).

The second hypothesis, which allows only one wrap-around, is not in the printed lemma; without it the statement fails at \(k = 4\), \(n = 1\), \(m = 1\).

theorem_wanted josephus_add_eq_sub_of_minimal (k n m : ℕ)
    (hk : 2 ≤ k) (hn : 1 ≤ n)
    (hmin : (∀ m' : ℕ, m' < m →
        MetaMathlibExt.josephus k n + k * m' ≤ n + m') ∧
      n + m < MetaMathlibExt.josephus k n + k * m)
    (hwrap : MetaMathlibExt.josephus k n + k * m ≤ 2 * (n + m)) :
    MetaMathlibExt.josephus k (n + m) =
      MetaMathlibExt.josephus k n + k * m - (n + m)

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Lemma 6.

Uses 1

Statement usesJosephus survivor function

TheoremExtremal points of the Josephus function near \(2k - 2\)#●ready to prove

Let \(k \ge 2\) be a natural number and let \(J_k\) be the Josephus function; call \(m\) low extremal if \(1 \le J_k(m) \le k - 1\), and high extremal if \(m + 1\) is low extremal. If \(J_k(2k - 2) \le k - 1\), then \(2k - 3\) is high extremal and \(2k - 2\) is low extremal. If \(J_k(2k - 2) > k - 1\), then \(2k - 2\) is high extremal and \(2k - 1\) is low extremal. In particular, \(2k - 2\) is always a low or a high extremal point.

theorem_wanted extremal_two_mul_sub (k : ℕ) (hk : 2 ≤ k) :
    (MetaMathlibExt.josephus k (2 * k - 2) ≤ k - 1 →
      IsHighExtremal k (2 * k - 3) ∧
        IsLowExtremal k (2 * k - 2)) ∧
    (k - 1 < MetaMathlibExt.josephus k (2 * k - 2) →
      IsHighExtremal k (2 * k - 2) ∧
        IsLowExtremal k (2 * k - 1))

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Corollary 7.

Uses 3

Statement usesHigh extremal point of the Josephus function · Low extremal point of the Josephus function · Josephus survivor function

TheoremLinear-step bound at a low extremal point#●ready to prove

Let \(k \ge 2\) and \(n\) be natural numbers, let \(J_k\) be the Josephus function, write \(j = J_k(n+1)\), and suppose \(j \le k - 1\). Then for every natural number \(m\), \(j + km \le n + 1 + m\) holds if and only if \(m \le \lfloor (n - (j - 1)) / (k - 1) \rfloor\). Moreover, if \(k - 2 + j \le n\), then \(\lfloor (n - (j - 1)) / (k - 1) \rfloor \ge 1\).

Since \(1 \le J_k(n+1) \le n + 1\), the hypothesis says \(j \in [1, k - 1]\), that is, \(n + 1\) is a low extremal point in the paper's sense, and none of the subtractions above is truncated.

theorem_wanted shift_le_iff_le_div (k n : ℕ) (hk : 2 ≤ k)
    (hj : MetaMathlibExt.josephus k (n + 1) ≤ k - 1) :
    (∀ m : ℕ, MetaMathlibExt.josephus k (n + 1) + k * m ≤ n + 1 + m ↔
      m ≤ (n - (MetaMathlibExt.josephus k (n + 1) - 1)) / (k - 1)) ∧
    (k - 2 + MetaMathlibExt.josephus k (n + 1) ≤ n →
      1 ≤ (n - (MetaMathlibExt.josephus k (n + 1) - 1)) / (k - 1))

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Lemma 8.

Uses 1

Statement usesJosephus survivor function

TheoremLinear growth of the Josephus function after a high extremal point#●ready to prove

Let \(k \ge 2\) and \(n_e \ge 2k - 3\) be natural numbers such that \(n_e\) is a high extremal point of the Josephus function \(J_k\), that is, \(1 \le J_k(n_e + 1) \le k - 1\), and write \(j = J_k(n_e + 1)\). Then \(J_k(n_e + 1 + m) = j + km\) for every natural number \(m \le \lfloor (n_e - (j - 1)) / (k - 1) \rfloor\).

theorem_wanted josephus_add_eq_of_high (k ne m : ℕ)
    (hk : 2 ≤ k) (hne : 2 * k - 3 ≤ ne)
    (hhigh : IsHighExtremal k ne)
    (hm : m ≤ (ne - (MetaMathlibExt.josephus k (ne + 1) - 1)) / (k - 1)) :
    MetaMathlibExt.josephus k (ne + 1 + m) =
      MetaMathlibExt.josephus k (ne + 1) + k * m

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Theorem 9.

Uses 2

Statement usesHigh extremal point of the Josephus function · Josephus survivor function

TheoremThe Josephus function has infinitely many fixed points#●ready to prove

For every natural number \(k \ge 2\), the set of natural numbers \(n\) with \(J_k(n) = n\) is infinite, where \(J_k\) is the Josephus function.

theorem_wanted infinite_fixedPoints (k : ℕ) (hk : 2 ≤ k) :
    {n : ℕ | MetaMathlibExt.josephus k n = n}.Infinite

Sources

• Yunier Bello-Cruz and Roy Quintero-Contreras, "Analytical Study and Efficient Evaluation of the Josephus Function", Theorem 13.

Uses 1

Statement usesJosephus survivor function

22 fully proved17 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.