module module

`IndisputableMonolith.Gravity.BlackHoleEchoesSI`

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.MasterTheorem module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.SIBridgeClosure module_import
IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce module_import

declarations in this module (27)

def planckTime_SI L82
def planckLength_SI L85
theorem planckTime_SI_pos L87
theorem planckLength_SI_pos L92
theorem planckTime_SI_sq L98
theorem planckLength_SI_sq L105
theorem planckLength_SI_eq_planckTime_mul_c L112
def bounceRadius_SI L130
theorem bounceRadius_SI_pos L132
theorem bounceRadius_SI_two_step L136
theorem bounceRadius_SI_strict_mono L142
def echoDelay_SI L154
theorem echoDelay_SI_def L157
theorem echoDelay_SI_eq_planckTime_form L162
theorem echoDelay_SI_pos L169
theorem echoDelay_SI_two_step L177
theorem echoDelay_SI_strict_mono L183
theorem echoDelay_SI_sq L207
def echoDampingRatio_SI L224
theorem echoDampingRatio_SI_eq L226
theorem echoDampingRatio_SI_pos L228
theorem echoDampingRatio_SI_lt_one L231
theorem echoDampingRatio_SI_band L234
structure BlackHoleEchoesSICert L240
def blackHoleEchoesSICert L269
theorem blackHoleEchoesSICert_inhabited L286
theorem black_hole_echoes_SI_one_statement L294