F_eq_gap

formal source

  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.
  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