M0
plain-language theorem explainer
M0 is the anchor mass scale fixed at unity in Recognition Science native units. Researchers deriving absolute fermion masses via the phi-ladder and gap function cite this normalization when converting rung and Z-index values to physical predictions. The declaration is a direct constant assignment with no computation or lemmas required.
Claim. $M_0 = 1$, the anchor mass scale in native units where fermion masses satisfy $m = M_0$ times the exponential of the rung-adjusted gap term times the logarithm of phi.
background
The RSBridge.Anchor module maps the twelve Standard Model fermions to mass predictions. Fermion enumerates the species, ZOf assigns the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks), and gap(Z) = ln(1 + Z/φ)/ln(φ) supplies the closed-form display function. massAtAnchor(f) multiplies M0 by exp(((rung f : ℝ) - 8 + gap(ZOf f)) * log φ). This realizes the single-anchor claim that the integrated RG residue equals gap(ZOf i) at scale μ⋆ to tolerance ~1e-6.
proof idea
The declaration is a direct constant assignment M0 := 1. No lemmas are applied and no tactics are invoked; the value 1 is supplied as the base unit for every mass expression in the module.
why it matters
M0 supplies the yardstick in the mass formula yardstick * φ^(rung - 8 + gap(Z)) on the phi-ladder. It is used in massAtAnchor, anchor_ratio, and QuarkAbsoluteMassResidual, the last of which closes the absolute quark-mass row of the scorecard. The definition normalizes predictions consistent with T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, and T8 D = 3 while keeping ħ = φ^{-5} and G = φ^5 / π in the same units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.