succ
plain-language theorem explainer
If a point q is reachable from p under iterated applications of a deterministic step map, then the one-step image of q is also reachable from p. Anyone building the one-way horizon obstruction from the universal property of reflexive-transitive closure cites this successor case. The proof is a short term argument: apply the closed predicate at q, then push it one step forward.
Claim. Let $s : X \to X$ be a step map on a type $X$, and write $p \leadsto_s q$ for the reflexive-transitive reachability relation (any $s$-closed predicate true at $p$ is true at $q$). Then $p \leadsto_s q$ implies $p \leadsto_s s(q)$.
background
The module formalizes a purely combinatorial obstruction to bounce-echo mechanisms at event horizons. An exterior-return claim would require a signal to cross into the interior, bounce at a microscopic interior radius, and reappear in the same exterior region. The model treats the future-directed evolution as a deterministic step map on an abstract point set, with the interior as a set closed under that step.
Reachability is packaged as StepStar: $q$ is reachable from $p$ when every predicate closed under the step that holds at $p$ also holds at $q$. That is the universal property of the reflexive-transitive closure, not an inductive datatype. The base case says every point reaches itself; this successor lemma extends a reachability witness by one application of the step.
The obstruction is combinatorial: a set closed under a function cannot reach its complement by iterated application. Full Lorentzian geometry is not formalized here.
proof idea
Unfold the universal-property definition of reachability. Fix an arbitrary predicate $P$ closed under the step and assume $P$ holds at $p$. The hypothesis that $q$ is reachable from $p$ yields $P(q)$. Closure of $P$ under the step then yields $P(s(q))$. Since $P$ was arbitrary, $s(q)$ is reachable from $p$. No external lemmas are required beyond the definition.
why it matters
This is the inductive step that makes iterated future evolution usable inside the echo-horizon argument. Together with the base case and the preservation lemma (any step-closed predicate is invariant along reachability), it underwrites the claim that interior points stay interior, so no bounce-to-exterior return path exists under the one-way boundary axiom.
Downstream, that feeds ExteriorReturnClaim impossibility and the status flag that records rejection of the bounce-echo mechanism in BlackHoleEchoesFromBounce. The same successor pattern appears throughout the causality stack (finite reachability balls and light-cone bounds), where one-step extension of paths is the basic generator. Within Recognition Science this is scaffolding for the gravity side of the ledger, not a forcing-chain (T0–T8) landmark; it closes a concrete causal gap rather than deriving a constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.