stationary_at_anchor
plain-language theorem explainer
The stationarity theorem shows that the RG residue for any fermion is stationary with respect to logarithmic scale variations at the canonical anchor μ⋆ whenever the anomalous dimension vanishes there, provided the anchor satisfies equal weights and the derivative relation holds. Researchers modeling renormalization group flows in the Recognition Science mass framework would cite it to justify the single-anchor choice at approximately 182.2 GeV. The proof is a direct term reduction that substitutes the given derivative identity and the zero γ(μ
Claim. Let γ be an anomalous dimension and f_residue a residue function. For any anchor specification A with equal-weight condition and A.μ⋆ = μ⋆, and for each fermion f, if d/dt [f_residue(f, exp(t))] = (1/λ) γ(f, exp(t)) for all t and γ(f, μ⋆) = 0, then d/dt [f_residue(f, exp(t))] evaluated at t = log(A.μ⋆) equals zero.
background
The module supplies the single-anchor RG policy interface. AnchorSpec is the structure holding the universal scale μ⋆ (≈182.201 GeV), λ = ln φ, κ = φ, and the equal-weight predicate. The RG residue is defined as the integrated anomalous dimension f_i(μ⋆) := (1/ln φ) ∫_{ln μ⋆}^{ln m_phys} γ_i(μ') d(ln μ'), arising from the RG equation d(ln m)/d(ln μ) = -γ_m(μ). Upstream RGTransport.stationarity_iff_gamma_zero supplies the mathematical link between vanishing γ at the anchor and stationarity of the residue.
proof idea
Term-mode proof. After introducing the anchor A, the equality A.muStar = muStar, the fermion f, the derivative identity, and γ(f, muStar) = 0, the script rewrites the anchor equality, substitutes the derivative form, applies Real.exp_log at the positive muStar, replaces γ by zero, and reduces the product by mul_zero.
why it matters
The result supplies the first-order stationarity condition required by the single-anchor policy in the mass framework. It directly implements the PMS identification of μ⋆ as the scale where scheme dependence vanishes to linear order and feeds the sibling stability_bound_at_anchor. Within the Recognition Science chain it anchors the phi-ladder mass formula by guaranteeing a fixed point for the residue transport; the open question it leaves is the higher-order stability bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.