f_RG_upper
This definition supplies the upper endpoint of the certified enclosure interval for the renormalization-group transport exponent of each Standard Model fermion. A physicist bounding running couplings between scales would cite it to close the interval around tabulated central values. The definition is a direct sum of the certified exponent and the fixed tolerance of 10^{-4}.
claimFor a fermion species $f$, the upper endpoint is $f_{RG,upper}(f) := f_{RG,certified}(f) + 10^{-4}$, where $f_{RG,certified}(f)$ is the tabulated central value of the RG transport exponent.
background
The module supplies certified values of the SM renormalization-group transport exponent $f^{RG}i(mu^*, mu{end})$ for each fermion under a canonical policy. Fermion is the inductive type listing the charged leptons, quarks, and neutrinos. The certified central values are tabulated explicitly (for example 494/10000 for the electron) while the tolerance is the constant rational 1/10000. Upstream results define the central values and the tolerance separately, with the latter carrying the hypothesis that the true exponent lies inside the resulting interval.
proof idea
This is a one-line definition that adds the certified central value to the tolerance. No lemmas or tactics are invoked beyond the arithmetic combination of the two upstream definitions.
why it matters in Recognition Science
The upper endpoint is used directly by the theorem establishing that the certified interval is nonempty. It thereby supports the enclosure hypothesis for RG transport exponents in the Recognition Science framework, consistent with the certified SM values derived from the canonical policy. It closes one step in the chain that bounds physical running quantities without introducing new hypotheses.
scope and limits
- Does not derive the RG exponents from the Recognition Science functional equation.
- Does not apply to bosons or composite states.
- Does not specify the renormalization scales mu* and mu_end.
- Does not tighten the tolerance beyond the fixed 10^{-4} value.
- Does not verify the enclosure against external data.
formal statement (Lean)
47def f_RG_upper (f : Fermion) : ℚ := f_RG_certified f + f_RG_tolerance
proof body
Definition body.
48