anchorClaimHolds
plain-language theorem explainer
The anchorClaimHolds definition encodes the single-anchor phenomenology claim: the RG-integrated residue at the anchor scale lies within tolerance of the gap function evaluated at each fermion's Z value. Physicists checking consistency between running masses and the structural phi-ladder formula would cite it when verifying stationarity of the residue. The definition is realized directly as a quantified inequality over fermions and reference scales with no additional lemmas required.
Claim. Let $γ$ be a mass anomalous dimension and $ε>0$ a tolerance. The claim holds when, for every fermion $f$ and reference scale logarithm $lnμ_{ref}$, $|residueAtAnchor(γ,f,lnμ_{ref}) - gap(Z(f))| < ε$.
background
The RGTransport module defines the integrated residue as $(1/λ)∫_{lnμ₀}^{lnμ₁} γ_m(μ') d lnμ'$, where λ = ln φ and γ_m is the mass anomalous dimension supplied by the AnomalousDimension structure. That structure packages a smooth, perturbatively bounded map Fermion → ℝ → ℝ. The local theoretical setting is the relation m(μ⋆) = m_phys · φ^{f(μ⋆,m_phys)}, so that equality of structural and physical masses at the anchor requires the residue to match the closed-form gap expression.
proof idea
This is a definition that directly states the single-anchor claim as a uniform bound. The body quantifies over all fermions f and reference logarithms, subtracts gap(ZOf f) from residueAtAnchor γ f lnμ_ref, and requires the absolute difference to lie inside the supplied tolerance. No tactics or upstream lemmas are applied inside the definition itself.
why it matters
The definition supplies the precise statement of single-anchor phenomenology invoked by stability_bound_at_anchor in AnchorPolicy and by mass_ratio_phi_power. It fills the claim residueAtAnchor γ f (ln m_phys) ≈ gap(ZOf f) that links RG transport to the closed-form gap in the mass formula. In the Recognition framework it supports the phi-ladder mass assignments and the stationarity condition at the anchor scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.