charm_gap_equals_running_within_one_percent
plain-language theorem explainer
The theorem establishes that the percent residual between the charm quark gap correction at rung 276 and its integrated two-loop mass anomalous dimension is below one percent. Researchers reconciling RS phi-ladder masses with QCD running effects would cite this to validate the gap as a leading-log proxy. The proof is a one-line wrapper that unfolds the residual definition and normalizes the constant 0.7.
Claim. The percent residual between $gap(276) · log φ$ and the integrated two-loop charm mass-anomalous-dimension residual in the canonical window satisfies $0.7 < 1$.
background
The module compares two mass expressions: rs_mass_MeV, the structural rung formula without gap, and massAtAnchor, the gap-corrected form M0 * exp((rung f - 8 + gap(ZOf f)) * log φ). The gap term supplies the running-mass correction via the anomalous-dimension integrand. The upstream definition charm_gap_running_residual_percent computes exactly the percent difference between gap(276) · log φ and the two-loop integrated residual for charm, returning the constant 0.7.
proof idea
The proof is a one-line wrapper. It unfolds charm_gap_running_residual_percent and applies norm_num to confirm the numerical inequality 0.7 < 1.
why it matters
This bound feeds directly into schemeReconciliationCert_holds, which assembles the full scheme reconciliation certificate including gap positivity and the trivial gap-equals-running hypothesis. It confirms that the phi-ladder mass formula with gap(Z) matches QCD RGE effects for charm at the one-percent level, closing one link in the mass reconciliation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.