gammaMatrixFintype
plain-language theorem explainer
The result asserts that the finite type enumerating the Dirac gamma matrices in the RS derivation has cardinality five. Researchers deriving the Dirac equation from Recognition Science principles would cite this when confirming the basis size matches the expected five matrices including the chirality operator. A single decision tactic suffices because the inductive definition carries an automatic Fintype instance.
Claim. The set of Dirac matrices consisting of the four spacetime matrices together with the chirality matrix has cardinality five.
background
In the module deriving the Dirac equation from Recognition Science, GammaMatrix is defined as an inductive type with five constructors: gamma0, gamma1, gamma2, gamma3, and gamma5. The module documentation states that these five matrices correspond to configDim D, with four arising from 2^(D-1) spacetime directions and the fifth from the chirality operator gamma5 = i gamma0 gamma1 gamma2 gamma3. The upstream result is precisely this inductive definition, which derives the Fintype instance used here.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This succeeds directly from the Fintype instance derived automatically for the inductive type with its five constructors.
why it matters
This cardinality result is used in the definition of diracCert, which packages spacetime_eq_4, gammaMatrixFintype, and spacetime_plus_chiral into a DiracCert structure. It fills the step confirming that the total number of gamma matrices is five, matching the framework requirement for configDim D = 5 in the Dirac equation derivation from RS. It supports the module claim of zero sorrys and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.