f_RG_interval_nonempty
plain-language theorem explainer
The declaration establishes that the lower and upper endpoints of the certified RG transport interval for any fermion satisfy lower endpoint ≤ upper endpoint. Physicists verifying renormalization-group flows in the Recognition Science framework cite it to confirm the enclosure interval is well-formed before applying the certified exponent. The proof is a one-line wrapper that unfolds the endpoint definitions and applies non-linear arithmetic using the non-negativity of the tolerance.
Claim. For any fermion $f$, let $f^RG_lower(f)$ denote the lower endpoint $f^RG_certified(f) - f^RG_tolerance$ and $f^RG_upper(f)$ the upper endpoint $f^RG_certified(f) + f^RG_tolerance$ of the certified enclosure interval. Then $f^RG_lower(f) ≤ f^RG_upper(f)$.
background
The module supplies certified values for the SM RG transport exponent $f^RG_i(μ^*, μ_end)$ obtained from the canonical policy. Fermion is the inductive type enumerating the standard-model fermions (electron, muon, tauon, up, charm, top, down, strange, bottom). The lower endpoint is defined by subtracting the tolerance from the certified center; the upper endpoint is defined by adding the tolerance. Non-negativity of the tolerance is recorded by a separate theorem proved by norm_num.
proof idea
The proof unfolds the definitions of the lower and upper endpoints, expressing them as the certified center minus and plus the tolerance. It then applies the nlinarith tactic to the non-negativity theorem for the tolerance, which directly yields the required inequality.
why it matters
The result sits inside the RGTransportCertificate module that supplies certified SM RG transport exponents. It guarantees the enclosure interval is nonempty, a prerequisite for the absolute-error enclosure form used in certification. Within Recognition Science it supports transport of renormalization-group data across scales while preserving bounds derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.