trivial_gap_equals_running
plain-language theorem explainer
The declaration supplies the degenerate case of the gap-equals-running hypothesis when the physical-scale coupling vanishes. It is cited inside the scheme reconciliation certificate to establish that the structural identity holds in the zero-coupling limit. The proof is a one-line wrapper that unfolds the hypothesis definition and selects the first disjunct.
Claim. For any fermion $f$, anchor coupling $alpha_anchor$, and flavor count $N_f$, the proposition GapEqualsRunningHypothesis$(f,0,alpha_anchor,N_f)$ holds, where the hypothesis asserts that either the physical coupling vanishes or the gap times $log phi$ equals the negative log of the two-loop mass ratio.
background
In the mass-scheme reconciliation module, two mass expressions are compared: the rung formula without gap correction and the anchor formula with gap(Z) correction. The gap is defined as the product of closure and Fibonacci factors in the Gap45 derivation, and also appears in AnchorPolicy as a logarithmic expression involving charge. The GapEqualsRunningHypothesis states that this gap equals the integrated mass-anomalous-dimension residual from the QCD RGE engine. Upstream results include the canonical arithmetic object and the gap definition equaling 45.
proof idea
The proof unfolds the definition of GapEqualsRunningHypothesis and applies the left injection of the disjunction, since the first clause is alpha_phys = 0 which matches the call site.
why it matters
This trivial case closes the hypothesis interface for the scheme reconciliation certificate, which assembles gap_zero_at_neutrino, gap_up_pos, etc., to certify that the gap correction matches the RGE residual. It touches the mass formula reconciliation in the Recognition Science framework, linking the phi-ladder masses to the running via the anomalous dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.