dirac_mass_increasing
plain-language theorem explainer
The theorem establishes that Dirac fermion masses increase strictly with each successive integer rung r. Researchers constructing the recognition-derived fermion spectrum would cite it to confirm the mass hierarchy on the phi-ladder. The proof is a direct term reduction that unfolds the mass definition and applies ordering lemmas for positive powers of phi.
Claim. For every integer rung $r$, the Dirac mass satisfies $m_r < m_{r+1}$, where $m_r = phi^r · phi^{-5}$.
background
The module derives the Dirac equation from the J-cost functional equation as a first-order recognition operator for spin-1/2 particles. The Dirac mass at rung r is defined by the upstream result dirac_mass as $phi^r · phi^{-5}$, which encodes the recognition mass formula with base scale $phi^{-5}$ in native units. The local setting supplies the structural certification DiracEquationCert whose fields include positivity and monotonicity of this mass function.
proof idea
The term proof unfolds dirac_mass, rewrites the exponent via zpow_add₀ and zpow_one, then closes with two applications of mul_lt_mul_of_pos_right using phi_gt_one and zpow_pos phi_pos.
why it matters
This supplies the monotonicity field required by the DiracEquationCert structure that certifies the full derivation of the Dirac equation from J-cost. It anchors the increasing mass spectrum on the phi-ladder, consistent with the recognition framework's T5 J-uniqueness and phi fixed-point construction. The module as a whole is a zero-sorry structural theorem linking the mass property to the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.