GammaMatrix
plain-language theorem explainer
The GammaMatrix inductive type enumerates the five Dirac matrices required for the Recognition Science derivation of the Dirac equation in four-dimensional spacetime. Researchers deriving the standard model from the RS forcing chain would reference this enumeration when certifying the gamma matrix algebra. The definition proceeds by listing the four spacetime matrices together with the chirality matrix and automatically derives decidable equality and finite type structure.
Claim. The Dirac matrices consist of the five elements $gamma^0, gamma^1, gamma^2, gamma^3, gamma^5$, where the first four correspond to the spacetime directions in dimension 4 and $gamma^5$ is the chirality operator.
background
In the Recognition Science framework the Dirac equation arises from the composition law applied to the forcing chain. The module establishes that spacetime has dimension 4, so there are $2^{D-1}=4$ gamma matrices for the spacetime directions, plus the chirality matrix gamma5, for a total of five. This matches configDim D =5. The inductive type GammaMatrix provides the finite set of these matrices, from which Fintype.card is computed as 5.
proof idea
The declaration is an inductive definition that introduces five distinct constructors corresponding to the gamma matrices and derives the Fintype instance by enumeration.
why it matters
This definition supplies the carrier type for the DiracCert structure, which records the spacetime dimension equality and the cardinality of the gamma matrices. It closes the enumeration step in the RS derivation of the Dirac equation, confirming that the five matrices align with the four-dimensional spacetime plus chirality required by the eight-tick octave and D=3 spatial dimensions in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.