family_ratio_from_display
Physicists deriving intra-family fermion mass ratios on the Recognition Science phi-ladder cite this result to obtain exact phi-power expressions once Z values match. For equal-Z fermions the anchor masses satisfy a ratio fixed solely by rung difference. The proof is a one-line wrapper applying the anchor_ratio theorem from RSBridge.Anchor.
claimLet $f$ and $g$ be fermions with $Z(f)=Z(g)$. Under the display-identity hypothesis at the anchor and the equal-weight condition on the anchor specification, the ratio of anchor masses is $m_f/m_g=exp((r_f-r_g)log phi)$, where $r_f$ and $r_g$ denote the rung levels of $f$ and $g$.
background
The module supplies a single-anchor RG policy for the mass framework. AnchorSpec encodes the universal anchor scale together with the equal-weight condition on motifs at that scale. The display identity hypothesis encodes the claim that the integrated RG residue equals the gap function of Z. Upstream, the anchor_ratio theorem from RSBridge.Anchor already establishes the mass-ratio formula under equal Z by unfolding the definition massAtAnchor f := yardstick * phi^(rung f - 8 + gap(ZOf f)) and subtracting the exponents when the gaps coincide.
proof idea
One-line wrapper that applies the anchor_ratio theorem from the RSBridge module.
why it matters in Recognition Science
The result supplies the structural form of equal-Z mass ratios on the phi-ladder, feeding lepton and quark mass derivations such as the muon-to-electron example m_μ/m_e = phi^11 noted in the module. It instantiates the general mass formula yardstick * phi^(rung-8+gap(Z)) for the equal-Z case, consistent with phi self-similarity and the eight-tick octave in the Recognition framework.
scope and limits
- Does not prove the display identity hypothesis.
- Does not compute numerical mass values.
- Does not treat ratios between fermions with unequal Z.
- Does not incorporate scale-dependent radiative corrections beyond the anchor.
formal statement (Lean)
265theorem family_ratio_from_display (_f_residue : Fermion → ℝ → ℝ)
266 (_h_disp : display_identity_at_anchor_hypothesis _f_residue)
267 (_A : AnchorSpec) (_hA : _A.equalWeight)
268 (f g : Fermion) (hZ : ZOf f = ZOf g) :
269 massAtAnchor f / massAtAnchor g =
270 Real.exp (((rung f : ℝ) - rung g) * Real.log phi) :=
proof body
Term-mode proof.
271 anchor_ratio f g hZ
272
273/-- Instantiation for leptons: m_μ / m_e = φ^11. -/