muStar

formal source

 250/-! ## Anchor Relation -/
 251
 252/-- The anchor scale from the papers: μ⋆ = 182.201 GeV. -/
 253def muStar : ℝ := 182.201
 254
 255theorem muStar_pos : muStar > 0 := by norm_num [muStar]
 256
 257/-- ln(μ⋆) for use in integral bounds. -/
 258def lnMuStar : ℝ := Real.log muStar
 259
 260/-- The residue at the anchor, relative to a reference ln-scale.
 261
 262    `f_i(μ⋆, μ_ref) := (1/λ) ∫_{ln μ⋆}^{lnμ_ref} γ_i(exp(t)) dt`
 263
 264    This is what the axiom `f_residue` in `AnchorPolicy.lean` is intended to represent. -/
 265def residueAtAnchor (γ : AnomalousDimension) (f : Fermion) (lnμ_ref : ℝ) : ℝ :=
 266  integratedResidue γ f lnMuStar lnμ_ref
 267
 268/-- The claim of Single Anchor Phenomenology: at the anchor scale μ⋆, the residue
 269    equals the closed-form display F(Z).
 270
 271    `residueAtAnchor γ f (ln m_phys) ≈ gap(ZOf f)`
 272
 273    This is what `display_identity_at_anchor` in `AnchorPolicy.lean` asserts. -/
 274def anchorClaimHolds (γ : AnomalousDimension) (tolerance : ℝ) : Prop :=
 275  ∀ (f : Fermion) (lnμ_ref : ℝ),
 276    |residueAtAnchor γ f lnμ_ref - gap (ZOf f)| < tolerance
 277
 278/-! ## Stationarity at the Anchor -/
 279
 280/-- The derivative of the residue with respect to the upper integration limit.
 281    This equals (1/λ) · γ(exp(lnμ)) = (1/λ) · γ(μ) by the fundamental theorem of calculus.
 282
 283    Stationarity of the residue at μ⋆ means this vanishes, i.e., γ(μ⋆) = 0. -/