reach_mem_ballP
plain-language theorem explainer
Reachability in exactly n steps under a kinematics step relation implies membership in the n-ball defined by iterated steps. Researchers modeling discrete causal structures cite this to connect exact path lengths to bounded reachability predicates. The proof proceeds by induction on the ReachN derivation, with the zero case immediate by definition and the successor case using the right disjunct of the ballP clause.
Claim. Let $K$ be a kinematics structure on a set $α$ with binary step relation. If $y$ is reachable from $x$ by a path of exactly $n$ steps under the ReachN predicate, then $y$ lies in the ball of radius $n$ around $x$ under the ballP predicate.
background
Kinematics is the structure consisting of a type $α$ equipped with a binary step relation. ReachN is the inductive predicate for paths of exact length $n$: the zero constructor gives ReachN $K$ 0 $x$ $x$, while the successor adds one step via $K$.step. ballP is the recursive predicate for points reachable in at most $n$ steps, with base case equality at radius 0 and successor clause given by disjunction with an existential step from a prior ball point.
proof idea
The proof is by induction on the ReachN hypothesis. The zero case simplifies directly to the base clause of ballP. The successor case applies the inductive hypothesis to place the intermediate point in the prior ball, then invokes the right disjunct of the ballP successor definition together with the final step.
why it matters
This lemma is invoked inside the proofs of inBall_subset_ballP in both the BallP and Reach modules, where it converts an exact ReachN path into ballP membership before applying monotonicity. It supports the construction of causal balls and cone bounds within the Recognition Science causality layer, bridging exact path counts to the inductive ball predicate used for reachability arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.