charm_gap_running_residual_percent
plain-language theorem explainer
The definition supplies the numerical value 0.7 as the percent residual between gap(276) log phi for the charm sector and the integrated two-loop mass anomalous dimension residual over the canonical running window. A physicist reconciling structural phi-ladder masses with QCD running would cite this constant when bounding scheme discrepancies. The definition is a direct constant assignment with no computation or lemmas applied.
Claim. Let $r$ denote the percent residual between $gap(276) · log φ$ and the integrated two-loop charm mass-anomalous-dimension residual in the canonical running window. Then $r := 0.7$.
background
The module compares two mass expressions in Recognition Science: rs_mass_MeV, the structural rung formula phi^(57+r)/2^22 scaled to MeV, and massAtAnchor, the gap-corrected form M0 * exp((rung f - 8 + gap(ZOf f)) * log phi). Their discrepancy equals gap(Z) * log phi, which is identified with the integrated mass anomalous dimension integrand from the RGE. The gap function supplies the correction that reconciles the phi-ladder formula with running, using the two-loop engine mass_ratio_two_loop from Physics.QCDRGE.MassAnomalousDimension.
proof idea
The definition is a direct numerical assignment of the precomputed residual value 0.7.
why it matters
This constant supplies the input for the theorem charm_gap_equals_running_within_one_percent, which proves the residual lies below one percent, and for the structure SchemeReconciliationCert that certifies gap reconciliation for up-type quarks. It closes the numerical link between the mass formula yardstick * phi^(rung - 8 + gap(Z)) and the two-loop RGE residual, consistent with the eight-tick octave and phi-ladder structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.