spacetime_eq_4
plain-language theorem explainer
The spacetime dimension in the Recognition Science derivation of the Dirac equation is fixed at four. Physicists assembling the gamma-matrix algebra for the standard model would cite this equality when verifying the 3+1 signature. The proof is a direct reflexivity step that matches the explicit definition of spacetimeDimension.
Claim. The spacetime dimension equals four: $D + 1 = 4$.
background
In the DiracEquationFromRS module the spacetime dimension is introduced as the natural number 4, written explicitly as D+1 with D the number of spatial dimensions. The module constructs the Dirac equation by identifying the four gamma matrices γ^μ (μ = 0,1,2,3) with the 4 = 2^(D-1) directions required by the Recognition Science forcing chain. The upstream definition is spacetimeDimension : ℕ := 4.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of spacetimeDimension.
why it matters
This theorem supplies the spacetime_4 component of the DiracCert record that certifies the full set of gamma matrices and chirality. It realizes the T8 step of the forcing chain that sets D = 3 spatial dimensions and thereby fixes the five gamma matrices (four spacetime plus γ^5) needed for the RS-native Dirac equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.