stationary_at_anchor
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 γ(μ
claimLet γ 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 in Recognition Science
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.
scope and limits
- Does not establish the numerical value or existence of the anchor scale μ⋆.
- Does not verify the equal-weight condition for concrete fermion species.
- Does not compute or bound second derivatives of the residue.
- Does not implement explicit QCD or QED beta-function kernels.
formal statement (Lean)
145theorem stationary_at_anchor (γ : AnomalousDimension) (f_residue : Fermion → ℝ → ℝ) :
146 ∀ (A : AnchorSpec), A.equalWeight →
147 (A.muStar = muStar) → -- Added: requires anchor alignment
148 ∀ (f : Fermion),
149 (∀ t, deriv (fun s => f_residue f (Real.exp s)) t =
150 (1 / lambda) * γ.gamma f (Real.exp t)) → -- Added: derivative matches FTC form
151 γ.gamma f muStar = 0 →
152 deriv (fun t => f_residue f (Real.exp t)) (Real.log A.muStar) = 0 := by
proof body
Term-mode proof.
153 -- This is the stationarity requirement for the single-anchor policy.
154 intro A _hA hA_eq f h_deriv_form hgamma_zero
155 -- The derivative of f_residue(exp(t)) at t = ln(μ) is (1/λ)·γ(μ) by hypothesis h_deriv_form.
156 -- When evaluated at the canonical anchor A.muStar = muStar = 182.201 GeV,
157 -- and γ(muStar) = 0 by hypothesis, the derivative vanishes.
158 rw [hA_eq]
159 rw [h_deriv_form, Real.exp_log muStar_pos, hgamma_zero, mul_zero]
160
161/-- **STABILITY BOUND THEOREM**
162
163 The second derivative of the RG residue is bounded at the anchor.
164
165 **Proof Structure**:
166 1. The second derivative $\delta^2 f / \delta (\ln \mu)^2$ is proportional to $d\gamma/d\ln \mu$.
167 2. In the perturbative regime near $\mu_{\star}$, the beta functions are small and smooth.
168 3. A bounded second derivative ensures that the anchor is not a singular point.
169 4. This provides the stability guarantee for the Single Anchor RG Policy.
170
171 **STATUS**: HYPOTHESIS (higher-order stability) -/