gap_down_pos
plain-language theorem explainer
The theorem establishes that the gap correction for down-type quarks is strictly positive. Mass-scheme reconciliation work cites it when certifying sign consistency across flavors. The proof is a term-mode argument that unfolds the gap expression and verifies positivity of both logarithms using the inequality phi greater than 1.
Claim. For down-type quarks the gap correction satisfies $0 < gap(24)$.
background
The module reconciles the rung-based mass formula without gap (rs_mass_MeV) against the gap-corrected massAtAnchor formula. The discrepancy in the exponent is exactly gap(Z) times log phi, which equals the integrated mass anomalous dimension from the anchor scale to the physical scale. gap(Z) is the correction term inserted on the phi-ladder for a species labeled by Z. The constant phi satisfies 1 less than phi, supplied by the upstream one_lt_phi lemma.
proof idea
Unfold the definition of gap. Apply div_pos to reduce positivity to the two logarithms. Show the numerator argument 24 over phi is positive via div_pos and phi_pos, then apply Real.log_pos. Apply Real.log_pos directly to one_lt_phi for the denominator. Finish with linarith.
why it matters
The result is collected into schemeReconciliationCert_holds, which assembles all flavor gap signs and the trivial_gap_equals_running hypothesis. It supplies the down-quark case required for the GapEqualsRunningHypothesis that equates the structural gap to the RGE residual. The declaration supports the mass-scheme identity while leaving open the derivation of the gap formula from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.