pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Constants.ElectronMass

show as:
view Lean formalization →

The module defines the electron mass in RS units as E_coh scaled by phi squared, taking the lepton rung r=2 from Anchor. Researchers deriving particle masses on the phi-ladder would cite it for the electron entry. The module assembles four sibling definitions and equalities from the imported Constants, PhiForcing, and Anchor modules.

claimThe electron mass in RS units satisfies $m_e = E_{coh} · φ^2$, where the lepton rung parameter obeys $r_{lepton}(e) = 2$.

background

Recognition Science places all masses on a phi-ladder whose rung and gap parameters are fixed by the Anchor module. The present module imports the base time quantum τ₀ = 1 tick, the self-similar forcing of φ from the J-cost ledger, and the canonical mass constants already centralized in Anchor. Electron mass is obtained by applying the rung value r_lepton(e) = 2 to the coherent-energy yardstick E_coh.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the electron slot required by the mass formula yardstick · phi^(rung - 8 + gap(Z)). It completes the lepton constants begun in the Anchor module and prepares the value for any later comparison or extension within the Constants domain.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (4)