`LQGStructure`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.LoopQuantumGravityFromRS
domain: Physics
line: 24 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.LoopQuantumGravityFromRS on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  21
  22namespace IndisputableMonolith.Physics.LoopQuantumGravityFromRS
  23
  24inductive LQGStructure where
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.