def
definition
def or abbrev
J_bit
show as:
view Lean formalization →
formal statement (Lean)
249noncomputable def J_bit : ℝ := Real.log phi
proof body
Definition body.
250
251/-- Coherence energy in RS units (dimensionless).
252 By Phase 2 derivation, E_coh = C_lock = φ⁻⁵. -/