f_RG_certified
plain-language theorem explainer
The definition supplies explicit rational values for the certified renormalization-group transport exponents of each Standard Model fermion under a fixed external policy snapshot. Researchers comparing Recognition Science mass predictions to PDG data cite these numbers when constructing enclosure intervals for transport corrections. The definition consists of a direct case analysis on the Fermion type with no further computation or derivation.
Claim. The map assigning certified RG transport exponents $f^{RG}_i$ takes each Standard Model fermion to a rational number: $f^{RG}(e) = 494/10000$, $f^{RG}(mu) = 288/10000$, $f^{RG}(tau) = 179/10000$, $f^{RG}(u) = 4822/10000$, $f^{RG}(d) = 4764/10000$, $f^{RG}(s) = 4764/10000$, $f^{RG}(c) = 5470/10000$, $f^{RG}(b) = 3807/10000$, $f^{RG}(t) = 98/10000$, and zero otherwise.
background
In the RGTransportCertificate module the definition records the central values of the RG transport exponents $f^{RG}_i(mu^*, mu_end)$ taken from a declared canonical policy. Upstream structures include the J-cost calibration from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of; SpectralEmergence.of supplies the gauge content and three-generation structure that fixes the fermion list. The module note states that these numbers are external conventions, not fit parameters of the RS layer, and must be declared for any PDG comparison.
proof idea
The declaration is an explicit pattern match on the Fermion inductive type. Each constructor is mapped directly to its precomputed rational value taken from the policy snapshot in data/certificates/rg_transport/canonical_2025_q4.json.
why it matters
The definition anchors the enclosure theorems certified_center_enclosed, f_RG_lower, f_RG_upper and is_certified_iff_abs_error_le inside the same module. It separates the external RG transport policy from the core phi-forcing chain (T5 J-uniqueness through T8 D=3) while still allowing direct numerical comparison with experiment. It touches the open question of how tightly the RG flow must align with the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.