def definition def or abbrev

`J_bit_val`

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

formal statement (Lean)

  60noncomputable def J_bit_val : ℝ := J phi

Definition body.

  61
  62/-- Alternative expression: J_bit = cosh(ln φ) - 1. -/

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

extremum_condition in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
extremum_unique in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_bit_bounds in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_bit_eq_cosh in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_bit_eq_phi_minus in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_bit_explicit in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
J_bit_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_from_Jbit in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
PlanckScaleMatchingCert in IndisputableMonolith.Constants.PlanckScaleMatching decl_use