  57  hC.M0_pos
  58
  59/-- Certificate replacement for the anchor identity (inequality form). -/
  60lemma anchorIdentity_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  61    {C : AnchorCert Species} (hC : Valid Z Fgap C)
  62  (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i)) :
  63  ∀ i : Species, |res i - Fgap (Z i)| ≤ 2 * C.eps (Z i) := by
  64  intro i
  65  have hF : memI (Igap C (Z i)) (Fgap (Z i)) := hC.Fgap_in i
  66  have hI : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
  67    hC.Ires_in_Igap i
  68  have hr : memI (Igap C (Z i)) (res i) := by
  69    have hr0 := hres i
  70    refine ⟨le_trans hI.1 hr0.1, le_trans hr0.2 hI.2⟩
  71  have hbound :=
  72    abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := Fgap (Z i)) hr hF
  73  -- width(Igap) = 2*eps
  74  have hw :
  75      width (Igap C (Z i)) = 2 * C.eps (Z i) := by
  76    simp [Igap, width]
  77    ring
  78  simpa [hw, two_mul] using hbound
  79
  80/-- Equal‑Z degeneracy (inequality form) from a certificate. -/
  81lemma equalZ_residue_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  82    {C : AnchorCert Species} (hC : Valid Z Fgap C)
  83  (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i))
  84  {i j : Species} (hZ : Z i = Z j) :
  85  |res i - res j| ≤ 2 * C.eps (Z i) := by
  86  have hI_i : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
  87    hC.Ires_in_Igap i
  88  have hI_j : (Igap C (Z j)).lo ≤ (C.Ires j).lo ∧ (C.Ires j).hi ≤ (Igap C (Z j)).hi :=
  89    hC.Ires_in_Igap j
  90  have hres_i : memI (Igap C (Z i)) (res i) := by

papers checked against this theorem

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