gammaMatrixCount
plain-language theorem explainer
The definition fixes the total count of Dirac gamma matrices at 5, covering the four spacetime matrices together with the chirality matrix. Physicists reconstructing the Dirac equation inside the Recognition Science framework cite this count to confirm that the matrix algebra dimension equals configDim D. The assignment is a direct numerical constant with no reduction or lemma application required.
Claim. The total number of Dirac gamma matrices is defined to be $5$.
background
The DiracEquationFromRS module obtains the Dirac equation from Recognition Science by mapping gamma matrices to configuration-space directions. Four matrices correspond to spacetime, since $4=2^{D-1}$ with $D=3$ spatial dimensions from the forcing chain; the fifth is the chirality matrix defined by $i$ times the product of the first four. Their sum equals configDim $D=5$ as stated in the module documentation.
proof idea
The definition is a direct constant assignment of the natural number 5.
why it matters
This definition supplies the matrix count required by the DiracCert structure and the two theorems gamma_count_eq_5 and spacetime_plus_chiral. It anchors the chiral extension of the Dirac algebra to the Recognition Science landmarks T8 (D=3 spatial dimensions) and the eight-tick octave, closing the count that matches the framework's 4+1 matrix structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.