/-!
# waypoints.si: the locks

The Syracuse map and the statements a submission must prove, in plain Lean 4 (no Mathlib). A submission
imports this file and proves `theorem solution : Waypoints.Lock.<Name> := ...`. Lean checks it, and only the
three standard axioms (propext, Classical.choice, Quot.sound) are allowed.
-/

namespace Waypoints.Lock

/-- The 2-adic valuation: how many times 2 divides n (v2 0 = 0). -/
def v2 (n : Nat) : Nat :=
  if h : n ≠ 0 ∧ n % 2 = 0 then v2 (n / 2) + 1 else 0
termination_by n
decreasing_by omega

/-- The Syracuse map: S(n) = (3n + 1) / 2^(v2(3n + 1)). -/
def S (n : Nat) : Nat := (3 * n + 1) / 2 ^ v2 (3 * n + 1)

/-- S applied k times. -/
def iter : Nat → Nat → Nat
  | 0, n => n
  | k + 1, n => iter k (S n)

/-- Warm-up 1, descent: for n ≡ 1 (mod 4) and n > 1, one step of S goes down. -/
def Descent : Prop := ∀ n : Nat, n % 4 = 1 → 1 < n → S n < n

/-- Warm-up 2: the only positive fixed point of S is 1. -/
def NoFixedPoints : Prop := ∀ n : Nat, 0 < n → S n = n → n = 1

/-- Warm-up 3: no positive integer other than 1 returns to itself after two steps of S. -/
def NoTwoCycles : Prop := ∀ n : Nat, 0 < n → S (S n) = n → n = 1

/-- The door, open since 1937: the only positive periodic point of S is 1 (no non-trivial cycles). -/
def NoCycles : Prop := ∀ n L : Nat, 0 < n → 0 < L → iter L n = n → n = 1

end Waypoints.Lock