muStar
plain-language theorem explainer
The definition supplies the fixed numerical value of the universal anchor scale μ⋆ = 182.201 GeV drawn from the Recognition Science mass papers. Researchers modeling RG transport of fermion masses or establishing anchor policies cite this constant when aligning the structural mass scale to the phi-ladder. It is introduced by direct assignment with no computation or derivation inside the module.
Claim. The universal renormalization anchor scale is fixed at $μ^⋆ = 182.201$ GeV.
background
This module formalizes renormalization group transport for mass residues. Fermion masses run with scale according to the anomalous dimension γ_m(μ), and the integrated residue f(μ₀, μ₁) = (1/λ) ∫ γ_m(μ') d(ln μ') determines how structural masses at the anchor relate to physical masses via m_phys = m_struct · φ^{-f}, where λ = ln φ.
proof idea
Direct constant definition that assigns the real number 182.201 to the anchor scale identifier.
why it matters
This definition supplies the numerical anchor required by AnchorSpec and by the theorems display_identity_at_anchor, stationary_at_anchor, stability_bound_at_anchor, and mfv_compatible_at_anchor. It implements the convention μ⋆ from the mass papers, aligning with the phi-ladder mass formula and the stationarity condition at the top-quark pole. The value is treated as a declared convention rather than a fit parameter, closing the reference point for RG transport while leaving higher-order kernels as open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.