`Z`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.AnchorPolicyCertified
domain: Physics
line: 41 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.AnchorPolicyCertified on GitHub at line 41.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  38
  39abbrev Species : Type := Fermion
  40
  41abbrev Z (f : Species) : Int := ZOf f
  42
  43abbrev Fgap (z : Int) : ℝ := gap z
  44
  45/-! ## Main certified consequences -/
  46
  47/-- If an external certificate bounds the per-species residues at the anchor, then every species'
  48residue is close to the closed-form display `gap(Z)` (inequality form). -/
  49theorem anchor_identity_from_cert
  50    (C : AnchorCert Species)
  51    (hC : Valid Z Fgap C)
  52    (resAtAnchor : Species → ℝ)
  53    (hres : ∀ f, memI (C.Ires f) (resAtAnchor f)) :
  54    ∀ f : Species, |resAtAnchor f - Fgap (Z f)| ≤ 2 * C.eps (Z f) := by
  55  -- Directly reuse the generic lemma.
  56  simpa [Species, Z, Fgap] using
  57    (anchorIdentity_cert (Z := Z) (Fgap := Fgap) (C := C) hC resAtAnchor hres)
  58
  59/-- Equal-Z degeneracy bound from a certificate: if two species share the same Z, their residues
  60must lie within the certified band. -/
  61theorem equalZ_residue_from_cert
  62    (C : AnchorCert Species)
  63    (hC : Valid Z Fgap C)
  64    (resAtAnchor : Species → ℝ)
  65    (hres : ∀ f, memI (C.Ires f) (resAtAnchor f))
  66    {f g : Species} (hZ : Z f = Z g) :
  67    |resAtAnchor f - resAtAnchor g| ≤ 2 * C.eps (Z f) := by
  68  simpa [Species, Z, Fgap] using
  69    (equalZ_residue_of_cert (Z := Z) (Fgap := Fgap) (C := C) hC resAtAnchor hres hZ)
  70
  71end

papers checked against this theorem

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