mass_ratio_formula
plain-language theorem explainer
The theorem states that the ratio of a fermion's running mass between two renormalization scales equals the exponential of the negative integral of its anomalous dimension over the logarithmic interval. Physicists deriving mass residues from the phi-ladder in Recognition Science would cite this when connecting structural masses at the anchor scale to observed values. The proof is a one-line wrapper that unfolds the runningMass definition and applies field simplification.
Claim. Let γ be an anomalous dimension (a smooth, perturbatively bounded function γ(f, μ) for fermion f) and let m_{μ₀} ≠ 0. Then the running mass satisfies m(μ₁)/m(μ₀) = exp(−∫_{ln μ₀}^{ln μ₁} γ(f, e^t) dt).
background
The module formalizes renormalization-group transport for mass residues in Recognition Science. The structure AnomalousDimension encodes the mass anomalous dimension γ_m(μ) as a function of fermion species and scale, required to be differentiable with a perturbative bound |γ| < B for μ > 1. The runningMass function integrates this dimension to produce the residue f(μ₀, μ₁) = (1/λ) ∫ γ_m d(ln μ) with λ = ln φ, the normalization used in the mass formula.
proof idea
The proof is a one-line wrapper that applies the definition of runningMass followed by field_simp to equate the ratio directly to the exponential of the negated integral.
why it matters
This result supplies the explicit RG transport formula that links the structural mass at the anchor μ⋆ = 182.201 GeV to physical masses via m_phys = m_struct · φ^{-f}. It completes the connection theorems described in the module doc-comment and supports the mass formula yardstick · φ^(rung - 8 + gap(Z)) on the phi-ladder. The declaration sits inside the T5–T8 forcing chain by providing the scale-dependent residue needed for D = 3 spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.