def
definition
superstringCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.SuperstringTheoryFromRS on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
39 flip_variant_match : extraDimensions = 2 ^ rsDimension - 1
40 seven_flip : (7 : ℕ) = 2 ^ 3 - 1
41
42def superstringCert : SuperstringCert where
43 extra_dim := extra_dim_eq_7
44 flip_variant_match := extra_dim_eq_flip_variants
45 seven_flip := seven_eq_flip_count
46
47end IndisputableMonolith.Physics.SuperstringTheoryFromRS