pith. machine review for the scientific record. sign in
def definition def or abbrev high

muStar

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 253def muStar : ℝ := 182.201

proof body

Definition body.

 254

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.