def
definition
stringTheoryCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.StringTheoryFromJCost on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
33 five_variants : Fintype.card StringTheoryVariant = 5
34 vacuum_zero : J 1 = 0
35
36noncomputable def stringTheoryCert : StringTheoryCert where
37 five_variants := stringTheoryCount
38 vacuum_zero := vacuum_jcost_zero
39
40end IndisputableMonolith.Physics.StringTheoryFromJCost