RunningCoupling
plain-language theorem explainer
RunningCoupling supplies an abstract structure for a scale-dependent coupling g(μ) that stays positive above 1 GeV and decreases at higher scales, capturing asymptotic freedom. Mass-formula specialists in Recognition Science cite it when specializing to QCD or QED running inside the RG residue calculation. The declaration is a plain structure definition consisting of one function field and two predicate fields.
Claim. A coupling function $g : ℝ → ℝ$ such that $g(μ) > 0$ for all $μ > 1$, and $g(μ₂) < g(μ₁)$ whenever $μ₁ < μ₂$ and $μ₂ > 100$.
background
The module formalizes renormalization-group transport that produces the empirical mass residue f^exp. Fermion masses obey d(ln m)/d(ln μ) = -γ_m(μ); the integrated residue is f(μ₀, μ₁) = (1/λ) ∫ γ_m d(ln μ) with λ = ln φ, which converts structural mass at the anchor scale into physical mass via m_phys = m_struct · φ^{-f}.
proof idea
The declaration is a structure definition that directly introduces the coupling function together with the positivity and asymptotic-freedom predicates; no lemmas or tactics are applied.
why it matters
It supplies the interface for scale-dependent couplings that the RGTransport module uses to build the residue f. The structure is referenced by GravityBridge.RunningCoupling when modeling scale-dependent C_lag. It supports the phi-ladder mass formula (yardstick · φ^{rung-8+gap(Z)}) while leaving explicit SM beta kernels as an open specialization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.