lemma
proved
zeroWidthCert_valid
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Recognition.Certification on GitHub at line 116.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
113, eps := fun _ => 0
114, eps_nonneg := by intro _; norm_num }
115
116lemma zeroWidthCert_valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) :
117 Valid Z Fgap (zeroWidthCert Z Fgap) := by
118 refine {
119 M0_pos := by simp [zeroWidthCert]
120 , Fgap_in := by
121 intro i
122 dsimp [zeroWidthCert, Igap, memI]
123 constructor <;> linarith
124 , Ires_in_Igap := by
125 intro i
126 dsimp [zeroWidthCert, Igap]
127 constructor <;> linarith
128 }
129
130/-- Exact anchor identity from a zero-width certificate. -/
131lemma anchorIdentity_of_zeroWidthCert {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ)
132 (res : Species → ℝ) (hres : ∀ i, memI ((zeroWidthCert Z Fgap).Ires i) (res i)) :
133 ∀ i : Species, res i = Fgap (Z i) := by
134 intro i
135 have h := hres i
136 dsimp [zeroWidthCert, memI] at h
137 exact le_antisymm h.2 h.1
138
139end
140
141end Certification
142end Recognition
143end IndisputableMonolith