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)
90structure T15Cert where
91 /-- The prediction is 2/W with W=17 wallpaper groups. -/
92 geometric_origin : alpha_s_pred = 2 / (wallpaper_groups : ℝ)
93 /-- The prediction matches experiment within uncertainty. -/
94 matches_pdg : abs (alpha_s_pred - alpha_s_exp) < alpha_s_err
95
96/-- The T15 certificate is verified. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
t15_verified
in IndisputableMonolith.Physics.StrongForce
decl_use
depends on (12)
Lean names referenced from this declaration's body.
-
wallpaper_groups
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
wallpaper_groups
in IndisputableMonolith.Constants.AlphaHigherOrder
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
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use
-
alpha_s_err
in IndisputableMonolith.Physics.StrongForce
decl_use
-
alpha_s_exp
in IndisputableMonolith.Physics.StrongForce
decl_use
-
alpha_s_pred
in IndisputableMonolith.Physics.StrongForce
decl_use