f_residue_model

formal source

  33/-- A computable stand-in for the RG residue: constant in scale and equal to the display `gap(Z)`.
  34
  35This encodes the single-anchor closed form as a *definition* rather than a phenomenology axiom. -/
  36noncomputable def f_residue_model (f : Fermion) (_mu : ℝ) : ℝ :=
  37  gap (ZOf f)
  38
  39@[simp] theorem f_residue_model_at (f : Fermion) (mu : ℝ) :
  40    f_residue_model f mu = gap (ZOf f) := rfl
  41
  42/-! ## Consequences (stationarity/robustness become trivial in the model) -/
  43
  44/-- In the model, the residue is constant in `t`, hence stationary at every point. -/
  45theorem stationary_at_any (muStar : ℝ) (f : Fermion) :
  46    deriv (fun t => f_residue_model f (Real.exp t)) (Real.log muStar) = 0 := by
  47  -- `f_residue_model` ignores its scale argument, so the function of `t` is constant.
  48  simp [f_residue_model]
  49
  50/-- In the model, the second derivative is also identically zero, hence bounded. -/
  51theorem stability_bound_at_any (muStar : ℝ) :
  52    ∃ (ε : ℝ), 0 < ε ∧ ∀ (f : Fermion),
  53      |deriv (deriv (fun t => f_residue_model f (Real.exp t))) (Real.log muStar)| < ε := by
  54  refine ⟨1, by norm_num, ?_⟩
  55  intro f
  56  -- Second derivative of a constant is 0.
  57  simp [f_residue_model]
  58
  59/-- Equal-Z degeneracy holds by definition in the model. -/
  60theorem equalZ_at_any {f g : Fermion} (hZ : ZOf f = ZOf g) (mu : ℝ) :
  61    f_residue_model f mu = f_residue_model g mu := by
  62  simp [f_residue_model, hZ]
  63
  64end AnchorPolicyModel
  65end IndisputableMonolith.Physics