M0
plain-language theorem explainer
M0 sets the base mass scale to unity in Recognition Science units. Researchers computing absolute fermion masses on the phi-ladder cite this normalization when applying the gap-corrected exponential formula. The declaration is a direct constant assignment with no computation or lemmas required.
Claim. $M_0 := 1$ in RS-native units, serving as the yardstick multiplier in the mass formula $M_0 * e^{((rung - 8 + gap(Z)) * ln φ)}$ for any fermion species.
background
The RSBridge.Anchor module supplies the core bridge from the recognition framework to Standard Model fermions. It defines the 12 fermion species, the charge-derived integer ZOf(f) = q̃² + q̃⁴ (+4 for quarks), the gap display function F(Z) = ln(1 + Z/φ)/ln(φ), and the massAtAnchor function that multiplies M0 by the exponential of the rung-and-gap term. The local setting is the single-anchor phenomenology claim that the integrated RG residue equals gap(ZOf) at the anchor scale μ⋆ with tolerance ~1e-6.
proof idea
One-line definition that directly assigns the real number 1 to M0.
why it matters
M0 normalizes every downstream mass expression, including massAtAnchor, anchor_ratio, and QuarkAbsoluteMassResidual. It supplies the base scale for AnchorCert structures and M0_pos_of_cert. The choice is consistent with the phi self-similar fixed point (T6) and the phi-ladder mass formula yardstick * φ^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.