pith. machine review for the scientific record. sign in
structure definition def or abbrev high

AnchorPolicy

show as:
view Lean formalization →

AnchorPolicy is a record type carrying the real parameters λ and κ that fix the renormalization-group anchor for the phi-ladder mass predictions. Mass-spectrum calculations in the Recognition framework cite this interface when they instantiate the canonical values (ln φ, φ) for RG flow and coherence energy. The declaration is a bare structure definition with no proof obligations or computational content.

claimAn anchor policy is a pair of real numbers $ (λ, κ) ∈ ℝ × ℝ $, where λ normalizes the logarithmic renormalization scale and κ sets the stiffness at the anchor point.

background

The structure lives in the Masses.AnchorPolicy module, which imports Constants, the Anchor definitions, and supporting material from RGTransport and thermal-conductivity regimes. Lambda is supplied by the upstream definition 'The λ-normalization constant: λ = ln(φ)' while kappa appears in two sibling contexts: as φ^k in thermal-conductivity regimes and as (log φ)² in the annular-cost stiffness constant. These parameters locate the fixed point of the phi-ladder at the eight-tick octave scale and supply the residue function used by gap(Z) = ln(1 + Z/φ) / ln(φ).

proof idea

The declaration is a bare structure definition that introduces the two fields lambda and kappa with no proof body, tactics, or lemmas applied.

why it matters in Recognition Science

CanonicalPolicy instantiates the structure to the concrete pair (ln φ, φ) and the same record is consumed by gap_down_pos, muon_electron_ratio, lnMuStar, and residueAtAnchor. It therefore supplies the anchor interface required by the mass-ladder formula and the RG-transport residue at μ⋆, closing the link between T6 (phi fixed point) and the explicit mass predictions m_μ / m_e = φ^11.

scope and limits

formal statement (Lean)

  76structure AnchorPolicy where
  77  lambda : ℝ
  78  kappa  : ℝ
  79
  80/-- Canonical anchor policy: `(λ, κ) = (ln φ, φ)` with coherence energy. -/

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.