mass_on_rung
plain-language theorem explainer
Mass on rung supplies the explicit formula for fermion masses in Recognition Science as the coherence energy E_coh multiplied by the golden ratio phi raised to the integer rung r. Researchers deriving structural mass ratios such as proton to electron cite this when expressing the hierarchy geometrically without free Yukawa parameters. The implementation is a direct one-line assignment from the anchor energy and phi exponentiation.
Claim. The mass of a fermion on rung $r$ is $m(r) = E_0 phi^r$, where $E_0$ is the coherence energy scale and $phi$ is the golden ratio fixed by self-similar forcing.
background
The module formalizes P-002, the fermion mass hierarchy from the phi-ladder. Each fermion occupies an integer rung on this ladder, with mass proportional to phi to that power because phi is the self-similar fixed point forced in the T0-T8 chain. The coherence energy E_coh serves as the base scale in RS-native units where c=1 and hbar=phi^{-5}. Upstream rung definitions map specific fermions to integers, for example electron to rung 2 and muon to rung 13, drawn from the Fermion type in RSBridge.Anchor.
proof idea
The definition is a direct one-line assignment that multiplies the imported coherence energy by phi raised to the rung power. No lemmas or tactics are invoked beyond the basic field operations and the phi constant from PhiForcing.
why it matters
This definition supplies the geometric mass law that dissolves the hierarchy problem, as shown in the downstream theorem hierarchy_problem_dissolves which states the equality directly. It is invoked by the structural ratio theorems in ProtonElectronMassRatio, including mass_ratio_structural and proton_electron_ratio_from_ladder, to obtain m_p/m_e = phi^(r_p-2). The construction aligns with the phi-ladder from T6 and the eight-tick octave from T7, removing free parameters that appear in the Standard Model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.