gap_up_pos
plain-language theorem explainer
The gap correction for up-type quarks at rung 276 is strictly positive. Researchers reconciling structural phi-ladder masses with running-mass corrections cite this to confirm the sign of the anomalous-dimension integrand. The term proof unfolds the gap definition and chains div_pos with Real.log_pos on the scaled rung and on phi itself.
Claim. $0 < g(276)$ where $g$ denotes the gap correction to the rung number arising from the integrated mass anomalous dimension for up-type quarks.
background
The module reconciles the gap-free rung formula rs_mass_MeV against the anchor expression massAtAnchor that inserts the gap(ZOf f) shift in the exponent. This shift equals the integrated mass anomalous dimension from the anchor scale to the physical scale. Upstream, one_lt_phi establishes phi > 1 while the gap definition in AnchorPolicy supplies the function evaluated here at 276 for up quarks.
proof idea
The term proof first unfolds the gap definition to a quotient of logarithms. It applies div_pos to obtain 0 < 276/phi, then Real.log_pos on that quotient, and finishes with Real.log_pos applied directly to phi via the upstream one_lt_phi lemma.
why it matters
The result supplies the gap_up_positive field inside schemeReconciliationCert_holds, which assembles the full set of sign statements and the running hypothesis. It completes the up-quark case in the mass-scheme reconciliation, supporting the phi-ladder formula whose gap corrections derive from the Recognition Composition Law and the T5 J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.