electron_mass_derived
plain-language theorem explainer
Recognition Science fixes the electron mass on the phi-ladder at rung 2 with no free parameters. The theorem states that the RS-unit electron mass is positive and equals the coherence energy times phi squared. Researchers deriving lepton masses from the forcing chain cite this baseline. The proof is a one-line term that pairs the positivity lemma with the rung-equality simplification.
Claim. In RS units the electron mass $m_e$ satisfies $0 < m_e$ and $m_e = E_coh · ϕ^2$, where $E_coh = ϕ^{-5}$ and the exponent 2 is fixed by the lepton rung assignment from the cube geometry.
background
The phi-ladder assigns masses as Anchor.E_coh times phi raised to a rung exponent drawn from Anchor.Integers. For the electron the rung is 2, so the definition unfolds to m_e_rs := Anchor.E_coh * phi^(r_lepton “e”). The coherence energy itself is phi to the minus five, taken from the foundation constants. The module states: “The electron sits on rung r = 2 of the lepton ladder. m_e = E_coh · φ^2 in RS units.”
proof idea
The proof is the term ⟨m_e_pos, m_e_rs_eq⟩. It supplies the positivity result obtained by unfolding and applying positivity, together with the equality obtained by simp on the rung values and rfl.
why it matters
This declaration resolves C-007 by placing the electron on the phi-ladder without adjustable parameters. It rests on the lepton mass ladder and anchor definitions that implement the self-similar fixed point from the forcing chain. The result supports the general mass formula yardstick * phi^(rung − 8 + gap) for the lepton sector and feeds the constants bundle used in the Law of Existence structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.