anchor_parameter_free
plain-language theorem explainer
The canonical anchor certificate is parameter-free: mass-independent SM beta structure, strictly positive stationarity tolerance, and an ordered dispersion window. Anyone citing non-circularity of μ⋆ = 182.201 GeV needs this status bit. The proof is a short term construction: the mass-independence lemma plus two norm_num checks on the certified bounds.
Claim. The canonical non-circularity certificate for the anchor scale $\mu_\star$ is parameter-free: it is mass-independent under the SM beta structure, its stationarity tolerance satisfies $\varepsilon > 0$, and its dispersion-minimizing bounds obey $\mu_{\mathrm{lower}} \le \mu_{\mathrm{upper}}$.
background
This module certifies that the RS anchor scale $\mu_\star = 182.201$ GeV is fixed by structural stationarity (PMS/BLM) on the SM RG flow, not by measured fermion masses. Non-circularity means: stationarity on the RG flow, beta functions from gauge-group representations only, and no Yukawa or mass inputs in the determination of $\mu_\star$.
Parameter-free status is the conjunction of three facts about a non-circularity certificate: mass-independence of the beta structure, positivity of the stationarity tolerance $\varepsilon$, and an ordered dispersion interval. The canonical certificate packages $\mu = \mu_\star$, the canonical SM beta structure, certified stationarity bounds ($\varepsilon = 0.001$ at $182.201$), and certified dispersion bounds ($[180,185]$ with optimum $182.201$).
Upstream, mass-independence is already proved structurally from the beta-function formula (no mass dependence in $\beta_s,\beta_e$). The stationarity and dispersion records are numerical certificates imported from external SM RG tools (RunDec-class), with Lean only checking the arithmetic inequalities.
proof idea
Unfold parameter-free status and the canonical certificate, then build the three-conjunct witness. The first conjunct is the already-proved mass-independence theorem for the same certificate. The second reduces, after unfolding the certified stationarity record, to $0 < 0.001$, discharged by norm_num. The third likewise unfolds the certified dispersion record to $180.0 \le 185.0$, again by norm_num. No RG dynamics are re-derived here; the proof only assembles structural mass-independence with the certified numeric inequalities.
why it matters
This is the middle status bit in the honesty stack for the anchor. The main certificate theorem (anchor_scale_certified) exists as a package of positivity, mass-independence, and parameter-free status for a certificate with $\mu = 182.201$; this declaration discharges the third conjunct for the canonical package.
In the Recognition framework the anchor $\mu_\star$ is the RG scale at which mass anomalous dimensions are stationary, feeding mass-ladder and coupling normalizations without circular appeal to the masses being predicted. The module is explicit that structure (P1–P4) is proved in Lean while the numeric stationarity and uniqueness claims (C1–C3) are certified externally. Closing parameter-free status makes that boundary machine-checkable rather than rhetorical.
No forcing-chain landmark (T5–T8) is re-proved here; the link is downstream use of a non-circular $\mu_\star$ in RS bridge and verification layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.