preserves_predicate
plain-language theorem explainer
A predicate closed under a deterministic step is preserved along the reflexive-transitive closure of that step. Anyone working the echo-horizon obstruction cites this as the combinatorial one-way boundary fact: reachability cannot escape a step-closed set. The proof is a one-line application of the universal property that defines reachability.
Claim. Let $X$ be a type and $s:X\to X$ a step map. If $P:X\to\mathrm{Prop}$ is closed under $s$ (i.e. $P(x)\Rightarrow P(s(x))$ for all $x$), then for any $p,q\in X$ with $q$ reachable from $p$ by zero or more applications of $s$, one has $P(p)\Rightarrow P(q)$.
background
The module builds an abstract causal model of an event horizon as a one-way boundary. Points carry a future-directed step map; the interior is required to be closed under that step. The rejected bounce-echo story needs a signal to enter the interior, bounce, and return to the same exterior, which the one-way axiom forbids on purely combinatorial grounds.
Reachability is packaged as the reflexive-transitive closure of the step: $q$ is reachable from $p$ when every predicate closed under the step that holds at $p$ also holds at $q$. That universal-property definition is the only upstream content this lemma needs; it does not depend on Lorentzian geometry or on any concrete manifold structure.
The local setting is deliberately thin: an abstract type of points and a function, not a full causal spacetime. The combinatorial claim is that a set closed under a map cannot meet its complement by iterated application of the map.
proof idea
One-line term proof. After introducing the endpoints and the reachability hypothesis, apply that hypothesis (the universal property of the reflexive-transitive closure) to the given predicate and the given closure assumption. No induction or auxiliary lemmas are required; the statement is essentially the defining elimination rule for reachability.
why it matters
This is the combinatorial heart of the one-way boundary used throughout the echo-horizon obstruction. Downstream siblings (exterior-return impossibility, violation of horizon causality, and the status flag that records rejection of the bounce-echo mechanism) rest on the fact that an interior predicate closed under future step cannot be escaped by any finite chain of steps. The module abstract justifies the rejection recorded in the companion bounce-echo module: any exterior-return claim with an interior bounce is causally forbidden once the interior is step-closed.
In the broader Recognition gravity stack this is scaffolding for ruling out a class of horizon-echo proposals without committing to full GR geometry. It is not itself a forcing-chain landmark (T0–T8), but it polices which bounce stories are allowed once the causal model is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.