dirac_mass
plain-language theorem explainer
The Dirac mass at integer rung r is defined as φ^r ⋅ φ^{-5} on the recognition phi-ladder in RS-native units. Researchers assembling the fermion spectrum from the J-cost functional cite this when proving mass positivity and monotonicity. The declaration is a direct equational definition with no lemmas or tactics required.
Claim. For any integer $r$, the Dirac fermion mass at rung $r$ is $m_r = φ^r ⋅ φ^{-5}$.
background
The module derives the Dirac equation from the J-cost as a first-order recognition operator on the 4-component spinor encoding (J, σ, Z, Θ). Fermion masses are assigned via the phi-ladder with base scale φ^{-5} tied to the coherence threshold. The DiracEquationCert collects this mass definition together with spin-1/2 from D=3 and the positivity properties. Upstream forcing chains fix φ as the self-similar fixed point and establish D=3 spatial dimensions.
proof idea
This is a direct definition that unfolds to the product of two powers of phi. No lemmas are applied; the body is the equational expression phi ^ r * phi ^ (-5).
why it matters
The definition populates the DiracEquationCert structure that certifies the Dirac equation as a structural theorem with zero axioms. It supplies the mass spectrum component linking to the phi-ladder and eight-tick octave at D=3. Downstream theorems establish positivity and strict increase with rung, supporting fermion dynamics from J-cost. It touches the open question of matching the alpha band to observed masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.