DiracCert
plain-language theorem explainer
DiracCert bundles the three equalities that fix spacetime dimension to 4 and the gamma matrix count to 5 in the Recognition Science derivation of the Dirac equation. Physicists tracing the Dirac operator back to the forcing chain and phi-ladder would cite this record to lock the dimension and matrix algebra. The declaration is a bare structure whose fields are direct equalities drawn from the upstream constants spacetimeDimension and gammaMatrixCount.
Claim. The structure DiracCert consists of the three assertions that spacetime dimension equals 4, the cardinality of the finite type of gamma matrices equals 5, and spacetime dimension plus one equals the gamma matrix count.
background
In the module deriving the Dirac equation from Recognition Science, spacetimeDimension is defined as 4 (corresponding to 3+1 dimensions) and gammaMatrixCount is defined as 5. GammaMatrix is the inductive type whose constructors are gamma0, gamma1, gamma2, gamma3 and gamma5. The module documentation states that the four spacetime matrices together with the chirality matrix gamma5 total five, matching the configuration dimension in the RS setup.
proof idea
This is a structure definition with no proof body. It directly declares the three fields as equalities between the upstream constants spacetimeDimension, gammaMatrixCount and the Fintype cardinality of GammaMatrix.
why it matters
DiracCert supplies the dimension and matrix count certificate instantiated by diracCert. It closes the link from the RS forcing chain (T8 fixing D=3 spatial dimensions) to the standard Dirac algebra in 4D spacetime with five gamma matrices. This supports emergence of the Dirac equation from the Recognition Composition Law without extra assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.