spacetimeDimension
plain-language theorem explainer
Recognition Science sets the spacetime dimension to 4 to match the four gamma matrices in the Dirac equation for 3+1 Minkowski space. Physicists deriving the Dirac equation inside the RS framework cite this constant as the base for gamma-matrix constructions. The definition is a direct numerical assignment with no computation or lemmas required.
Claim. In the Recognition Science derivation of the Dirac equation, the spacetime dimension is defined to be $4$.
background
The module realizes the Dirac equation $(iγ^μ ∂_μ - m)ψ = 0$ from Recognition Science. It introduces spacetimeDimension as the count of spacetime directions μ = 0,1,2,3, set equal to 4, which equals $2^{D-1}$ for the three spatial dimensions forced by T8. The module also counts five gamma matrices total: the four spacetime matrices plus the chirality matrix γ⁵ = iγ⁰γ¹γ²γ³, giving configDim D = 5.
proof idea
The definition is a direct assignment of the natural number 4. No lemmas or tactics are invoked; it functions as the base constant for the module's subsequent theorems.
why it matters
This definition supplies the spacetime dimension required by the DiracCert structure, which records spacetime_4 : spacetimeDimension = 4 together with gamma5_total and chiral_from_4. It anchors the RS derivation of the Dirac equation and is used directly by spacetime_eq_4, spacetime_eq_2sq, and spacetime_plus_chiral. The value is consistent with T8 forcing three spatial dimensions and therefore four spacetime dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.