lnMuStar
plain-language theorem explainer
Defines ln(μ⋆) as the natural logarithm of the anchor renormalization scale to serve as the lower bound in RG residue integrals. Mass renormalization work in the Recognition framework cites this when evaluating integrated residues from the structural anchor to a reference scale. It is a direct one-line definition that applies the real logarithm to the pre-defined muStar constant.
Claim. $ln μ^⋆ := log μ^⋆$, where $μ^⋆$ is the renormalization anchor scale used as the lower limit in the integrated residue $f_i(μ^⋆, μ_{ref}) = (1/λ) ∫_{ln μ^⋆}^{ln μ_{ref}} γ_i(e^t) dt$.
background
The module sets up renormalization group transport for mass residues. Fermion masses run according to d(ln m)/d(ln μ) = -γ_m(μ), and the integrated residue from anchor to reference is normalized by λ = ln φ. This supplies the lower integration bound ln μ⋆ for that formula. It draws on muStar (same module) and the AnchorPolicy structure whose lambda and kappa fields encode the canonical (ln φ, φ) choice.
proof idea
One-line definition that applies Real.log directly to muStar.
why it matters
It supplies the anchor logarithm required by residueAtAnchor to compute the residue at μ⋆, which in turn feeds the stationarity_iff_gamma_zero theorem. The definition closes the lower bound in the RG transport integral that links the structural mass at the anchor to the physical mass via the phi-ladder, implementing the framework described in the module doc for plugging in anomalous-dimension kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.