anchor_value
plain-language theorem explainer
The canonical anchor certificate carries scale μ⋆ equal to 182.201 GeV. Non-circularity and mass-ladder work cite this numerical pin before packaging positivity and mass-independence. The argument is a one-line unfold of the certificate record against the fixed muStar constant.
Claim. The scale field of the canonical anchor certificate equals $182.201$ GeV, i.e. $\mu^\star = 182.201$.
background
This module certifies that the RS anchor scale $\mu^\star = 182.201$ GeV is fixed by PMS/BLM stationarity on the SM RG flow, not by measured fermion masses. Non-circularity means: stationarity of the flow, beta functions built only from gauge-group representations, and no Yukawa or mass inputs in the determination of $\mu^\star$.
Lean already owns the structural half: stationarity when all mass anomalous dimensions vanish, mass-independence of $\beta_s$ and $\beta_e$, the forced normalization $\lambda = \ln\varphi$, and positivity $\mu^\star > 0$. The concrete number $182.201$ GeV and the claim that $\gamma_m(\mu^\star)\approx 0$ are certified from external SM RG numerics, not derived inside the kernel.
Here $\mu$ is simply the scale field on the certificate record; in RS-native units masses are real scalars on the $\varphi$-ladder, but this theorem only pins the GeV value stored in the canonical certificate.
proof idea
One-line definitional reduction. simp only unfolds the canonical certificate constructor and the muStar constant, exposing the hard-coded equality to $182.201$. No algebraic lemmas and no external RG facts are invoked; the goal is pure record projection. DOC_COMMENT marks the intended shape as definition plus norm_num; the body presently stops at the unfold.
why it matters
Feeds the main package theorem anchor_scale_certified, which asserts existence of a non-circularity certificate with $\mathrm{cert}.\mu = 182.201$, mass-independence, and parameter-free status. Without this numerical pin the existential cannot be discharged by use canonical_anchor_cert.
In the Recognition framework the anchor is the mass yardstick against which the $\varphi$-ladder (rung formula with gap corrections) is read in GeV. Closing non-circularity matters because circular mass input would collapse the claim that particle masses are predicted rather than fitted. Structural pieces (P1–P4 in the module doc) are already proved; this declaration is the thin numerical hinge between those proofs and the external PMS value $182.201$ GeV.
It does not touch T5–T8 forcing, RCL, or the $\alpha$ band directly; it sits in the verification layer that glues SM RG output to the RS mass bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.