certified_center_enclosed
plain-language theorem explainer
The certified RG transport exponent for each fermion lies inside its tolerance interval around the tabulated center value. Particle physicists working with the Recognition Science mass ladder would cite this when verifying that the canonical policy values satisfy the enclosure hypothesis. The proof is a short tactic sequence that unfolds the definition and applies nonnegativity of the tolerance together with basic real inequalities.
Claim. For every fermion species $f$, let $c(f)$ denote the certified RG transport exponent and let $0 < ε ≤ 10^{-4}$ be the tolerance. Then $c(f) - ε ≤ c(f) ≤ c(f) + ε$.
background
The module supplies certified values for the RG transport exponents $f^{RG}i(μ^*, μ{end})$ of Standard Model fermions under the Recognition Science framework. Fermion is the inductive type enumerating the charged leptons, quarks, and neutrinos. The function $c(f)$ assigns explicit rational values drawn from the canonical policy, for example 494/10000 for the electron and 4822/10000 for the up quark. The predicate is_certified asserts that a real number lies inside the closed interval of half-width ε centered at $c(f)$. The upstream lemma establishing nonnegativity of ε is invoked directly in the argument.
proof idea
One-line wrapper that unfolds the is_certified predicate, invokes nonnegativity of the tolerance via the upstream lemma f_RG_tolerance_nonneg, and splits into the two endpoint inequalities using the constructor tactic together with sub_le_self and le_add_of_nonneg_right.
why it matters
This theorem verifies that each tabulated center value satisfies the enclosure hypothesis required by the certified RG transport certificate. It supplies the base case confirming that the canonical policy exponents are admissible under the Recognition Science mass-ladder construction. No downstream applications are recorded, leaving open its integration into larger transport or renormalization proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.