def definition def or abbrev

`coshEnhancement`

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

formal statement (Lean)

  59def coshEnhancement (t : ℝ) : ℝ :=

Definition body.

  60  if t = 0 then 1 else 2 * (Real.cosh t - 1) / t ^ 2
  61
  62/-- The perturbative (quadratic) cost: t²/2. -/

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

coupling_identity in IndisputableMonolith.Unification.CouplingLaw decl_use
CouplingLawCert in IndisputableMonolith.Unification.CouplingLaw decl_use
coupling_law_determines_strength in IndisputableMonolith.Unification.CouplingLaw decl_use
enhancement_at_zero in IndisputableMonolith.Unification.CouplingLaw decl_use
enhancement_ge_one in IndisputableMonolith.Unification.CouplingLaw decl_use
enhancement_gt_one in IndisputableMonolith.Unification.CouplingLaw decl_use
enhancement_near_one in IndisputableMonolith.Unification.CouplingLaw decl_use
enhancement_symmetric in IndisputableMonolith.Unification.CouplingLaw decl_use
enhancement_unbounded in IndisputableMonolith.Unification.CouplingLaw decl_use
exactCost_eq in IndisputableMonolith.Unification.CouplingLaw decl_use
recognitionStrength in IndisputableMonolith.Unification.CouplingLaw decl_use
structural_dominance in IndisputableMonolith.Unification.CouplingLaw decl_use

Lean names referenced from this declaration's body.