recognition / Physics / Physics.AnchorPolicyModel / equalZ_at_any

theorem

`equalZ_at_any`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.AnchorPolicyModel on GitHub at line 60.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

formal source

  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.