theorem
proved
quantumFieldTypeCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26 | scalar | spinor | vector | tensor | spinorTensor
27 deriving DecidableEq, Repr, BEq, Fintype
28
29theorem quantumFieldTypeCount : Fintype.card QuantumFieldType = 5 := by decide
30
31/-- 2 statistics × 5 field types = 10 = 2 × configDim D. -/
32def statisticsCount : ℕ := 2
33theorem statistics_times_fields : statisticsCount * Fintype.card QuantumFieldType = 10 := by decide
34
35structure QFOCert where
36 five_fields : Fintype.card QuantumFieldType = 5
37 ten_total : statisticsCount * Fintype.card QuantumFieldType = 10
38
39def qfoCert : QFOCert where
40 five_fields := quantumFieldTypeCount
41 ten_total := statistics_times_fields
42
43end IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS