bottom_anchor_native
plain-language theorem explainer
The definition bottom_anchor_native supplies the RS-native anchor mass for the bottom quark by direct instantiation of the general massAtAnchor formula. Researchers deriving heavy-quark masses on the phi-ladder in Recognition Science cite it when scaling the third-generation down-type fermion without measured inputs. The construction is a one-line abbreviation selecting Fermion.b and applying the exponential expression M0 * exp(((rung b - 8) + gap(ZOf b)) * log phi).
Claim. The RS-native bottom-quark anchor mass is defined by $m_b = M_0 * exp(((r_b - 8) + g_b) * log phi)$, where $r_b$ is the rung of the bottom fermion, $g_b = gap(ZOf b)$ its gap correction, $M_0$ the base scale, and $phi$ the golden-ratio fixed point.
background
Recognition Science places fermion masses on a phi-ladder whose spacing follows from the self-similar fixed point phi and the eight-tick octave. The general massAtAnchor function (imported from RSBridge.Anchor) computes the anchor value for any fermion f as M0 * exp(((rung f - 8) + gap(ZOf f)) * log phi), with rung and ZOf drawn from the Fermion inductive type that enumerates d, s, b, u, c, t and the leptons. This module restricts attention to the heavy quarks, deriving their anchors directly from the RSBridge formula with no PDG data admitted. The upstream massAtAnchor definition supplies the exact expression instantiated here for the bottom case.
proof idea
This is a direct one-line definition that applies the imported massAtAnchor function to the constructor Fermion.b.
why it matters
The definition supplies the concrete bottom-quark instance required by the equality theorem bottom_anchor_eq_massAtAnchor and the positivity theorem heavy_anchor_positive. It also feeds the QuarkAnchorDerivationCert structure that records rung and Z assignments for charm, bottom and top. Within the framework it realizes the mass formula on the phi-ladder for the third-generation down-type quark, consistent with the forcing-chain derivation of D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.