stability_bound_at_any
In the AnchorPolicy model the second derivative of the residue function with respect to logarithmic scale is identically zero for any fermion. This bound confirms that the model residue remains stable under scale variations. The proof is a direct term-mode simplification that reduces the expression to the zero function via the definition of f_residue_model.
claimThere exists a positive real number $ε$ such that for every fermion $f$, the absolute value of the second derivative of the map $t ↦ f_{residue model}(f, e^t)$ evaluated at $t = log μ_*$ is less than $ε$.
background
The AnchorPolicyModel supplies a Lean-native stand-in for the RG residue by setting f_residue_model f μ := gap(ZOf f). This definition makes the residue independent of the renormalization scale μ, so the function is constant when expressed in the logarithmic variable t. The module treats the actual multi-loop RG kernel as an opaque interface and works entirely inside this definitional model. Upstream structures include the J-cost calibration from PhiForcingDerived and the ledger factorization that defines the gap function.
proof idea
The term proof refines the witness ε = 1 and then applies simp on the definition of f_residue_model. Because the model residue equals gap(ZOf f) with no dependence on the scale argument, the second derivative is identically zero.
why it matters in Recognition Science
The result closes the local stability check inside the definitional anchor model. It aligns with the Recognition Science forcing chain in which J-uniqueness produces scale-independent fixed points. No downstream theorems currently cite it, and the declaration does not address the open question of lifting the model to a full multi-loop RG proof.
scope and limits
- Does not prove the residue bound for the actual Standard-Model RG flow.
- Does not compute numerical values of the gap function.
- Does not depend on the concrete value of muStar.
- Does not incorporate multi-loop threshold corrections.
formal statement (Lean)
51theorem stability_bound_at_any (muStar : ℝ) :
52 ∃ (ε : ℝ), 0 < ε ∧ ∀ (f : Fermion),
53 |deriv (deriv (fun t => f_residue_model f (Real.exp t))) (Real.log muStar)| < ε := by
proof body
Term-mode proof.
54 refine ⟨1, by norm_num, ?_⟩
55 intro f
56 -- Second derivative of a constant is 0.
57 simp [f_residue_model]
58
59/-- Equal-Z degeneracy holds by definition in the model. -/