m_charm
plain-language theorem explainer
Defines the charm-quark mass at the common anchor scale μ* as a pure forward prediction: up-sector yardstick, charm rung from generation torsion, and charge-band gap at Z = 2/3. Cited by the charm/up = φ^11 ratio and the six-quark residue-coordinate theorem. Body is a one-line application of the shared predict-mass formula; no PDG input.
Claim. The charm quark mass at the anchor scale $\mu^*$ is the forward mass prediction in the up-type sector using the integer rung assigned to charm and the charge-band coordinate $Z$ of an up-type quark at electric charge $2/3$: $m_c(\mu^*) = A_{\mathrm{up}}\,\varphi^{r_c-8+\mathrm{gap}(Z_{c})}$.
background
The module builds one forward pipeline for all six quark masses under Convention A: sector yardsticks from cube geometry, integer rungs from generation torsion, and gap(Z) from the charge-band map. Nothing from the PDG enters. Absolute masses still sit on a calibration seam, so the pipeline emphasizes dimensionless ratios to the electron at the same anchor μ*.
The mass law is $m_i(\mu^*)=A_s\varphi^{r_i-8+\mathrm{gap}(Z_i)}$, with $A_s=2^{B_{\mathrm{pow}}(s)}E_{\mathrm{coh}}\varphi^{r_0(s)}$ and $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$. Here the sector is up-type, the rung is the charm entry of the up-rung table, and $Z$ is the up-sector band map at charge $2/3$. Constants are RS-native: $\varphi$ from T5/T6, counting integers $(V,E,F,\ldots)$ from the ledger layer.
Upstream mass and $Z$ symbols in the dependency graph are ledger column-mass and path-sum normalizers used elsewhere in the SevenGaps stack; this definition only consumes the mass-law and anchor rung/Z maps imported by the pipeline.
proof idea
One-line definitional wrapper. It instantiates the shared predict-mass function at three fixed inputs: the up-quark sector tag, the charm rung $r_{\mathrm{up}}(\mathrm{c})$, and the charge-band value $Z$ for up-type quarks at electric charge $2/3$. No tactic proof; the mathematical content is entirely in those three arguments and the mass-law body of predict-mass.
why it matters
Pins the charm mass as a genuine forward output of the unified quark pipeline, not a fit. Downstream, charm_to_up_eq_phi11 quotes it to obtain $m_c/m_u=\varphi^{11}$ from the rung gap $15-4=11$, a clean φ-ladder check. The positivity lemma m_charm_pos is immediate from predict-mass positivity. The six-quark theorem all_quark_predictions_have_derived_residue_coordinates packages $m_c$ with the other five masses as residueMass relative to the electron, tying the quarter/residue coordinate story to the same pipeline.
In the broader RS chain this sits on T5/T6 (φ uniqueness and fixed point) and the mass formula yardstick × φ^(rung−8+gap(Z)). It supports the module claim that all six quarks are predicted from counting integers, φ, and α alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.