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)

  48def J_transition (x_star : ℝ) : ℝ := J x_star

Definition body.

  49
  50/-- Activation energy (dimensionless) = J(x*) - J(reactant). -/

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

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 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.