M0_pos
plain-language theorem explainer
The theorem establishes positivity of the anchor mass M0 at the base of the Recognition Science mass ladder. Researchers deriving fermion masses via the phi-ladder and gap function would cite it to guarantee all subsequent anchor-derived quantities remain positive. The proof is a one-line wrapper that unfolds the constant definition of M0 and applies numerical normalization.
Claim. $0 < M_0$ where the anchor mass $M_0$ equals the constant 1 in RS-native units.
background
The RSBridge.Anchor module maps the 12 Standard Model fermions to integer charge indices Z via ZOf and defines the gap function F(Z) = ln(1 + Z/φ)/ln(φ) that equals the integrated RG residue at the anchor scale μ⋆. The constant M0 supplies the base scale for the mass formula yardstick · φ^(rung - 8 + gap(Z)). Upstream results introduce M0 directly as the definition M0 : ℝ := 1 with no further hypotheses.
proof idea
One-line wrapper that applies dsimp on the definition M0 followed by norm_num to verify the numerical fact 0 < 1.
why it matters
It supplies the required M0_pos field inside the Valid certificate structure and is invoked by heavy_anchor_positive to establish positivity of charm, bottom, and top anchor masses. The result closes the base case for the phi-ladder construction before the Recognition Composition Law and the eight-tick octave are applied downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.