spacetime_plus_chiral
plain-language theorem explainer
Four-dimensional spacetime in the Recognition Science derivation requires five Dirac gamma matrices once the chirality matrix is adjoined. Researchers reconstructing the Dirac equation from the forcing chain or Recognition Composition Law cite this count relation to close the matrix algebra. The proof is a direct numerical check on the two constant definitions.
Claim. In four-dimensional spacetime the total number of Dirac gamma matrices, including the chirality matrix, satisfies $4 + 1 = 5$.
background
The module constructs the Dirac equation (iγ^μ ∂_μ - m)ψ = 0 inside Recognition Science by identifying gamma matrices with the 4 = 2^(D-1) directions required by the forcing chain. Spacetime dimension is fixed at 4, corresponding to three spatial dimensions plus time. Gamma matrix count is fixed at 5, comprising the four spacetime matrices γ⁰ through γ³ together with the chirality matrix γ⁵ = i γ⁰ γ¹ γ² γ³.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic equality of the two constant definitions.
why it matters
This supplies the chiral_from_4 field inside the DiracCert structure that certifies the full Dirac setup. It closes the count step that follows from T8 (D = 3 spatial dimensions) and the eight-tick octave, allowing the module to assert that 4 + 1 = 5 gamma matrices suffice for the four-dimensional case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.