is_parameter_free
plain-language theorem explainer
A non-circularity certificate is parameter-free when mass-independent SM beta structure, a positive stationarity tolerance, and ordered dispersion bounds all hold. Anyone citing the anchor-scale certificate uses this predicate as the structural half of non-circularity. It is a three-way conjunction definition, not a derived theorem.
Claim. A non-circularity certificate is parameter-free when (i) its SM beta coefficients match the mass-independent formula $\beta_0^{\mathrm{QCD}}(n_f)=11-\tfrac{2}{3}n_f$, (ii) the stationarity tolerance satisfies $\varepsilon>0$, and (iii) the certified dispersion window obeys $\mu_{\mathrm{lower}}\le\mu_{\mathrm{upper}}$.
background
The module certifies that the RS anchor scale $\mu^\star=182.201,\mathrm{GeV}$ is fixed by PMS/BLM stationarity on the RG flow, not by measured fermion masses. A non-circularity certificate packages the scale under test, a positivity proof, an SM beta structure, and two external numerical packages: stationarity bounds and a dispersion-minimum window.
Mass-independence is the sibling predicate requiring that every $\beta_0^{\mathrm{QCD}}(n_f)$ equal the pure group-theory formula $11-\tfrac{2}{3}n_f$, with no Yukawa or mass parameters. Parameter-free status strengthens that: $\mu^\star$ must be forced by SM gauge structure, the stationarity (PMS) condition, and the golden-ratio normalization $\lambda=\ln\varphi$, with no adjustable knobs.
The honesty split in the module is deliberate: Lean proves the structural claims (P1–P4); external SM RG tools supply the numerical certificates (C1–C3).
proof idea
Pure definition: the predicate is the conjunction of three propositions on a certificate. First conjunct is the mass-independence predicate (beta coefficients equal the group-theory formula for all $n_f$). Second requires the stationarity certificate's tolerance $\varepsilon$ to be strictly positive. Third requires the dispersion certificate's lower bound not to exceed its upper bound. No tactics or lemmas; just Prop-level packaging of structural plus certified numerical side-conditions.
why it matters
This predicate is the structural gate for the two main results in the module. The theorem that the canonical anchor is parameter-free unfolds this definition and discharges the three conjuncts from mass-independence plus the certified stationarity and dispersion packages. The main certificate theorem then exhibits a certificate with $\mu=182.201$ that is both mass-independent and parameter-free.
In the Recognition framework this closes the non-circularity claim for the mass-ladder yardstick: $\mu^\star$ is not fit to fermion data. It sits downstream of the $\varphi$-forced normalization $\lambda=\ln\varphi$ and the SM beta structure, and upstream of any mass-formula use of the anchor. The remaining open surface is numerical (external PMS optimization and $\gamma_m(\mu^\star)\approx 0$), not structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.