module module

`IndisputableMonolith.Gravity.EchoHorizonObstruction`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce module_import

declarations in this module (11)

def StepStar L44
lemma base L50
lemma succ L56
lemma preserves_predicate L65
lemma trans L72
structure CausalModel L89
structure ExteriorReturnClaim L126
def ViolatesHorizonCausality L155
theorem bounce_echo_mechanism_violates_horizon_causality L169
theorem exterior_return_claim_impossible L185
theorem blackHoleEchoMechanismStatus_records_rejection L192