stability_bound_at_anchor
plain-language theorem explainer
The theorem shows that a uniform bound less than 1 on the second logarithmic derivative of the RG residue at muStar transfers directly to any equal-weight anchor scale coinciding with muStar. Researchers modeling single-anchor RG flows and mass generation in Recognition Science would cite this result to guarantee local non-singularity at the anchor. The proof is a term-mode argument that substitutes the anchor equality hypothesis and selects epsilon equal to 1.
Claim. Let $f: {Fermion} → ℝ → ℝ$ be the residue map. Suppose that for every fermion $f$ the absolute value of the second derivative of $t ↦ f(f, e^t)$ evaluated at $t = ln μ_⋆$ is strictly less than 1. Then for any anchor specification $A$ satisfying the equal-weight condition and $A.μ_⋆ = μ_⋆$ there exists ε > 0 such that the corresponding second derivative evaluated at ln A.μ_⋆ is bounded by ε for all fermions.
background
AnchorSpec is the structure that packages the universal anchor scale muStar together with the equal-weight predicate on motif weights at that scale, typically with muStar near 182 GeV and parameters drawn from phi. The module implements the Single-Anchor RG Policy by representing the integrated anomalous dimension residue as a hypothesis that equals the geometric gap F(Z) = gap(ZOf i) from RSBridge. This setting reuses Constants.phi and connects to RGTransport for the integral definition of the residue from ln muStar to physical mass scales.
proof idea
The term proof introduces the anchor A and the equality hypothesis hA_eq. It then uses 1 as the witness for epsilon. The constructor splits the goal into positivity of 1 (discharged by norm_num) and the universal quantification over fermions. Rewriting the target with hA_eq reduces the bound exactly to the input hypothesis h_bounded.
why it matters
The declaration supplies the local stability guarantee required by the Single-Anchor RG Policy in the mass framework, ensuring the anchor remains a regular point under RG flow. It closes the higher-order stability hypothesis documented in the module and supports downstream use of the residue identity f_i(μ⋆) = F(Z_i). The result ties into the Recognition Science phi-ladder and RG transport while addressing radiative stability concerns for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.