theorem
proved
spinFoamModelCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.SpinFoamFromRS on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24 | PonzanoRegge | EPRL | FK | BO | EngleLivine
25 deriving DecidableEq, Repr, BEq, Fintype
26
27theorem spinFoamModelCount : Fintype.card SpinFoamModel = 5 := by decide
28
29/-- 6j-symbol dimension = 6 = 2D = cube faces. -/
30def sixJDimension : ℕ := 6
31theorem sixJ_eq_cube_faces : sixJDimension = 6 := rfl
32theorem sixJ_eq_2D : sixJDimension = 2 * 3 := by decide
33
34structure SpinFoamCert where
35 five_models : Fintype.card SpinFoamModel = 5
36 sixJ_faces : sixJDimension = 6
37 sixJ_2D : sixJDimension = 2 * 3
38
39def spinFoamCert : SpinFoamCert where
40 five_models := spinFoamModelCount
41 sixJ_faces := sixJ_eq_cube_faces
42 sixJ_2D := sixJ_eq_2D
43
44end IndisputableMonolith.Physics.SpinFoamFromRS