m_e_pos
plain-language theorem explainer
Physicists deriving particle masses on the Recognition Science phi-ladder cite this result to confirm that the electron mass remains strictly positive. The claim states that m_e equals the coherence energy times phi to the power 2 is positive. The proof is a term-mode reduction that unfolds the mass definition, applies the mul_pos lemma to the product, rewrites the negative exponent in E_coh, and closes with div_pos and pow_pos.
Claim. The electron mass in RS units satisfies $0 < E_{coh} phi^2$, where $E_{coh}$ denotes the coherence energy and $phi$ is the golden ratio.
background
In Recognition Science, the mass hierarchy places particles on the phi-ladder. The function mass_on_rung(r) returns E_coh times phi to the integer power r, with the electron fixed at rung 2. This yields the definition m_e = E_coh * phi^2. Module C-009 formalizes the proton-to-electron ratio as phi to the power (r_p minus 2) once the proton rung is obtained from confinement. Upstream results supply the mass_on_rung definition from MassHierarchy and the positivity of phi and E_coh from LeptonMassLadder and ElectronMass.
proof idea
The term proof unfolds m_e and mass_on_rung to expose the product E_coh * phi^2, then applies mul_pos. The first factor is rewritten by replacing the negative exponent in E_coh with an inverse and applying div_pos of 1 over phi^5. The second factor is discharged directly by pow_pos of phi to the 2.
why it matters
This positivity result supports the C-007 resolution in electron_mass_derived, which states that the electron mass equals E_coh times phi squared with no free parameters. It anchors the structural form of the proton-electron ratio in C-009 and aligns with the phi-ladder construction required by the eight-tick octave and D=3 spatial dimensions. The result closes a basic consistency check before the full ratio exponent is derived from the proton confinement step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.