f_residue_model_at
plain-language theorem explainer
The model sets the residue of any fermion f at chemical potential mu equal to the gap computed from Z(f). Anchor-policy modelers in Recognition Science cite it to obtain executable stationarity and stability statements without RG integration. The proof is a one-line reflexivity on the model's definitional equation.
Claim. For fermion $f$ and real number $mu$, the model residue equals the gap at $Z(f)$: $f_{residue model}(f, mu) = gap(Z(f))$.
background
The AnchorPolicyModel module supplies a Lean-native stand-in for the Standard-Model RG residue, defined by construction as $f_{residue model} f mu := gap (ZOf f)$. Here gap is the product of closure and Fibonacci factors from Gap45.Derivation, whose main theorem asserts the value 45. Fermion is the type imported from Masses.RSBridge.Anchor; ZOf extracts the effective integer label used in the phi-ladder mass formula. The module treats the true residue as an opaque interface and substitutes this closed form so that algebraic consequences remain computable.
proof idea
One-line wrapper that applies reflexivity to the definitional equation of f_residue_model.
why it matters
The result lets downstream lemmas on stationarity and stability become trivial inside the model, as noted in the module's Consequences section. It realizes the anchor identity by fiat, consistent with the Recognition Science use of gap in mass formulas and the eight-tick octave. The declaration leaves open the derivation of the physical residue from multi-loop kernels rather than the model substitution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.