AnchorSpec

formal source

  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.
  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. -/
  90noncomputable def canonicalAnchor : AnchorSpec where
  91  muStar := 182.201
  92  muStar_pos := by norm_num
  93  lambda := Real.log phi
  94  kappa := phi
  95  equalWeight := True  -- Placeholder; the actual condition is checked numerically
  96
  97/-! ## Z-Map (for reference; aligns with RSBridge.ZOf) -/
  98
  99/-- Canonical Z bands used in papers.
 100    - 24:   down quarks (Q = -1/3, 6Q = -2)
 101    - 276:  up quarks   (Q = +2/3, 6Q = +4)