IndisputableMonolith.Physics.RGTransportCertificate
This module certifies the RG transport exponent f^RG_i(μ*, μ_end) for each Standard Model fermion using the canonical policy. Particle physicists applying Recognition Science mass ladders would cite these bounds to control scale evolution from the anchor. The module supplies definitions for the certified function together with lemmas on tolerance non-negativity and interval enclosure.
claimCertified RG transport exponent $f^{RG}_i(\mu^*, \mu_{end})$ for fermion species $i$, obtained from the canonical policy with explicit error tolerance.
background
The module imports the RSBridge.Anchor definitions: Fermion (the 12 SM species), ZOf (charge-indexed integer $Z_i = \tilde{q}^2 + \tilde{q}^4$ plus 4 for quarks), gap(F) given by $F(Z) = \ln(1 + Z/\phi)/\ln(\phi)$, and massAtAnchor at scale $\mu^\star$. These supply the input data for the transport exponent. The local setting is the bridge that converts recognition-theoretic quantities into SM particle masses via the phi-ladder.
proof idea
This is a definition module, no proofs. It introduces the certified function f_RG_certified together with auxiliary predicates is_certified, f_RG_lower, f_RG_upper and the supporting lemmas f_RG_tolerance_nonneg, f_RG_interval_nonempty, is_certified_iff_abs_error_le, certified_center_enclosed.
why it matters in Recognition Science
The module supplies the certified transport step required for any downstream mass calculation that starts from the anchor scale. It therefore feeds the Recognition Science mass formula that places each fermion on the phi-ladder using gap(Z). No direct used_by edges are recorded, but the definitions close the canonical-policy interface between the RSBridge and physics-scale evolution.
scope and limits
- Does not evaluate the exponent at concrete numerical scales.
- Does not derive the canonical policy itself.
- Does not address non-SM fermions.
- Does not replace the underlying RG flow equation.