quantumFieldTypeCount
plain-language theorem explainer
quantumFieldTypeCount establishes that the finite set of quantum field types has cardinality exactly 5. Researchers deriving QFT operators from Recognition Science cite this count when assembling the operator algebra and verifying the combinatorial structure against configDim. The proof is a one-line decision procedure that enumerates the constructors of the inductive type.
Claim. The finite type of quantum field types has cardinality five: $|Q| = 5$ where $Q = $ {scalar, spinor, vector, tensor, spinor-tensor}.
background
The module derives quantum field operators from the Recognition Science framework by mapping creation and annihilation operators to J-cost operators on the recognition Hilbert space. Bosons obey $[a, a^†] = 1$ and fermions obey ${a, a^†} = 1$. Five canonical field types are introduced to match the configuration dimension, which upstream results define as $D + 2$ (spatial degrees plus temporal and ledger balance) and fix at 5 when $D = 3$ from the eight-tick octave.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance automatically derived for the inductive type QuantumFieldType with its five constructors.
why it matters
The result supplies the five_fields component of the QFOCert definition, which certifies the full quantum field operator structure. It directly implements the combinatorial claim that five field types equal configDim, closing the step that links the Recognition Composition Law to the operator algebra and the phi-ladder mass formulas. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.