is_certified_iff_abs_error_le
plain-language theorem explainer
This theorem equates the certification predicate for a fermion's RG transport value with the absolute deviation from the certified exponent staying inside the tolerance bound. Physicists checking numerical renormalization group flows against the canonical policy would cite it to convert abstract certification into a concrete error test. The proof is a direct biconditional split that applies linear arithmetic to the absolute-value inequalities in both directions.
Claim. For any fermion $f$ and real number $val$, the value $val$ is certified for the RG transport exponent of $f$ if and only if $|val - c(f)| ≤ τ(f)$, where $c(f)$ is the certified RG transport exponent and $τ(f)$ is the tolerance.
background
The RGTransportCertificate module supplies certified values for the Standard Model renormalization group transport exponents $f^{RG}i(μ^*, μ{end})$ obtained from the canonical policy. The Fermion inductive type enumerates the quarks and leptons (electron, muon, tauon, up, charm, top, down, strange, bottom). The predicate is_certified checks membership in the certified interval for a given fermion, while f_RG_certified and f_RG_tolerance supply the center and half-width of that interval.
proof idea
The proof uses the constructor tactic to split the biconditional. The forward direction destructures the certification hypothesis into lower and upper bounds, then applies linarith to obtain the pair of inequalities required by abs_le.mpr. The reverse direction applies abs_le.mp to recover the bounds and uses linarith to reconstruct the certification pair.
why it matters
The equivalence supplies a numerically convenient form for the certified RG transport values stated in the module doc-comment. It supports direct verification of computed exponents against the canonical policy without exposing the internal interval structure. No downstream theorems are recorded, so the result functions as a local utility lemma inside the RGTransportCertificate module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.