def definition def or abbrev

`quartic_coefficient_canonical`

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

formal statement (Lean)

 179def quartic_coefficient_canonical (Λ v : ℝ) : ℝ := Λ ^ 4 / (24 * v ^ 4)

proof body

Definition body.

 180
 181/-- Algebraic identity: the quartic Taylor potential equals the canonical
 182    quadratic-plus-quartic Lagrangian potential up to renaming. -/

used by (3)

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

HiggsEFTBridgeCert in IndisputableMonolith.StandardModel.HiggsEFTBridge decl_use
quartic_coupling_from_normalization in IndisputableMonolith.StandardModel.HiggsEFTBridge decl_use
V_RS_quartic_canonical in IndisputableMonolith.StandardModel.HiggsEFTBridge decl_use

depends on (5)

Lean names referenced from this declaration's body.

canonical in IndisputableMonolith.Foundation.ArithmeticOf decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
canonical in IndisputableMonolith.Gap45.Beat decl_use
canonical in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use