ReachN
plain-language theorem explainer
ReachN encodes exact n-step reachability via the step relation of a kinematics structure. It is referenced in proofs of ball membership and reachability lemmas throughout the Causality hierarchy. The inductive definition uses a zero base case together with a successor rule that composes one additional transition.
Claim. For a kinematics structure $K$ on a type $α$ equipped with a binary step relation, the predicate ReachN$(K,n,x,y)$ asserts the existence of an exact chain of $n$ transitions from $x$ to $y$ under that relation, defined by the base case of zero steps when the points coincide and the inductive step that appends one transition.
background
Kinematics $α$ is the structure consisting solely of a binary step relation on $α$. ReachN is the inductive definition of finite-step reachability built directly from that relation. The same inductive appears in upstream modules Causality.Basic and Causality.Reach, where it supplies the core relation for inBall and Reaches. The local setting is the discrete causal model employed to derive cone bounds and propagation properties in Recognition Science.
proof idea
This is an inductive definition. It is introduced by the zero constructor for the base case of zero steps and the succ constructor that extends a reachability of $n$ steps by one additional step via the step relation.
why it matters
This declaration supplies the core reachability relation used by downstream results such as reaches_of_reachN, reach_in_ball, and ballP_subset_inBall. It supports uniqueness arguments by formalizing finite-step propagation. In the Recognition framework it underpins causal cone bounds and discrete time evolution in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.