`stability_bound_at_any`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.AnchorPolicyModel
domain: Physics
line: 51 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.AnchorPolicyModel on GitHub at line 51.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.