theorem
proved
qftSectors_five
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumFieldTheoryDepthFromRS on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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