statisticsCount
plain-language theorem explainer
statisticsCount defines the number of statistics in the RS-derived QFT model as the natural number 2, standing for the boson and fermion cases. A researcher counting total quantum field configurations from the recognition Hilbert space would cite this constant when verifying the product with the five field types. The declaration is a direct constant assignment with no lemmas or reduction steps.
Claim. Define the statistics count by the equation $s := 2$.
background
The module Quantum Field Operators from RS starts from the recognition Hilbert space whose J-cost operators realize creation and annihilation. It distinguishes two statistics (bosons with commutator $[a,a^†]=1$, fermions with anticommutator ${a,a^†}=1$) and five canonical field types (scalar, spinor, vector, tensor, spinor-tensor) whose count equals configDim D. The supplied definition supplies the factor 2 that multiplies the field-type cardinality to produce the total of ten configurations.
proof idea
This is a direct definition that assigns the constant 2 to statisticsCount; no lemmas are applied and no tactics are executed.
why it matters
The definition supplies the left-hand factor in the ten_total field of the QFOCert structure and in the theorem statistics_times_fields that proves the product equals 10. It therefore anchors the combinatorial layer of the RS QFT construction that links the two statistics to the five field types arising from configDim D. No open scaffolding questions are closed by this constant itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.