pith. sign in
module module high

IndisputableMonolith.Physics.RGTransportCertificate

show as:
view Lean formalization →

The module supplies certified definitions for the RG transport exponent f^RG_i(μ*, μ_end) on Standard Model fermions under the canonical policy. Physicists modeling scale-dependent masses via the phi-ladder cite these to obtain certified bounds. The module consists of definitions and certification lemmas that draw directly from the Anchor bridge without external proof obligations.

claimCertified RG transport exponent $f^{RG}_i(μ^*, μ_{end})$ for fermion species $i$, obtained from the gap function $F(Z)$ and anchor scale $μ^*$ with explicit certification that the absolute error lies inside the tolerance interval.

background

The upstream RSBridge.Anchor module defines the Fermion type for the twelve Standard Model species, the charge-indexed integer ZOf giving $Z_i = q̃^2 + q̃^4$ (plus four for quarks), the gap display function $F(Z) = ln(1 + Z/φ)/ln(φ)$, and the massAtAnchor value at the reference scale $μ^$. The present module extends that bridge by packaging the RG transport exponent with certification predicates. The local theoretical setting is the physics layer that converts recognition-scale quantities into certified running masses between $μ^$ and an arbitrary end scale.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the certified transport exponents that feed downstream mass-ladder calculations in the Recognition framework. It directly supports the mass formula yardstick · φ^(rung − 8 + gap(Z)) by furnishing the scale-evolution piece between anchor and target scales, closing the RG-transport step of the T0–T8 forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)