diracEquationCert_inhabited
plain-language theorem explainer
The theorem establishes non-emptiness of the DiracEquationCert structure, confirming that the bundled properties for spin-1/2 fermions derived from J-cost are simultaneously realizable. Researchers extracting the Dirac equation as a first-order recognition operator would cite it to close the existence step in the fermion dynamics derivation. The proof is a direct term-mode construction that packages the pre-established spin and mass lemmas into the certificate.
Claim. The structure certifying the Dirac equation from J-cost is inhabited: there exists $C$ such that $C$ asserts $D=3$ (hence spin-1/2), the Dirac mass function satisfies $0 < m(r)$ for all integer rungs $r$, and $m(r) < m(r+1)$.
background
The module derives the Dirac equation $(iγ^μ∂_μ - m)ψ = 0$ as the recognition operator equation for spin-1/2 particles on the J-cost Hilbert space. The certificate structure DiracEquationCert bundles three fields: spin_half_from_D3 : D = 3, dirac_mass_pos : ∀ r : ℤ, 0 < dirac_mass r, and dirac_mass_increasing : ∀ r : ℤ, dirac_mass r < dirac_mass (r + 1). These encode the D=3 origin of SU(2) spin and the phi-ladder mass spectrum. The upstream definition diracEquationCert assembles the three lemmas into a single record.
proof idea
The proof is a one-line term-mode wrapper that applies the definition diracEquationCert to inhabit Nonempty DiracEquationCert.
why it matters
This declaration closes the existence proof for DiracEquationCert inside the module that extracts the Dirac equation from J-cost. It supports the structural theorem status listed in the module header and links directly to the Recognition Science landmarks T8 (D=3) and the phi-ladder mass formula. No downstream uses are recorded, so the result functions as an internal consistency check rather than a lemma for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.