DiracEquationCert
plain-language theorem explainer
The DiracEquationCert structure packages the three conditions needed for the Dirac equation to emerge from the J-cost: spatial dimension exactly 3, positivity of the rung mass for every integer, and strict increase of that mass with rung number. A physicist deriving fermion spectra in Recognition Science cites it to confirm that the phi-ladder supplies a valid first-order wave operator. The definition is a direct bundling of three prior lemmas with no further reduction steps.
Claim. A certificate for the Dirac equation consisting of the assertions $D=3$, $0 < m_r$ for every integer rung $r$, and $m_r < m_{r+1}$ for every integer rung $r$, where the rung mass is given by $m_r = phi^r phi^{-5}$.
background
In the Recognition Science framework the Dirac equation is obtained as the first-order recognition operator equation for spin-1/2 particles. The module derives it from the J-cost by matching the Clifford algebra to the recognition metric and by placing fermion masses on the phi-ladder. The auxiliary definition dirac_mass r supplies the explicit rung formula $m_r = phi^r phi^{-5}$ in RS-native units. The theorem spin_half_from_D3 records that D equals 3, which forces spin-1/2 via the covering group Spin(3) equal to SU(2). The two mass theorems establish that this formula is positive and strictly increasing for all integer rungs.
proof idea
The structure is defined by direct field assignment: its three components are set equal to the theorems spin_half_from_D3, dirac_mass_pos, and dirac_mass_increasing. No tactics or algebraic reductions occur inside the declaration itself.
why it matters
DiracEquationCert is the master structural object that closes the derivation of the Dirac equation from the J-cost. It is instantiated by the downstream definition diracEquationCert and used to prove the inhabitedness theorem diracEquationCert_inhabited. In the forcing chain it supplies the final link from T8 (D equals 3) and the phi-ladder mass formula to the existence of spin-1/2 fermions obeying the first-order wave equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.