m_top
plain-language theorem explainer
Defines the top-quark mass at the common anchor scale μ* as a pure forward prediction: sector yardstick for up-type quarks, integer rung for the third generation, and charge-band gap at electric charge 2/3. Cited by the six-quark residue-coordinate theorem and the top positivity lemma. The body is a one-line application of the shared mass law.
Claim. The top-quark mass at the anchor $\mu^*$ is $m_t(\mu^*) = \mathrm{predict\_mass}(\text{up sector},\, r_t,\, Z_{\mathrm{up}}(2/3))$, i.e. the sector yardstick times $\varphi^{r_t-8+\mathrm{gap}(Z)}$ with $Z$ the charge-band coordinate at electric charge $2/3$.
background
The module runs a single Convention-A forward pipeline for all six quarks. Inputs are only counting-layer integers (cube geometry), the golden ratio $\varphi$ forced by T5/T6, and $\alpha$ from the same layer. No measured quark mass enters.
The mass law is $m_i(\mu^)=A_s,\varphi^{r_i-8+\mathrm{gap}(Z_i)}$, where $A_s$ is the sector yardstick, $r_i$ is the integer rung (baseline plus generation torsion), and $\mathrm{gap}(Z)=\log_\varphi(1+Z/\varphi)$ is the charge-band correction. Absolute masses still sit behind a calibration seam; the intended observables are dimensionless ratios $m_q/m_e$ at $\mu^$.
Here the sector is up-type, the rung is the top label via $r_{\mathrm{up}}(\mathrm{t})$, and $Z$ is evaluated on the up sector at electric charge $2/3$.
proof idea
Pure definitional abbreviation. The right-hand side calls the shared predict_mass combinator on the up-quark sector, the top rung from the up-sector rung map, and the charge-band coordinate $Z$ at $2/3$. No tactic proof; unfolding yields the yardstick–rung–gap formula of the module pipeline.
why it matters
Closes the third-generation up-type slot in the six-quark forward table. Downstream, m_top_pos records positivity by the general positivity of predict_mass, and all_quark_predictions_have_derived_residue_coordinates packages $m_t$ as a residue mass relative to the electron, showing the quarter/residue coordinates are derived from the same pipeline rather than fitted. The construction sits on the RS mass formula (yardstick $\times,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and the $\varphi$-ladder forced by T5/T6; it is one of the seam-free predictions the verification layer compares to data without PDG targeting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.