bottom_anchor_eq_massAtAnchor
plain-language theorem explainer
The equality confirms that the bottom quark native anchor mass matches the RSBridge formula applied to the bottom fermion. Researchers deriving heavy quark masses on the phi-ladder would cite this to lock the bottom rung without external data. The proof is a direct reflexivity step that equates the module definition to the general massAtAnchor application.
Claim. The native bottom anchor mass equals $M_0$ times the exponential of $((rung(b) - 8 + gap(Z(b))) log φ)$, where $b$ denotes the bottom fermion, $M_0$ is the base scale, and $φ$ is the golden-ratio fixed point.
background
The module derives heavy-quark anchor masses directly from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ), producing RS-native dimensionless values with no PDG inputs. bottom_anchor_native is the specialization of this formula to the bottom entry in the Fermion inductive type. Upstream results supply the Fermion constructors (including b) and the massAtAnchor definition that encodes the rung-gap scaling with the phi logarithm.
proof idea
The proof is a one-line wrapper that applies reflexivity to match the native definition bottom_anchor_native with the massAtAnchor call on Fermion.b.
why it matters
This declaration completes the anchor derivation for the bottom quark in the heavy-quark series, supporting the overall mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. It aligns with the T5 J-uniqueness and T6 phi fixed-point steps by enforcing self-similar scaling in the forcing chain. No downstream theorems are listed, so the result serves as a modular building block rather than a direct parent for further claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.