muStar_pos
plain-language theorem explainer
The theorem asserts that the RG anchor scale μ⋆ is positive. Researchers building AnchorSpec structures for stationarity conditions in mass residue transport cite it to satisfy the positivity hypothesis in anchor definitions. The proof reduces immediately to a numerical check on the constant 182.201 via norm_num.
Claim. The renormalization anchor scale satisfies $μ^⋆ > 0$, where $μ^⋆ = 182.201$ GeV is the fixed reference point in the RG transport for mass residues.
background
The RGTransport module supplies the mathematical framework for renormalization group transport of fermion masses, with the integrated residue $f(μ_0, μ_1)$ defined via the integral of the mass anomalous dimension γ_m normalized by λ = ln φ. This connects the structural mass at the anchor to the physical mass through the relation $m_phys = m_struct · φ^{-f}$. The upstream muStar definition supplies the concrete numerical value 182.201 GeV as the anchor scale from the papers; the 'for' structure records meta-realization properties required by the broader self-reference axioms.
proof idea
One-line wrapper that applies norm_num to the definition of muStar.
why it matters
This positivity result is required by the AnchorSpec structure, which abstracts the universal anchor and equal-weight condition for the stationarity theorem stationary_at_anchor. It supports the RG transport connection to the mass formula at the phi-ladder scale, consistent with the eight-tick octave and D = 3 from the forcing chain (T7-T8). The result closes a basic interface for downstream lemmas that assume a positive anchor without deriving its value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.