M0_pos_of_cert
plain-language theorem explainer
The lemma extracts the positivity of the lower bound of the M0 interval from a valid anchor certificate. Researchers certifying mass anchors in Recognition Science models cite it to confirm the base scale remains positive under the validity predicate. The proof is a direct one-line field projection from the Valid structure.
Claim. Let $C$ be an anchor certificate over a species type with charge map $Z$ and gap display $Fgap$. If $C$ is valid with respect to $Z$ and $Fgap$, then the lower endpoint of the $M_0$ interval in $C$ is strictly positive.
background
AnchorCert is a structure containing an M0 interval, per-species residue intervals Ires, charge-wise centers and epsilons (with eps non-negative). Valid is the predicate requiring M0 lower bound positivity, Fgap membership in Igap intervals, and residue intervals contained in gap intervals. The lemma sits in the Certification module, which supplies certified replacements for anchor identities. It draws on the basic M0 positivity result from RSBridge.Anchor establishing 0 < M0 for the unit base scale.
proof idea
The proof is a one-line term that projects the M0_pos field directly out of the Valid hypothesis hC.
why it matters
This supplies the certified positivity of the base mass scale used in anchor relations and the phi-ladder mass formula. It supports downstream certification of species residues and gap intervals in the Recognition framework. It connects to the M0 definition and positivity theorem in RSBridge.Anchor, ensuring the yardstick remains positive in certified models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.