canonicalAnchor
plain-language theorem explainer
canonicalAnchor fixes the single-anchor RG policy by setting muStar to 182.201 GeV, lambda to ln phi, and kappa to phi. Mass-ladder and RG-transport papers cite this definition to enforce BLM/PMS stationarity at the top-quark pole without free parameters. The definition is a direct structure record that satisfies AnchorSpec via norm_num on positivity and a placeholder proposition for equal weights.
Claim. The canonical anchor scale is the structure with $muStar = 182.201$, $lambda = ln phi$, $kappa = phi$, and equalWeight as a proposition, where $muStar$ is the BLM/PMS stationarity scale fixed by the RS structure at the top-quark pole.
background
AnchorSpec is the structure that abstracts the PMS/BLM mass-free stationarity condition plus motif equal weights at the anchor scale muStar. It consists of muStar : R with positivity proof, lambda typically ln phi, kappa typically phi, and equalWeight : Prop standing for w_k(muStar, lambda) = 1 for all motifs k. The module supplies a precise Lean surface for single-anchor phenomenology in the mass framework, wiring to Constants.phi and RSBridge.Anchor while isolating assumptions about scale and stability for downstream use. Upstream ZOf maps each fermion to an integer via sector and charge Q, while the related Z definition supplies the integer map used by the anchor relation in the mass papers.
proof idea
This is a definition by direct structure instantiation. It sets muStar to the constant 182.201, discharges muStar_pos via norm_num, sets lambda to Real.log phi and kappa to phi, and assigns True to equalWeight as a placeholder proposition.
why it matters
This definition supplies the fixed anchor values used by canonicalAnchorSpec in RSBridge.ResidueData, where the display identity requires f_residue f muStar = gap(ZOf f). It implements the declared convention from the mass papers that muStar emerges from the RS phi-ladder structure rather than data fitting, connecting to the self-similar fixed point and the eight-tick octave. The module addresses radiative stability and flavor compatibility by making the anchor explicit for RG transport hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.