def definition def or abbrev

`jBit`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 215noncomputable def jBit : ℝ := Real.log phi

Definition body.

 216
 217/-- J_bit > 0 -/

From the project-wide theorem graph. These declarations reference this one in their body.

jBit_pos in IndisputableMonolith.Foundation.JCostGeometry decl_use
finite_capacity_veto in IndisputableMonolith.Foundation.TopologicalVeto decl_use
link_penalty_positive in IndisputableMonolith.Foundation.TopologicalVeto decl_use