theorem
proved
rsAlphaFactor_gt_100
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 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26theorem rsAlphaFactor_pos : 0 < rsAlphaFactor := by
27 unfold rsAlphaFactor; positivity
28
29theorem rsAlphaFactor_gt_100 : rsAlphaFactor > 100 := by
30 unfold rsAlphaFactor
31 linarith [Real.pi_gt_three]
32
33/-- 44π is the gauge loop area denominator in the RS α⁻¹ formula. -/
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