diracEquationCert
plain-language theorem explainer
diracEquationCert assembles the master certificate for the Dirac equation in the recognition framework by confirming D equals 3 together with positivity and strict increase of the fermion mass on the phi-ladder. A physicist deriving spin-1/2 fermion dynamics from J-cost would cite this certificate to anchor the first-order wave equation. The construction is a direct record definition that populates the three required fields from the corresponding prior theorems.
Claim. The Dirac equation certificate asserts that the spatial dimension satisfies $D=3$, that the Dirac mass $m_r = phi^r phi^{-5}$ is positive for every integer rung $r$, and that $m_r < m_{r+1}$ holds for all $r in Z$.
background
The module derives the Dirac equation as the first-order recognition operator for spin-1/2 particles, with the spinor encoding the four-component state on the recognition Hilbert space and the gamma matrices satisfying the Clifford algebra from the recognition metric. DiracEquationCert is the structure whose three fields are spin_half_from_D3 : D=3, dirac_mass_pos : forall r : Z, 0 < dirac_mass r, and dirac_mass_increasing : forall r : Z, dirac_mass r < dirac_mass (r+1). The upstream theorems establish D=3 by reflexivity, positivity of the mass via multiplication of positive powers of phi, and monotonicity via the zpow_add identity and positivity of phi.
proof idea
The definition is a one-line record constructor that directly supplies the three fields of DiracEquationCert by referencing the theorems spin_half_from_D3, dirac_mass_pos, and dirac_mass_increasing.
why it matters
This definition supplies the master certificate DiracEquationCert that is used to prove the inhabitedness of the structure, confirming consistency of the Dirac equation derivation. It completes the structural theorem for fermion dynamics by linking the D=3 result from the forcing chain to the phi-ladder mass spectrum. The certificate anchors the Clifford algebra and gamma matrices in the recognition metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.