stationary_at_any
The theorem shows that the model residue function is independent of logarithmic scale, so its derivative vanishes at every muStar for any fermion f. Researchers verifying scale invariance in Recognition Science RG models would cite it to confirm stationarity by construction. The proof is a one-line simplification that reduces the expression to the constant definition of f_residue_model.
claimIn the model where the residue equals the gap of the Z-value of the fermion, for every real number $mu_*$ and every fermion $f$ the derivative satisfies $d/dt [f_{residue model}(f, e^t)]$ evaluated at $t = log mu_* = 0$.
background
The AnchorPolicyModel module supplies a Lean-native stand-in for the Standard-Model RG residue treated as an opaque interface. It defines f_residue_model f mu := gap (ZOf f), making the value independent of the scale argument mu by construction. This permits executable algebraic checks while avoiding axioms for multi-loop kernels. The local setting is the Recognition Science forcing chain (T0-T8) with J-cost and phi-ladder structures supplied by upstream results such as PhiForcingDerived.of and LedgerFactorization.of.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of f_residue_model. Because the model residue ignores its scale argument, the function of t is constant, so the derivative at any point is identically zero.
why it matters in Recognition Science
This result confirms that the model residue satisfies stationarity under logarithmic rescaling, consistent with the anchor identity holding by definition in the module. It supports sibling results such as stability_bound_at_any and equalZ_at_any within the same file. In the broader framework it aligns with the eight-tick octave and D=3 emergence from the phi-fixed point (T6-T8), though the declaration itself remains a definitional model rather than a derivation of the physical RG flow.
scope and limits
- Does not prove the physical SM RG statement or match experimental data.
- Applies only inside the model definition f_residue_model f mu := gap (ZOf f).
- Does not extend to implementations with explicit multi-loop kernels or threshold policies.
- Does not address non-stationary or time-dependent residue extensions.
formal statement (Lean)
45theorem stationary_at_any (muStar : ℝ) (f : Fermion) :
46 deriv (fun t => f_residue_model f (Real.exp t)) (Real.log muStar) = 0 := by
proof body
Term-mode proof.
47 -- `f_residue_model` ignores its scale argument, so the function of `t` is constant.
48 simp [f_residue_model]
49
50/-- In the model, the second derivative is also identically zero, hence bounded. -/