GapEqualsRunningHypothesis
plain-language theorem explainer
The declaration encodes the hypothesis that the closed-form gap for a fermion equals the integrated two-loop mass anomalous dimension residual between physical and anchor scales, or holds in any degenerate case where a scale or flavor count is zero. A researcher reconciling rung-based masses with QCD running in the Recognition framework would cite this to equate the structural correction to the RGE residue. The definition is a direct disjunction with no lemmas or tactics applied.
Claim. Let $f$ be a fermion species, let $Z(f)$ be the charge-derived integer for $f$, let $R_2$ be the two-loop mass ratio function, and let $N_f$ be the number of flavors. The hypothesis holds if $alpha_phys=0$ or $alpha_anchor=0$ or $N_f=0$ or $F(Z(f)) ln phi = -ln R_2(alpha_phys, alpha_anchor, N_f)$, where $F(Z) = ln(1 + Z/phi)/ln phi$ is the gap function.
background
The module reconciles two mass expressions: the direct rung formula without gap and the anchor-scale formula that inserts the gap correction into the exponent. The gap function is the closed-form residue $F(Z) = ln(1 + Z/phi)/ln phi$ at the anchor scale, with $Z(f)$ obtained from the fermion sector and charge. Upstream, the gap is the product of closure and Fibonacci factors whose main theorem asserts the value 45, while the two-loop mass ratio is supplied by the QCD RGE engine.
proof idea
The declaration is a direct definition of the propositional hypothesis. It constructs the claim as the disjunction of the three degenerate cases or the equality between the scaled gap and the negative logarithm of the two-loop mass ratio. No lemmas are applied and no tactics are used beyond the definition itself.
why it matters
This hypothesis is invoked by SchemeReconciliationCert to certify quark reconciliation and by the trivial witness theorem for degenerate cases. It fills the structural claim that the gap correction equals the integrated mass anomalous dimension residue, supporting the phi-ladder mass formula with gap(Z) correction. In the framework it links the self-similar fixed point to the running-mass integrand and leaves open full numerical discharge beyond the charm sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.