structure
definition
FineStructureCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.FineStructureConstantFromRS on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
34theorem alpha_rung_factor : (alphaRung : ℝ) * Real.pi = rsAlphaFactor := by
35 unfold rsAlphaFactor; norm_cast
36
37structure FineStructureCert where
38 alpha_rung : alphaRung = 44
39 factor_pos : 0 < rsAlphaFactor
40 factor_gt_100 : rsAlphaFactor > 100
41
42noncomputable def fineStructureCert : FineStructureCert where
43 alpha_rung := alphaRung_eq
44 factor_pos := rsAlphaFactor_pos
45 factor_gt_100 := rsAlphaFactor_gt_100
46
47end IndisputableMonolith.Physics.FineStructureConstantFromRS