theorem
proved
stringTheoryCount
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 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24 | typeI | typeIIA | typeIIB | so32Heterotic | e8e8Heterotic
25 deriving DecidableEq, Repr, BEq, Fintype
26
27theorem stringTheoryCount : Fintype.card StringTheoryVariant = 5 := by decide
28
29/-- Recognition vacuum selects J = 0. -/
30theorem vacuum_jcost_zero : J 1 = 0 := J_one
31
32structure StringTheoryCert where
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