CausalModel
plain-language theorem explainer
Abstract causal model of a one-way event horizon: a point type, a deterministic future step, interior/exterior predicates, and the axiom that interior is closed under the step. Anyone arguing that bounce-echo black-hole signals are causally forbidden cites this carrier. It is a pure structure definition; no proof body.
Claim. A causal model consists of a point type $X$, a future-directed step $s: X\to X$, predicates $\mathrm{Int}$, $\mathrm{Ext}$, $\mathrm{Int}_{\mathrm{strict}}$ on $X$, a same-exterior-region relation, the implication $\mathrm{Int}_{\mathrm{strict}}\Rightarrow\mathrm{Int}$, the one-way boundary axiom $\mathrm{Int}(p)\Rightarrow\mathrm{Int}(s(p))$, and disjointness $\mathrm{Ext}\cap\mathrm{Int}=\emptyset$.
background
The module Echo Horizon Obstruction rejects the bounce-echo mechanism from BlackHoleEchoesFromBounce. That mechanism needed a signal to cross into the horizon, bounce at a microscopic radius strictly inside, and return to the same exterior. The module encodes the obstruction combinatorially: a set closed under a function cannot reach its complement by iterating that function.
The companion reachability relation is the reflexive-transitive closure of the step: $q$ is reachable from $p$ if every predicate closed under the step that holds at $p$ also holds at $q$. The model is deliberately not Lorentzian geometry; only the one-way boundary matters.
Local setting: interior closed under future step means once inside, always inside. No interior point can causally reach an exterior point.
proof idea
Definition only: a structure bundling the point type, step map, region predicates, and three axioms (strict-interior implies interior; interior closed under step; exterior and interior disjoint). No proof tactics. Downstream theorems instantiate this carrier and apply the closure axiom along StepStar chains from the bounce point to the claimed return point.
why it matters
This is the ambient type for the module's main results. ExteriorReturnClaim is parameterized by a CausalModel. The main theorem bounce_echo_mechanism_violates_horizon_causality states that any such claim forces the return point to be both interior (by one-way closure from a strictly interior bounce) and exterior (by the return fact), i.e. ViolatesHorizonCausality. The corollary exterior_return_claim_impossible derives False from disjointness.
That obstruction justifies blackHoleEchoMechanismStatus recording bounce_escape_mechanism_rejected. In the broader RS gravity story it separates admissible echo phenomenology from mechanisms that would reverse a classical horizon. It is combinatorial scaffolding for the rejection, not a derivation of horizons from the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.