statistics_times_fields
plain-language theorem explainer
The theorem asserts that the product of the statistics count and the cardinality of the quantum field types set equals 10. A physicist reconstructing QFT structures inside Recognition Science would cite this identity to fix the total number of operator classes at 10. The proof reduces to a single application of the decide tactic that evaluates the product on the explicit natural number definitions.
Claim. Let $S=2$ be the number of statistics types (boson or fermion) and let $F$ be the finite set of five quantum field types consisting of scalar, spinor, vector, tensor, and spinor-tensor. Then $S$ times the cardinality of $F$ equals 10.
background
The module on Quantum Field Operators from RS maps QFT creation and annihilation operators to J-cost operators on the recognition Hilbert space, distinguishing bosons by commutation relations and fermions by anticommutation relations. The inductive type QuantumFieldType enumerates exactly five cases: scalar, spinor, vector, tensor, and spinorTensor, matching configDim D = 5. The upstream definition statisticsCount is fixed at the constant 2, with its documentation stating that 2 statistics times 5 field types equals 10, equivalently 2 times configDim D.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic unfolds statisticsCount to the literal 2 and uses the automatically derived Fintype instance on the inductive QuantumFieldType to obtain cardinality 5, then confirms the arithmetic product equals 10.
why it matters
This theorem supplies the ten_total field inside the qfoCert certificate that certifies the overall quantum field operator construction. It completes the basic combinatorial step in the module that links the two statistics to the five field types, producing the total of 10 in agreement with the Recognition Science configuration dimension. The count aligns with the forcing chain landmarks where D = 3 spatial dimensions and the five-dimensional field configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.