QuantumFieldType
plain-language theorem explainer
An inductive enumeration defines the five canonical quantum field types recognized in the RS derivation of QFT. A researcher counting degrees of freedom for operators on the recognition Hilbert space would cite this list when fixing the configuration dimension at five. The definition proceeds by direct listing of the five cases and automatic derivation of decidability and finiteness instances.
Claim. The quantum field types form the finite set consisting of the scalar field, the spinor field, the vector field, the tensor field, and the spinor-tensor field.
background
The module sets up creation and annihilation operators that act as J-cost operators on the recognition Hilbert space. Bosons obey the commutation relation [a, a†] = 1 and fermions obey the anticommutation relation {a, a†} = 1. Five canonical field types are introduced to realize configDim D = 5, which supplies the primary combinatorial factor in the count 2 statistics × 5 field types = 10.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives the instances DecidableEq, Repr, BEq, and Fintype automatically.
why it matters
This enumeration is required by the certification structure QFOCert, which records that the cardinality equals 5 and that the product with statisticsCount equals 10. It supplies the concrete content for the theorems quantumFieldTypeCount and statistics_times_fields, both proved by decision. The construction realizes the five-type count that the module identifies as primary for RS-derived QFT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.