QFOCert
plain-language theorem explainer
The QFOCert structure records that the set of quantum field types has cardinality five and that twice this number equals ten when multiplied by the statistics factor. Physicists constructing QFT operators from Recognition Science would cite it to fix the combinatorial basis for the five field sectors and boson-fermion distinction. The declaration is realized as a plain structure definition that directly encodes the two cardinality equations supplied by the inductive type and the constant statisticsCount.
Claim. Let $F$ be the set of quantum field types consisting of scalar, spinor, vector, tensor, and spinor-tensor. Then $|F|=5$ and $2 times |F|=10$.
background
The module interprets creation and annihilation operators as J-cost operators on the recognition Hilbert space, with bosons satisfying $[a,a^dagger]=1$ and fermions satisfying ${a,a^dagger}=1$. QuantumFieldType is the inductive type whose five constructors are scalar, spinor, vector, tensor, and spinorTensor; its Fintype.card therefore equals five, matching the module's statement that this equals configDim D. statisticsCount is the constant 2 that supplies the boson-fermion distinction, so that the product yields the total of ten operator classes.
proof idea
This is a structure definition that packages the two cardinality equations: Fintype.card of the five-constructor inductive type equals 5, and statisticsCount times that cardinality equals 10. No lemmas or tactics are invoked; the fields simply restate the facts already present in the referenced inductive definition and the constant definition.
why it matters
QFOCert supplies the certificate consumed by the downstream qfoCert definition, which instantiates the structure to confirm the full operator combinatorics. It anchors the five-field-type count that the module presents as primary, consistent with the Recognition Science view that these types arise from J-cost operators on the recognition Hilbert space. The declaration does not yet reach the explicit commutation relations or any link to the phi-ladder or spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.