theorem
proved
qftTechniqueCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumFieldTheoryDepthFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | feynmanDiagrams | latticeQFT
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem qftTechniqueCount : Fintype.card QFTTechnique = 5 := by decide
29
30/-- QFT vacuum: 5 distinct sectors from the RS DFT-8 structure. -/
31def qftSectors : ℕ := 5
32theorem qftSectors_five : qftSectors = 5 := rfl
33
34structure QFTDepthCert where
35 five_techniques : Fintype.card QFTTechnique = 5
36 five_sectors : qftSectors = 5
37
38def qftDepthCert : QFTDepthCert where
39 five_techniques := qftTechniqueCount
40 five_sectors := qftSectors_five
41
42end IndisputableMonolith.Physics.QuantumFieldTheoryDepthFromRS