is_certified
plain-language theorem explainer
The definition is_certified states that a real number val lies inside the certified enclosure for fermion f precisely when it satisfies the two-sided inequality around the precomputed RG transport exponent. Researchers verifying renormalization group flows for Standard Model fermions in Recognition Science would cite this enclosure predicate when checking numerical consistency of transport exponents against canonical policy outputs. It is implemented as a direct interval membership predicate using the sibling declarations f_RG_certified and f_R
Claim. For fermion $f$, real $v$ is certified when $f^{RG}_{certified}(f) - t(f) ≤ v ≤ f^{RG}_{certified}(f) + t(f)$, where $t(f)$ is the tolerance for the RG transport exponent of $f$.
background
The module supplies certified enclosures for Standard Model RG transport exponents $f^{RG}i(μ^*, μ{end})$ obtained from the canonical policy. These exponents sit on the phi-ladder and are calibrated via J-cost minimization. Upstream structures include PhiForcingDerived.of, which encodes the J-cost functional $J(x) = (x + x^{-1})/2 - 1$, and SpectralEmergence.of, which derives the gauge content SU(3)×SU(2)×U(1) together with exactly three generations and 24 chiral fermions from the Q3 structure. LedgerFactorization.of supplies the underlying (ℝ₊, ×) calibration of J, while NucleosynthesisTiers.of organizes nuclear densities in discrete phi-tiers.
proof idea
This is a definition that directly constructs the Prop as the conjunction of the lower and upper bounds. It casts the certified center and tolerance values to ℝ and asserts closed-interval membership. No lemmas are applied; the body is a one-line interval predicate.
why it matters
The predicate supplies the core hypothesis used by the downstream theorems certified_center_enclosed and is_certified_iff_abs_error_le. It formalizes the claim that true RG transport exponents lie inside certified tolerances, supporting verification of SM parameters inside the Recognition Science forcing chain (T5 J-uniqueness, T7 eight-tick octave). It closes a verification interface without requiring explicit computation of the full RG flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.