def
definition
def or abbrev
k_rec_com
show as:
view Lean formalization →
formal statement (Lean)
103def k_rec_com : ℝ := 1.4e6
proof body
Definition body.
104
105/-- The curvature bound at the recognition event R0:
106 |R| ≤ 1/λ_rec² = 1 (in RS-native units). -/