AnchorSpec
plain-language theorem explainer
AnchorSpec packages the universal anchor scale muStar together with lambda equals ln phi, kappa equals phi, and the equalWeight proposition that motif weights equal one at that scale. Mass and RG calculations in the Recognition framework cite this record to fix the reference point without free parameters. The declaration is a plain structure definition that bundles the positivity hypothesis on muStar with the placeholder equalWeight field.
Claim. An anchor specification consists of a positive real number $muStar > 0$, a real number $lambda$ (conventionally $ln phi$), a real number $kappa$ (conventionally $phi$), and a proposition equalWeight asserting that the motif weights satisfy $w_k(muStar, lambda) = 1$ for every motif $k$.
background
The module supplies a Lean surface for single-anchor RG policy in the mass framework. It reuses Constants.phi and the gap display function from RSBridge, representing the integrated residue as the hypothesis $f_i(muStar) = F(Z_i)$ with $F(Z) = log_phi(1 + Z/phi)$. The equalWeight field abstracts the PMS/BLM stationarity plus equal motif weights at the anchor. Upstream arithmetic and forcing results guarantee the phi-ladder and self-similar fixed point exist before this policy is stated.
proof idea
This is a structure definition. It declares four fields: the anchor scale with its positivity proof, the two RS-derived parameters, and the equalWeight proposition. No lemmas or tactics are invoked; the body simply records the type.
why it matters
AnchorSpec supplies the predicate used by downstream results including display_identity_at_anchor, stationary_at_anchor, mfv_compatible_at_anchor, and family_ratio_from_display. It fills the P1.5 convention in the mass papers by declaring muStar = 182.201 GeV as fixed by BLM/PMS stationarity at the top-quark pole rather than a fit. The choices lambda = ln phi and kappa = phi connect directly to the phi-ladder fixed point and the eight-tick octave. It leaves open whether the numerical anchor value can be obtained without external stationarity input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.