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