pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Masses.QuarkSchemeReconciliation

show as:
view Lean formalization →

The QuarkSchemeReconciliation module reconciles the Recognition Science gap function with QCD running masses for quarks. It proves the gap vanishes at Z=0 for neutral fermions and shows the charm residual lies within one percent of the running correction. Mass modelers in particle physics would cite it to justify the phi-ladder against standard scheme differences. The argument proceeds by direct substitution into the gap formula followed by explicit residual comparison.

claimThe gap function satisfies $F(0)=0$ for neutral fermions with $Z=0$. The hypothesis that gap equals running holds trivially, and the charm gap residual is at most one percent. The scheme reconciliation certificate is established.

background

The module sits in the masses domain and imports the RS time quantum τ₀=1 tick from Constants. From RSBridge.Anchor it uses the fermion species, the charge index ZOf(F)=q̃²+q̃⁴ (+4 for quarks), and the gap display function gap(F)=ln(1+Z/φ)/ln(φ). From QCDRGE.MassAnomalousDimension it imports the two-loop MS-bar anomalous dimension γ_m(α_s)=c₀α_s+c₁α_s² that governs d log m / d log μ².

proof idea

This is a definition and theorem module. It defines gap_zero_at_neutrino by direct evaluation at Z=0, introduces GapEqualsRunningHypothesis, proves the trivial case by algebraic identity, computes the charm residual percent explicitly, and certifies SchemeReconciliationCert by combining the gap and running expressions.

why it matters in Recognition Science

The module closes the discrete-continuous gap for quark masses in the Recognition framework and supports the phi-ladder mass formula. It feeds downstream mass predictions by confirming that RS gap corrections reproduce QCD running residuals to the stated precision. It touches the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (10)