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)
248def summary : List String := [
proof body
Definition body.
249 "Higgs potential = J-cost functional",
250 "VEV = J-cost minimum",
251 "W, Z get mass, photon stays massless",
252 "Higgs boson discovered at 125 GeV",
253 "Hierarchy problem: v << M_Planck"
254]
255
256/-! ## Falsification Criteria -/
257
258/-- The derivation would be falsified if:
259 1. Higgs mechanism is wrong
260 2. VEV doesn't minimize J-cost
261 3. Additional Higgs bosons found (complicates story) -/
depends on (12)
Lean names referenced from this declaration's body.
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
W
in IndisputableMonolith.Masses.Anchor
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use
-
get
in IndisputableMonolith.RRF.Core.Vantage
decl_use