IndisputableMonolith.Masses.QuarkSchemeReconciliation
This module reconciles the RS gap function with QCD running masses for quarks by showing the correction vanishes at Z=0 and verifying the charm case matches within one percent. Particle physicists modeling fermion mass hierarchies would cite the SchemeReconciliationCert and its supporting lemmas. The module is a short chain of position lemmas that feed a final certificate theorem built on the gap definition and anomalous dimension.
claim$F(0)=0$ for neutral fermions, with the charm gap residual matching the two-loop running mass to within 1 percent via the reconciliation certificate.
background
The module sits in the Masses domain and imports the RS time quantum from Constants, the fermion bridge from RSBridge.Anchor, and the two-loop MS-bar anomalous dimension from QCDRGE.MassAnomalousDimension. Anchor supplies the core objects: Fermion species, the charge index ZOf = q̃² + q̃⁴ (+4 for quarks), the gap display function F(Z) = ln(1 + Z/φ)/ln(φ), and massAtAnchor at the reference scale. The anomalous dimension governs d log m / d log μ² = -γ_m(α_s) with the two-loop coefficients c0 and c1.
proof idea
This module is a collection of targeted lemmas rather than a single proof. It first places the gap function at zero for neutrinos, then computes explicit gap positions for leptons and up/down quarks, derives the running residual for charm, and closes with the SchemeReconciliationCert that packages the within-one-percent match.
why it matters in Recognition Science
The module supplies the quark-side gap corrections required by the RS mass formula (yardstick × φ^(rung-8+gap(Z))) and feeds the larger mass hierarchy results downstream. It directly addresses the interface between the phi-ladder and QCD running, closing one reconciliation step in the T0-T8 forcing chain.
scope and limits
- Does not compute running for bottom or top quarks.
- Does not extend beyond two-loop anomalous dimension.
- Does not address electroweak corrections to the gap.
- Does not derive the gap function itself.
depends on (3)
declarations in this module (10)
-
theorem
gap_zero_at_neutrino -
theorem
gap_lepton_pos -
theorem
gap_up_pos -
theorem
gap_down_pos -
def
GapEqualsRunningHypothesis -
theorem
trivial_gap_equals_running -
def
charm_gap_running_residual_percent -
theorem
charm_gap_equals_running_within_one_percent -
structure
SchemeReconciliationCert -
theorem
schemeReconciliationCert_holds