base
plain-language theorem explainer
Every point is reachable from itself under the reflexive-transitive closure of a deterministic step. Anyone building the abstract causal model for horizon obstruction cites this as the zero-step case of reachability. The proof is immediate from the universal-property definition: the target predicate already holds at the starting point.
Claim. For any type of points, any step map $s$, and any point $p$, one has $\mathrm{Step}^*\!\!(s,p,p)$: $p$ is reachable from itself in zero applications of $s$.
background
The module builds an abstract causal obstruction to bounce-echo mechanisms at event horizons. An exterior-return claim would require a signal to enter the interior, bounce, and reappear in the same exterior region. The obstruction is combinatorial: a set closed under a future-directed step cannot reach its complement by iterating that step.
Reachability is packaged as StepStar: $q$ is reachable from $p$ under $s$ when every predicate closed under $s$ that holds at $p$ also holds at $q$. That is the standard universal-property encoding of the reflexive-transitive closure of a deterministic step, not a path-list construction.
The local setting is deliberately not full Lorentzian geometry. It only needs a one-way boundary axiom (interior closed under the step) plus this reachability relation, so that any claimed exterior return after an interior bounce is formally forbidden.
proof idea
Unfold the universal-property definition of reachability. After introducing an arbitrary step-closed predicate $P$ and the hypotheses that $P$ is closed under the step and that $P$ holds at $p$, the goal is exactly $P,p$, which is the given hypothesis. No induction and no appeal to the successor lemma are required; this is pure reflexivity of the closure.
why it matters
Reflexivity is the base brick of the reachability relation used throughout the echo-horizon obstruction. Successor and transitivity lemmas sit beside it; together they support the causal model, the exterior-return claim, and the theorems that any such claim violates horizon causality and that the bounce-echo mechanism is rejected.
That rejection is what justifies the status flag in BlackHoleEchoesFromBounce (bounce_escape_mechanism_rejected). In the broader Recognition gravity stack, the point is negative but sharp: interior bounce cannot supply exterior gravitational-wave echoes under a one-way horizon axiom. Downstream certificates elsewhere that mention a generic base name are incidental name collisions; the scientific parent chain is the horizon-causality rejection path in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.