def
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 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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