lnphi

formal source

  52/-! ## Core Constants (from existing infrastructure) -/
  53
  54/-- Log of golden ratio. -/
  55noncomputable def lnphi : ℝ := Real.log phi
  56
  57/-- Display function F(Z) = log(1 + Z/φ) / log(φ).
  58    This is exactly `RSBridge.gap`. We provide an alias for clarity. -/
  59noncomputable def F (Z : ℤ) : ℝ := gap Z
  60
  61/-- Verify F matches RSBridge.gap. -/
  62theorem F_eq_gap (Z : ℤ) : F Z = gap Z := rfl
  63
  64/-! ## Anchor Specification -/
  65
  66/-- Universal anchor scale and equal‑weight condition.
  67    This abstracts "PMS/BLM mass‑free stationarity + motif equal weights at μ⋆"
  68    into a single predicate that downstream lemmas can reference.
  69
  70    From Source-Super: μ⋆ = 182.201 GeV, λ = ln φ, κ = φ. -/
  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.
  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.