IndisputableMonolith.Masses.QuarkAnchorDerivation
The QuarkAnchorDerivation module supplies explicit native definitions and equalities for the anchor masses of the charm, bottom, and top quarks. Particle physicists modeling fermion mass hierarchies would cite these to connect the recognition Z-map to concrete quark species. The module is a collection of definitions and one-line equality lemmas that instantiate massAtAnchor using the upstream bridge.
claimThe module defines charm_anchor_native, bottom_anchor_native, and top_anchor_native as instances of massAtAnchor for the respective quarks, together with the equalities charm_anchor_eq_massAtAnchor, bottom_anchor_eq_massAtAnchor, top_anchor_eq_massAtAnchor, charm_rung_eq, bottom_rung_eq, top_rung_eq, charm_Z_eq, bottom_Z_eq, and top_Z_eq.
background
This module sits in the Masses domain and imports the RSBridge.Anchor module, whose doc-comment states: 'This module defines the core bridge between the recognition framework and particle physics: 1. Fermion: The 12 Standard Model fermions (6 quarks + 3 leptons + 3 neutrinos). 2. ZOf: The charge-indexed integer Z_i = q̃² + q̃⁴ (+ 4 for quarks). 3. gap (F): The display function F(Z) = ln(1 + Z/φ) / ln(φ). 4. massAtAnchor: The mass at the anchor scale μ⋆.' The sibling declarations implement these objects specifically for the three heavy quarks.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the quark-specific instantiations of massAtAnchor that complete the fermion bridge for the three heavy quarks. It thereby supplies the concrete inputs required by the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)) when applied to charm, bottom, and top. No downstream theorems yet reference the module.
scope and limits
- Does not treat lepton or neutrino anchors.
- Does not compare derived masses to experimental values.
- Does not derive the general massAtAnchor expression itself.
- Does not address the light quarks u, d, s.
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