structure
definition
WeakForceCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.WeakNuclearForceFromRS on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
38theorem phi10_gt_100 : phi ^ 10 > 100 := by
39 rw [phi10_fibonacci]; linarith [phi_gt_onePointSixOne]
40
41structure WeakForceCert where
42 five_types : Fintype.card WeakDecayType = 5
43 phi10_val : phi ^ 10 = 55 * phi + 34
44 phi10_bound : phi ^ 10 > 100
45
46noncomputable def weakForceCert : WeakForceCert where
47 five_types := weakDecayCount
48 phi10_val := phi10_fibonacci
49 phi10_bound := phi10_gt_100
50
51end IndisputableMonolith.Physics.WeakNuclearForceFromRS