f_RG_lower
This definition supplies the lower endpoint of the certified enclosure interval for the renormalization-group transport exponent of a specified fermion species. Researchers bounding SM running couplings or lattice transport factors would cite it to close the interval around the canonical-policy value. The definition is a direct subtraction of the non-negative tolerance from the certified central value, with both operands drawn from upstream J-cost and spectral structures.
claimFor each fermion species $f$, the lower endpoint of the certified enclosure interval equals the certified RG transport value minus the tolerance: $f^RG_{cert}(f) - δ(f)$, where $δ(f) ≥ 0$ is the rational tolerance.
background
The module supplies certified bounds on the SM renormalization-group transport exponent $f^RG_i(μ^*, μ_end)$ obtained from the canonical policy. This exponent integrates the running of couplings or masses between reference and endpoint scales in Recognition Science units with $c=1$ and $ℏ=φ^{-5}$. Upstream structures include the strictly convex J-cost function whose global minimum lies at unity, the spectral emergence of SU(3)×SU(2)×U(1) gauge content with exactly three generations, and the ledger factorization that calibrates the J-function. The Fermion type enumerates the twelve species (d, s, b, u, c, t, e, μ, τ, ν1, ν2, ν3).
proof idea
The definition is a one-line arithmetic subtraction of the tolerance from the certified transport value. No additional lemmas are applied beyond the rationality of both operands and the non-negativity of the tolerance established in a sibling definition.
why it matters in Recognition Science
The lower endpoint is invoked by the downstream theorem that proves the certified interval is nonempty via nlinarith on the non-negative tolerance. It completes the enclosure for the RG transport exponent, ensuring consistency with the eight-tick octave and D=3 spatial dimensions of the Recognition framework. The construction touches the open calibration of tolerance from the phi-ladder mass formula.
scope and limits
- Does not compute explicit numerical values of the tolerance for any fermion.
- Does not prove that the certified central value lies inside the interval.
- Does not address running of couplings outside the SM fermion sector.
- Does not incorporate higher-order loop corrections beyond the canonical policy.
formal statement (Lean)
44def f_RG_lower (f : Fermion) : ℚ := f_RG_certified f - f_RG_tolerance
proof body
Definition body.
45
46/-- Upper endpoint of the certified enclosure interval. -/