diracCert
plain-language theorem explainer
diracCert assembles the four-dimensional spacetime and five gamma matrices into a single certificate for the Recognition Science derivation of the Dirac equation. A physicist mapping the J-cost functional equation onto the Standard Model would cite this to fix the Clifford algebra dimension. The definition is a direct structure constructor that assigns each field from an upstream equality.
Claim. The Dirac certificate is the structure witnessing spacetimeDimension = 4, Fintype.card GammaMatrix = 5, and spacetimeDimension + 1 = gammaMatrixCount.
background
In the Recognition Science setting the Dirac equation (i gamma^mu partial_mu - m) psi = 0 is obtained once the configuration dimension reaches five. The structure DiracCert records three facts required for the four-dimensional Clifford algebra: spacetime has dimension exactly four, the set GammaMatrix has cardinality five, and adjoining the chirality matrix increases the count by one. These facts rest on the relation 4 = 2^(D-1) with D = 4 together with the eight-tick octave that forces spatial dimension three.
proof idea
The definition constructs an instance of DiracCert by direct field assignment. The spacetime_4 field receives the reflexivity proof from spacetime_eq_4, the gamma5_total field receives the decision proof from gammaMatrixFintype, and the chiral_from_4 field receives the decision proof from spacetime_plus_chiral.
why it matters
This definition supplies the concrete matrix configuration that embeds the Dirac operator inside the Recognition Science forcing chain after T8 has fixed spatial dimension three. It closes the step from the eight-tick period to the four-dimensional spacetime plus chirality matrix required by the Clifford algebra. No downstream theorems yet consume the certificate, leaving open the explicit construction of Dirac spinor solutions from the J-uniqueness relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.