AnchorSpec
AnchorSpec bundles the universal RG anchor scale μ⋆ > 0 with derived parameters λ = ln φ and κ = φ together with the equal-weight motif condition into a single predicate. Mass-framework and RG-transport papers cite it to reference the PMS/BLM stationarity assumption at the top-quark pole without restating the numerical conventions. The declaration is introduced as a plain structure definition whose documentation records the convention status explicitly.
claimThe structure AnchorSpec consists of a positive real number $μ^⋆$, real numbers $λ$ and $κ$, and a proposition equalWeight asserting that motif weights $w_k(μ^⋆, λ)$ equal 1 for every motif $k$. It encodes the universal anchor with the conventions $μ^⋆ = 182.201$ GeV, $λ = ln φ$, and $κ = φ$.
background
The Single-Anchor RG Policy module supplies a Lean interface for the single-anchor phenomenology of the mass framework. It reuses Constants.phi and RSBridge.Anchor, connects to Fermion and ZOf, and states the integrated RG residue $f_i(μ^⋆) := (1/ln φ) ∫_{ln μ^⋆}^{ln m_phys} γ_i(μ') d(ln μ')$ as a hypothesis that is conjectured to equal the display function F(Z) = gap(ZOf i). The actual QCD/QED kernels remain outside Lean and are supplied by external transport codes.
proof idea
The declaration is a structure definition that directly introduces the five fields muStar, muStar_pos, lambda, kappa, and equalWeight. The only proof obligation is the positivity witness muStar_pos, supplied by norm_num in the canonical instance; equalWeight is left as an open Prop whose concrete content is discharged by downstream theorems.
why it matters in Recognition Science
AnchorSpec is the interface that feeds canonicalAnchor, display_identity_at_anchor, family_ratio_from_display, mfv_compatible_at_anchor, stability_bound_at_anchor, and stationary_at_anchor. It records the Source-Super convention that fixes μ⋆ by the BLM/PMS stationarity condition and derives λ and κ from the φ-ladder (T6–T7). The structure thereby closes the scaffolding for flavor-universal RG transport while leaving the numerical verification of equalWeight as an open empirical check.
scope and limits
- Does not implement the QCD 4L or QED 2L anomalous-dimension kernels.
- Does not prove that the equal-weight condition holds for any concrete motif set.
- Does not derive the numerical value of μ⋆ from first principles inside Lean.
- Does not address multi-anchor or scale-dependent weight extensions.
formal statement (Lean)
71structure AnchorSpec where
72 muStar : ℝ
73 muStar_pos : 0 < muStar
74 lambda : ℝ -- typically ln φ
75 kappa : ℝ -- typically φ
76 equalWeight : Prop -- stands for w_k(μ⋆,λ)=1 ∀ motif k
77
78/-- The canonical anchor from Source-Super and the mass papers.
79
80**CONVENTION STATUS** (P1.5 Policy Knob Audit):
81- `muStar := 182.201 GeV` is a **declared convention**, NOT a fit parameter.
proof body
Definition body.
82 It is determined by the BLM/PMS stationarity condition at the top-quark pole.
83 The specific numerical value emerges from the RS structure, not from fitting
84 to experimental data.
85- `lambda := ln φ` is **derived** from the φ-ladder structure.
86- `kappa := φ` is **derived** from the golden ratio.
87
88These values are NOT adjusted to improve agreement with experiment.
89They are fixed by the RS structure and then compared to experiment. -/