IndisputableMonolith.Masses.QuarkAnchorDerivation
The QuarkAnchorDerivation module instantiates the RSBridge.Anchor definitions to produce native anchor masses for the charm, bottom, and top quarks. It supplies charm_anchor_native, bottom_anchor_native, and top_anchor_native together with their rung and Z equalities. Researchers deriving quark masses on the phi-ladder cite these to obtain explicit instances of massAtAnchor. The module consists of parallel native definitions followed by direct equality lemmas that link each quark to the general anchor scale.
claimThe module defines native anchors $m_c^* = $ massAtAnchor$(Z_c, r_c)$, $m_b^* = $ massAtAnchor$(Z_b, r_b)$, $m_t^* = $ massAtAnchor$(Z_t, r_t)$ for the charm, bottom, and top quarks, together with the equalities charm_anchor_eq_massAtAnchor, bottom_anchor_eq_massAtAnchor, and top_anchor_eq_massAtAnchor.
background
This module belongs to the Masses domain and imports the RSBridge.Anchor module. The upstream Anchor module defines the Fermion type covering the twelve Standard Model particles, the ZOf map Z_i = q̃² + q̃⁴ (+4 for quarks), the gap function F(Z) = ln(1 + Z/φ)/ln(φ), and the massAtAnchor function that returns the mass at the anchor scale μ⋆. QuarkAnchorDerivation specializes these objects to the three heavy quarks by supplying their concrete Z values and rungs on the phi-ladder.
proof idea
This is a definition module. It introduces native definitions for each quark anchor and then proves the three equality lemmas (charm_anchor_eq_massAtAnchor and analogs) by direct instantiation of massAtAnchor on the quark-specific Z and rung parameters.
why it matters in Recognition Science
The module supplies the concrete anchor points required for heavy-quark mass calculations in the Recognition Science framework. It instantiates the general mass formula for charm, bottom, and top, thereby connecting the abstract Anchor definitions to the phi-ladder mass predictions. No downstream theorems are listed yet, but the derivations close the gap between the general bridge and quark-specific applications.
scope and limits
- Does not derive anchors for up, down, or strange quarks.
- Does not compute numerical mass values or experimental fits.
- Does not address leptons or neutrinos.
- Does not prove the underlying massAtAnchor theorem.
depends on (1)
declarations in this module (15)
-
def
charm_anchor_native -
def
bottom_anchor_native -
def
top_anchor_native -
theorem
charm_anchor_eq_massAtAnchor -
theorem
bottom_anchor_eq_massAtAnchor -
theorem
top_anchor_eq_massAtAnchor -
theorem
charm_rung_eq -
theorem
bottom_rung_eq -
theorem
top_rung_eq -
theorem
charm_Z_eq -
theorem
bottom_Z_eq -
theorem
top_Z_eq -
theorem
heavy_anchor_positive -
structure
QuarkAnchorDerivationCert -
theorem
quarkAnchorDerivationCert_holds