No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
341theorem mass_gap_from_phi : Jcost phi = massGap := Jcost_phi_eq_massGap
proof body
Term-mode proof.
342
343/-- **Mass gap numerical bounds**: 0.118 < Δ < 0.119. -/
depends on (7)
Lean names referenced from this declaration's body.
-
Mass
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
gap
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
Jcost_phi_eq_massGap
in IndisputableMonolith.Unification.YangMillsMassGap
decl_use
-
massGap
in IndisputableMonolith.Unification.YangMillsMassGap
decl_use