module module

`IndisputableMonolith.Verification.GWTC3PosteriorManifest`

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.Verification.GWTC3RingdownZipSchema module_import

declarations in this module (21)

structure PosteriorFile L42
def zenodoRecordId L47
def imrFile L49
def ringdownFile L54
def simFile L59
def livFile L64
def parFile L69
def allPosteriorFiles L74
def HasPositiveSize L79
theorem imr_size_pos L82
theorem ringdown_size_pos L86
theorem sim_size_pos L90
theorem liv_size_pos L94
theorem par_size_pos L98
theorem posterior_manifest_has_five_files L102
theorem posterior_manifest_record_id_pos L107
theorem ringdown_file_key L112
structure GWTC3PosteriorManifestCert L117
def gwtc3PosteriorManifestCert L127
theorem gwtc3PosteriorManifestCert_inhabited L137
theorem gwtc3_posterior_manifest_one_statement L144