charm_mass_pos
plain-language theorem explainer
Charm quark mass positivity follows from the general mass formula in Recognition Science. Researchers auditing Standard Model predictions against the phi-ladder would cite this when confirming all fermion masses remain positive. The proof is a one-line wrapper that instantiates predict_mass_pos at the charm sector, rung, and Z values.
Claim. The predicted mass of the charm quark satisfies $m_c > 0$, where $m(f) = $ yardstick(fermionSector $f$) times phi to the power of (fermionRung $f$ minus 8 plus gap of fermionZ $f$).
background
The module states Standard Model mass predictions via the law $m(p) = $ yardstick(Sector) times phi to the power of (r minus 8 plus gap(Z)), with yardstick, rung, and Z drawn from cube geometry (D=3) and charge structure. fermionMass is the definition that computes this expression for any Fermion by feeding its sector, rung, and Z into predict_mass. Upstream, predict_mass_pos proves the mass expression is strictly positive for every valid sector, rung, and integer Z.
proof idea
One-line wrapper that applies predict_mass_pos to the three arguments extracted by fermionSector, fermionRung, and fermionZ for the charm case.
why it matters
This theorem contributes to the proved mass-law positivity block listed in the module header. It feeds the claim that all Standard Model fermion masses are positive under the phi-scaling formula with zero free parameters. No downstream uses are recorded yet; the result closes one instance of the general positivity statement for the charm rung on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.