stationary_at_any
plain-language theorem explainer
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.
Claim. In 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.