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)
236noncomputable def higgsGaugeCoupling (m_V v : ℝ) : ℝ := 2 * m_V^2 / v
proof body
Definition body.
237
238/-! ## Summary -/
239
240/-- RS derivation of electroweak breaking:
241
242 1. **Higgs potential = J-cost**: Same mathematical form
243 2. **VEV = J-cost minimum**: Symmetry breaks spontaneously
244 3. **W, Z masses**: From coupling to VEV
245 4. **Photon massless**: U(1)_EM unbroken
246 5. **Higgs boson**: Radial excitation of Higgs field
247 6. **Hierarchy**: May be φ-related (under investigation) -/
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
W
in IndisputableMonolith.Masses.Anchor
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use