f_residue_model
The definition supplies a computable stand-in for the renormalization-group residue of any fermion species by setting it equal to the gap function at the species' Z index. Researchers modeling the Recognition Science anchor policy would reference it to obtain executable algebraic properties without relying on external axioms. It is realized as a direct assignment to the pre-existing gap expression.
claimFor each fermion species $f$, the model residue is defined by $f_{residue model}(f,μ) := ℱ(Z(f))$, where $ℱ(Z) = ln(1 + Z/φ)/ln φ$ is the closed-form display function and $Z(f)$ is the integer index computed from the fermion's sector and charge quantum numbers.
background
In the AnchorPolicyModel module the Standard-Model RG residue is treated as an opaque interface in the main development, but this file supplies a Lean-native model that sets the residue equal to the closed-form gap by definition. The gap function, defined in RSBridge.Anchor as $ℱ(Z) = ln(1 + Z/φ)/ln φ$, represents the integrated residue at the anchor scale. The auxiliary function ZOf maps each Fermion (an inductive type enumerating quarks and leptons) to its effective integer index Z via sector-dependent formulas involving the charge tildeQ.
proof idea
The declaration is a direct definition that evaluates to gap (ZOf f), ignoring the scale argument mu. It is a one-line wrapper that applies the gap function from the RSBridge.Anchor module to the Z index computed by ZOf.
why it matters in Recognition Science
This definition enables the parent theorems equalZ_at_any, stationary_at_any, and stability_bound_at_any in the same module, which establish degeneracy, vanishing derivative, and bounded second derivative under the model. It fills the role of a computable proxy for the single-anchor closed form claimed in the Recognition Science framework, where the residue equals gap(Z) at the anchor scale. The construction avoids axiom dependencies while preserving the algebraic consequences of the T5 J-uniqueness and phi-ladder structure.
scope and limits
- Does not constitute a proof of the physical RG residue equality.
- Does not incorporate multi-loop renormalization kernels or threshold effects.
- Assumes the gap function as an external definition.
- Applies only within the single-anchor model, not the full multi-scale RG flow.
- Ignores any explicit mu dependence by construction.
Lean usage
theorem stationary_example (muStar : ℝ) (f : Fermion) : deriv (fun t => f_residue_model f (Real.exp t)) (Real.log muStar) = 0 := stationary_at_any muStar fformal statement (Lean)
36noncomputable def f_residue_model (f : Fermion) (_mu : ℝ) : ℝ :=
proof body
Definition body.
37 gap (ZOf f)
38