module module

`IndisputableMonolith.Gravity.BHEchoPerEventCatalog`

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.Gravity.BHEchoAmplitudes module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.BHEchoesLIGOCatalog module_import

declarations in this module (12)

inductive HeadlineEvent L41
def predictedRung L50
def predictedBounceRadius L57
def predictedEchoDelay L61
theorem predictedBounceRadius_pos L65
theorem predictedEchoDelay_pos L71
def predictedEchoFrequency L77
theorem predictedEchoFrequency_pos L80
theorem event_count L86
theorem rung_ordering L90
structure BHEchoCatalogCert L96
def bhEchoCatalogCert L107