def definition def or abbrev

`J_transition`

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

formal statement (Lean)

 126noncomputable def J_transition (x y : ℝ) (_ : 0 < x) (_ : 0 < y) : ℝ :=

Definition body.

 127  |Real.log (y / x)| * ((J x + J y) / 2)
 128
 129/-- Transition to self has zero cost. -/

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

J_transition in IndisputableMonolith.Chemistry.ActivationEnergy decl_use
determined_necessary_for_minimal in IndisputableMonolith.Modal.Actualization decl_use
PathAction in IndisputableMonolith.Modal.Actualization decl_use
modal_distance in IndisputableMonolith.Modal.ModalGeometry decl_use
modal_distance_nonneg in IndisputableMonolith.Modal.ModalGeometry decl_use
modal_geometry_status in IndisputableMonolith.Modal.ModalGeometry decl_use
identity_always_possible in IndisputableMonolith.Modal.Possibility decl_use
identity_prefers_stasis in IndisputableMonolith.Modal.Possibility decl_use
J_change in IndisputableMonolith.Modal.Possibility decl_use
J_pos_of_ne_one in IndisputableMonolith.Modal.Possibility decl_use
J_stasis_nonneg in IndisputableMonolith.Modal.Possibility decl_use
J_transition_self in IndisputableMonolith.Modal.Possibility decl_use
J_transition_symm in IndisputableMonolith.Modal.Possibility decl_use
Possibility in IndisputableMonolith.Modal.Possibility decl_use

Lean names referenced from this declaration's body.