stationarity_iff_gamma_zero
plain-language theorem explainer
The equivalence equates vanishing of the residue derivative at the reference scale to the anomalous dimension for a given fermion being zero at that scale. Modelers of RG flow for structural masses in the Recognition Science ladder would cite the result when confirming stationarity of the integrated residue. The proof is a direct term reduction that unfolds residueDerivative, applies the exponential-log identity, and splits the product using the nonzero character of lambda together with the no-zero-divisors lemma.
Claim. For an anomalous dimension function $γ$ and fermion species $f$, the derivative of the residue at $ln μ_⋆$ vanishes if and only if $γ(f, μ_⋆) = 0$.
background
The module supplies the mathematical framework for RG transport of fermion masses. The structure AnomalousDimension packages a map $γ : Fermion → ℝ → ℝ$ that is differentiable and perturbatively bounded; this map encodes the mass anomalous dimension $γ_m(μ)$ appearing in the Standard Model running equation $d(ln m)/d(ln μ) = -γ_m(μ)$. The integrated residue is then defined by $f(μ_0, μ_1) = (1/λ) ∫_{ln μ_0}^{ln μ_1} γ_m(μ') d(ln μ')$ with normalization $λ = ln φ$.
proof idea
The term proof first simplifies residueDerivative and lnMuStar, then rewrites via Real.exp_log. It records that lambda is nonzero from lambda_pos, opens the biconditional, and in one direction applies mul_eq_zero to the product (1/lambda)·γ.gamma f muStar. The converse direction substitutes directly. The key algebraic step is therefore the isolation of γ.gamma f muStar once the prefactor is known to be invertible.
why it matters
The result feeds the anchor residue theorem in AnchorPolicy and the mass-ratio phi-power statement in the same module. It guarantees that stationarity of the residue at the anchor scale is equivalent to vanishing anomalous dimension, thereby closing the link between the RG integral and the phi-ladder mass formula $m = yardstick · φ^{rung-8+gap(Z)}$. In the broader chain it supports the consistency of the structural mass at μ⋆ with the observed physical masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.