heavy_anchor_positive
plain-language theorem explainer
The theorem proves that the RS-native anchor masses for the charm, bottom, and top quarks are strictly positive. A physicist deriving the heavy quark spectrum from the Recognition Science phi-ladder would reference this result to guarantee the scales lie above zero before comparing to experiment. The proof is a direct term-mode application of the positivity of M0 and the exponential function after unfolding the massAtAnchor definitions.
Claim. Let $m_c = M_0$ exp$(((r_c - 8 + g(Z_c)) log φ))$, and similarly for $m_b$ and $m_t$, where $r_f$ is the rung of fermion $f$, $Z_f$ its charge, and $g$ the gap function. Then $m_c > 0$, $m_b > 0$, and $m_t > 0$.
background
The module derives heavy-quark anchor-scale masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ). No PDG masses enter. The result is RS-native and dimensionless. The anchor masses are defined as charm_anchor_native := massAtAnchor Fermion.c, and analogously for bottom and top. The theorem M0_pos establishes 0 < M0, and massAtAnchor is the exponential expression involving the phi constant. This sits in the Masses domain of Recognition Science, building on the anchor definitions in RSBridge.Anchor.
proof idea
The proof unfolds charm_anchor_native, bottom_anchor_native, top_anchor_native, and massAtAnchor. It then uses constructor to split the three-way conjunction into separate goals. Each goal is discharged by mul_pos applied to M0_pos and Real.exp_pos _.
why it matters
This result feeds the quarkAnchorDerivationCert_holds theorem, which assembles the full certification of the quark anchor derivation. It confirms the positivity required for the mass formula on the phi-ladder, ensuring the heavy quark anchors (rungs corresponding to charm, bottom, top) are positive quantities in the Recognition Science framework. The derivation avoids experimental input, remaining fully native to the T0-T8 forcing chain and the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.