dirac_mass_pos
plain-language theorem explainer
Recognition Science assigns fermion masses on the phi-ladder as m(r) = phi^r * phi^{-5}. The theorem establishes that these masses remain strictly positive for every integer rung r. This positivity is required so that the mass term in the derived Dirac equation describes physical particles rather than tachyons. The proof is a one-line term application of mul_pos to the two zpow_pos factors.
Claim. For every integer $r$, the Dirac mass $m(r) = phi^r * phi^{-5} > 0$.
background
The module derives the Dirac equation from the J-cost functional for spin-1/2 particles. The mass is defined by dirac_mass r := phi^r * phi^{-5}, which supplies the coefficient in the recognition operator equation. Upstream, rung maps particles to integers (electron at 2, muon at 13) and Mass is the real-number type. Phi positivity follows from its definition as the self-similar fixed point greater than 1.
proof idea
Term proof that directly invokes mul_pos on zpow_pos phi_pos r and zpow_pos phi_pos (-5). No intermediate lemmas or tactics are required beyond the built-in positivity of powers of a positive base.
why it matters
The result populates the dirac_mass_pos field inside DiracEquationCert, the master certificate that also records spin_half_from_D3 and dirac_mass_increasing. It thereby completes the structural verification that the recognition-derived Dirac equation yields physical, positive, and rung-ordered fermion masses. The construction aligns with the phi fixed point and the mass formula on the recognition ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.