CharmMSBarCert
plain-language theorem explainer
The charm MS-bar certification structure packages the rung assignment for charm, positivity and central value of the PDG mass, and positivity of the two-loop running prediction for any positive strong couplings. Heavy-quark phenomenologists checking Recognition Science mass predictions would cite this to confirm that the rung-15 structural value evolves into the observed band after QCD running. The definition assembles the four properties directly from the module constants and the imported two-loop running function.
Claim. A structure asserting rung equality $r=15$ for charm, positivity $0<m_c^{PDG}$, central value $m_c^{PDG}=1.27$ GeV, and the universal positivity statement that $m_c^{predicted}(a_{m_c},a_{M_Z})>0$ whenever $a_{m_c}>0$ and $a_{M_Z}>0$, where $m_c^{predicted}$ is the two-loop mass running from the $M_Z$ anchor.
background
Recognition Science places the charm quark at rung 15 on the phi-ladder via the sector formula for up-type generation 2. The module records the PDG central value $m_c^{PDG}=1.27$ GeV at the charm scale together with the reference rung $r=15$. The auxiliary function $m_c^{predicted}$ applies the two-loop mass anomalous dimension (imported from MassAnomalousDimension) to evolve the RS anchor mass at $M_Z$ down to the charm scale, using the two-loop alpha_s running from TwoLoopAlphaS and threshold matching.
proof idea
The structure is introduced by direct enumeration of its four fields: rung equality to the constant r_charm, positivity of m_c_PDG_GeV, equality of that constant to 1.27, and the quantified positivity of m_c_predicted for positive alpha inputs. No lemmas or tactics are invoked; the definition simply bundles the three referenced sibling definitions.
why it matters
The structure supplies the certificate instantiated by the downstream theorem charmMSBarCert_holds, which closes the charm sector scorecard. It confirms that the RS mass formula at rung 15, after two-loop QCD evolution between $M_Z$ and the charm scale, reproduces the PDG central value inside the quoted band. The construction relies on the RGE modules to handle scale dependence while leaving the underlying phi-ladder mass formula untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.