module module

`IndisputableMonolith.Recognition.Certification`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.AnchorPolicyCertified module_import

declarations in this module (13)

structure Interval L11
def memI L16
def width L18
lemma abs_sub_le_width_of_memI L21
structure AnchorCert L36
def Igap L43
structure Valid L49
lemma M0_pos_of_cert L55
lemma anchorIdentity_cert L60
lemma equalZ_residue_of_cert L81
def zeroWidthCert L109
lemma zeroWidthCert_valid L116
lemma anchorIdentity_of_zeroWidthCert L131