stationarity_structural
plain-language theorem explainer
Stationarity of the RG residue at the anchor scale μ⋆ is equivalent to vanishing of the mass anomalous dimension for each fermion species. Anyone auditing the non-circularity certificate for μ⋆ cites this as the structural meaning of PMS/BLM stationarity. The proof is a one-line wrapper of the existing iff lemma relating residue derivative to γ.
Claim. For every anomalous-dimension assignment $\gamma$ and fermion $f$, the residue derivative of $\gamma$ at $f$ with respect to $\ln\mu_\star$ vanishes if and only if $\gamma(f,\mu_\star)=0$.
background
The module certifies that the RS anchor scale $\mu_\star=182.201,\mathrm{GeV}$ is fixed by structural stationarity (PMS/BLM), not by measured fermion masses. Non-circularity means: $\mu_\star$ solves a stationarity condition on the RG flow; that condition uses only SM group structure (beta functions); no fermion mass inputs enter the determination.
P1 isolates the meaning of stationarity itself. The residue derivative of the anomalous dimension along $\ln\mu$ at $\mu_\star$ is the local slope of the RG residue. The claim is that this slope is zero precisely when the anomalous dimension $\gamma_m$ itself vanishes at $\mu_\star$ for the given fermion.
Sibling results handle the complementary pieces: mass-independence of SM beta coefficients (P2), the $\phi$-forced normalization $\lambda=\ln\phi$ (P3), and positivity of $\mu_\star$ (P4). Numerical vanishing $\gamma_m(\mu_\star)\approx 0$ is certified externally (C1), not proved here.
proof idea
One-line term-mode wrapper: apply stationarity_iff_gamma_zero at the given anomalous-dimension assignment and fermion. No additional algebraic work; the structural equivalence is already packaged upstream and is merely re-exported under the certificate's P1 name.
why it matters
This is THEOREM P1 of the Anchor Scale Non-Circularity Certificate: it states what stationarity means, namely vanishing anomalous dimension at $\mu_\star$. Without this equivalence, the certificate could not separate structural content (Lean-proved) from external numerics (C1–C3).
It sits beside P2 (SM beta coefficients depend only on gauge representations, no mass parameters), P3 ($\lambda=\ln\phi$), and P4 ($\mu_\star>0$). Together they underwrite the honesty split: structure is proved; the specific GeV value and uniqueness of the dispersion minimum remain certified from external computation. No downstream Lean consumers are recorded yet; the declaration is a named export for the certificate surface and for human audit of the non-circularity claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.