stationary_at_any

formal source

  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