top_anchor_native
plain-language theorem explainer
top_anchor_native defines the anchor-scale mass for the top quark by applying massAtAnchor to the top fermion. Researchers deriving heavy quark masses on the phi-ladder cite this definition when working in RS-native units without PDG input. The definition is a direct one-line specialization of the exponential formula involving rung and gap parameters.
Claim. The top quark anchor-scale mass is given by $M_0$ times the exponential of $((rung(t) - 8 + gap(Z(t))) * log phi)$, where $M_0$ is the base scale, rung and gap are the ladder parameters for the top quark, and phi is the self-similar fixed point.
background
The QuarkAnchorDerivation module derives heavy-quark anchor-scale masses directly from the RSBridge formula without PDG masses. As stated upstream, massAtAnchor is the noncomputable function $M_0 * Real.exp(((rung f : R) - 8 + gap(ZOf f)) * Real.log(Constants.phi))$ for fermion f. The Fermion inductive type includes the top quark as constructor t. This setup ensures all masses remain dimensionless and native to the phi-ladder.
proof idea
The definition is a one-line specialization that applies massAtAnchor to the top fermion constructor.
why it matters
This definition feeds the heavy_anchor_positive theorem establishing positivity for charm, bottom, and top anchors, and the QuarkAnchorDerivationCert structure recording rung and Z values. It also supports the equality top_anchor_eq_massAtAnchor. The construction realizes the mass formula on the phi-ladder for the top quark at rung 21, consistent with the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.