pith. sign in
module module high

IndisputableMonolith.Physics.RGTransportCertificate

show as:
view Lean formalization →

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)