M0_pos
plain-language theorem explainer
The anchor mass M0 is fixed at unity in RS-native units. Workers deriving quark and lepton masses from the phi-ladder or constructing AnchorCert structures cite this positivity result to guarantee that all subsequent scales remain positive. The proof is a one-line wrapper that unfolds the constant definition and normalizes the inequality.
Claim. The anchor mass satisfies $0 < M_0$ where $M_0 := 1$ in RS-native units.
background
In the RSBridge.Anchor module the anchor mass M0 supplies the base scale for the phi-ladder mass formula. The module introduces the Z-map ZOf that assigns charge-indexed integers to the twelve fermions and the gap function F(Z) = ln(1 + Z/φ)/ln(φ) that fixes the rung offset at the anchor scale μ⋆. Upstream the definition M0 := 1 simply chooses units so every physical mass is expressed as a pure phi-power times this yardstick.
proof idea
The proof is a one-line wrapper that applies dsimp to unfold M0 := 1 followed by norm_num to confirm the numerical fact 0 < 1.
why it matters
This theorem supplies the M0_pos field required by the Valid certificate structure and by M0_pos_of_cert in Recognition.Certification; it is also invoked by heavy_anchor_positive when constructing positive charm, bottom and top anchors. It closes the base case for the single-anchor phenomenology claim that integrated RG residues equal gap(ZOf i) at μ⋆. In the broader framework it supports the T8 derivation of three spatial dimensions by ensuring the mass ladder begins from a strictly positive reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.