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)
39theorem vev_implies_scale (h : vev_from_ledger) : scale_from_ledger :=
proof body
Term-mode proof.
40 h
41
42/-- The VEV structural scale is pinned to the same phi interval. -/
depends on (8)
Lean names referenced from this declaration's body.
-
vev_from_ledger
in IndisputableMonolith.Constants.ElectroweakVEVStructure
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
scale_from_ledger
in IndisputableMonolith.QFT.ElectroweakScaleStructure
decl_use
-
interval
in IndisputableMonolith.Unification.SpacetimeEmergence
decl_use