theorem
proved
lqgStructureCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.LoopQuantumGravityFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | spinNetwork | spinFoamLQG | kinematicHilbert | thiemannQuantization | coherentStates
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem lqgStructureCount : Fintype.card LQGStructure = 5 := by decide
29
30/-- 5 = D + 2 = 3 + 2. -/
31theorem lqg_five_Dp2 : Fintype.card LQGStructure = 3 + 2 := by decide
32
33structure LQGCert where
34 five_structures : Fintype.card LQGStructure = 5
35 five_Dp2 : Fintype.card LQGStructure = 3 + 2
36
37def lqgCert : LQGCert where
38 five_structures := lqgStructureCount
39 five_Dp2 := lqg_five_Dp2
40
41end IndisputableMonolith.Physics.LoopQuantumGravityFromRS