reach_mem_ballP
plain-language theorem explainer
The lemma shows that any chain of exactly n steps under a kinematics step relation places the endpoint inside the n-ball of the ball predicate. Researchers formalizing discrete causal neighborhoods cite it to convert inductive reachability into bounded-ball membership. The proof is by induction on the ReachN constructor, with the zero case simplifying directly and the successor case feeding the inductive hypothesis into the existential clause of ballP.
Claim. Let $K$ be a kinematics structure on a type $α$ with step relation. For all $x,y∈α$ and all natural numbers $n$, if $y$ is reachable from $x$ in exactly $n$ steps via the inductive ReachN predicate, then $y$ lies in the ball of radius $n$ centered at $x$ under the recursively defined ballP predicate.
background
A Kinematics structure on a type $α$ consists solely of a binary step relation. ReachN is the inductive predicate for exact-distance reachability: the zero constructor gives reflexivity at distance 0, and the successor constructor prepends one additional step. The ballP predicate is defined recursively to capture all points at distance at most $n$: radius 0 requires equality to the center, while the successor clause includes any point already in the prior ball or any point reached by a step from a point in the prior ball.
proof idea
The proof is by induction on the ReachN hypothesis. The zero case reduces immediately by simplification against the base clause of ballP. The successor case applies the inductive hypothesis to obtain membership of the intermediate point in the radius-n ball, then uses the final step to witness the existential disjunct in the successor clause of ballP.
why it matters
This lemma is invoked inside inBall_subset_ballP (both in BallP and Reach modules) to convert reachability data into ball membership before applying monotonicity. It supplies the basic bridge between exact inductive reachability and the at-most-n ball predicate, supporting the broader development of causal cones and bounded neighborhoods in the Causality section. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.