spacetime_eq_2sq
plain-language theorem explainer
The spacetime dimension in the Recognition Science Dirac derivation equals four, matching the count of gamma matrices for 3+1 spacetime. Researchers mapping RS structures to the Dirac equation would cite this to fix the four-dimensional count before introducing chirality. The proof is a one-line decision procedure that reduces both sides to the numeral four using the upstream definition.
Claim. The spacetime dimension equals $2^{2}$.
background
The DiracEquationFromRS module constructs the Dirac equation (iγ^μ∂_μ - m)ψ = 0 from Recognition Science by identifying the four gamma matrices γ^0 to γ^3 with the 4 = 2^(D-1) directions when D = 3. It introduces spacetimeDimension as the natural number 4, which encodes three spatial dimensions plus time and supplies the base count for both spacetime matrices and the chirality matrix γ^5. The upstream definition spacetimeDimension : ℕ := 4 directly supplies the value that this theorem equates to 2^2.
proof idea
This is a one-line wrapper that applies the decide tactic to the equality spacetimeDimension = 2 ^ 2, which succeeds because the definition of spacetimeDimension reduces both sides to the numeral 4.
why it matters
The result fixes the four-dimensional spacetime required for the gamma-matrix construction in the RS Dirac derivation, aligning with T8 of the forcing chain that sets D = 3 spatial dimensions and with the module statement that 4 = 2^(D-1). It precedes sibling results such as gamma_count_eq_5 and spacetime_eq_4 that build the full set of five matrices. No open questions are closed here; the equality simply discharges the numerical identity needed for the subsequent DiracCert construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.