f_RG_tolerance_nonneg
plain-language theorem explainer
Non-negativity of the tolerance for certified RG transport exponents follows directly from its definition as the rational 1/10000. Workers on fermion certification in Recognition Science invoke this to secure interval non-emptiness and center enclosure. The argument is a norm_num reduction on the constant.
Claim. $0 ≤ f_{RG}^{tol}$ where $f_{RG}^{tol} := 1/10000$ is the tolerance for certified SM RG transport exponents.
background
The module treats certified SM RG transport exponents $f^{RG}i(μ^*, μ{end})$ obtained from canonical policy. The tolerance parameter is introduced as the explicit rational constant 1/10000 to bound the certified range for these exponents. The upstream definition supplies the concrete value whose non-negativity is asserted here.
proof idea
One-line wrapper that applies norm_num to the definition of f_RG_tolerance.
why it matters
It supports certified_center_enclosed, which asserts enclosure of the certified center for every fermion, and f_RG_interval_nonempty, which establishes that the lower bound does not exceed the upper bound. Within the Recognition Science framework this secures the basic positivity needed for the RG transport certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.