top_anchor_eq_massAtAnchor
plain-language theorem explainer
The equality shows that the native top-quark anchor mass is identical to the RSBridge anchor-mass formula applied to the top fermion. Researchers deriving heavy-quark masses on the phi-ladder cite it to confirm uniform application of the exponential formula across charm, bottom, and top without external data. The proof is a one-line reflexivity that follows directly from the native definition.
Claim. Let $m_t^{anchor}$ denote the native top-quark anchor mass and let $m_{anchor}(t)$ be the RSBridge anchor mass for the top fermion. Then $m_t^{anchor} = m_{anchor}(t)$.
background
The heavy-quark anchor derivation module computes RS-native masses from the formula $m_{anchor}(f) = M_0 * exp(((rung(f) - 8 + gap(Z(f))) * log phi))$, where phi is the self-similar fixed point, rung and gap are fermion-specific integers, and Z(f) is the charge or related index. The Fermion inductive type enumerates the top quark t among quarks and leptons. The native top anchor is obtained by direct substitution of t into the general formula, yielding a dimensionless value on the phi-ladder.
proof idea
The proof is a one-line reflexivity that follows immediately from the definition of the native top anchor as the direct application of the anchor formula to the top fermion.
why it matters
This statement completes the uniform derivation for the top quark in the quark-anchor module, ensuring the phi-ladder formula applies without additional hypotheses. It supports the Recognition Science program of obtaining all fermion masses from the eight-tick octave and the J-uniqueness fixed point. Parallel statements exist for charm and bottom in the same module; no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.