trans
plain-language theorem explainer
Reachability under iterated application of a deterministic step is transitive: if q is reachable from p and r from q, then r is reachable from p. Anyone chaining causal steps in the abstract one-way horizon model cites this. The proof is a short composition of the two universal-property witnesses for the reflexive-transitive closure.
Claim. Let $s : X \to X$ be a deterministic step on a point set $X$. Write $p \rightsquigarrow_s q$ when every predicate closed under $s$ that holds at $p$ also holds at $q$ (reflexive-transitive reachability). If $p \rightsquigarrow_s q$ and $q \rightsquigarrow_s r$, then $p \rightsquigarrow_s r$.
background
The module encodes a combinatorial causal obstruction to bounce-echo mechanisms for black holes. An event horizon is treated as a one-way boundary: the interior predicate is closed under the future-directed step, so once inside, always inside. No interior point can reach an exterior point by iterated stepping.
Reachability is the reflexive-transitive closure of a deterministic map $s$, defined by its universal property: $q$ is reachable from $p$ when every $s$-closed predicate true at $p$ is true at $q$. Base and successor cases live in the same namespace; this lemma is the composition law for those chains.
The setting is deliberately abstract, not a formalization of Lorentzian geometry. As the module states, the obstruction is purely combinatorial: a set closed under a function cannot reach its complement via iterated application of that function.
proof idea
Unfold the universal-property definition of reachability. Fix an arbitrary predicate $P$ closed under the step and assume $P$ holds at $p$. Apply the first hypothesis to obtain $P$ at $q$, then feed that into the second hypothesis to obtain $P$ at $r$. The tactic body is three lines: intros on $P$, its closure, and the base fact; then exact composition of the two witnesses. No induction or path construction is needed.
why it matters
Transitivity is the composition law for causal reachability in the abstract horizon model. Sibling results that reject exterior return after an interior bounce (the exterior-return impossibility and the bounce-echo causality violation) treat multi-step interior paths as single reachability facts; this lemma is the glue that makes those chains well-defined.
The parent module supplies the formal obstruction behind the recorded rejection of the bounce-escape mechanism in the black-hole echoes development: any claim that a signal enters the interior, bounces strictly inside the horizon, and returns to the same exterior region contradicts the one-way boundary axiom. The argument stays combinatorial and does not invoke full GR causality structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.