reach_in_ball
plain-language theorem explainer
The lemma shows that exact n-step reachability under a kinematics step relation implies membership in the corresponding n-ball. Researchers modeling discrete causal propagation cite it to connect precise step counts to bounded distance predicates. The proof is a direct term construction supplying the exact count, reflexivity of the order, and the reachability hypothesis to the existential definition of the ball.
Claim. Let $K$ be a kinematics structure on type $α$ with step relation $R$. Suppose $y$ is reachable from $x$ in exactly $n$ steps under the inductive closure of $R$. Then there exists $k ≤ n$ such that $y$ is reachable from $x$ in exactly $k$ steps.
background
The Causality.Basic module defines a Kinematics structure on a type $α$ as a record containing only a binary step relation. ReachN is the inductive predicate for exact reachability: the zero constructor gives reflexivity at zero steps, while the successor constructor extends a reachability fact by one application of the step. The inBall predicate is the existential packaging of ReachN, asserting existence of some $k ≤ n$ satisfying the exact reachability.
proof idea
This is a one-line term-mode wrapper. It constructs the witness for the existential in the definition of inBall by taking the exact count $n$, the reflexivity proof le_rfl for the inequality $n ≤ n$, and the supplied ReachN hypothesis.
why it matters
The lemma supplies a basic interface fact for reachability in the Causality module and is referenced by the matching declaration in the Reach submodule. It supports development of bounded causal cones by linking exact step counts to at-most-n distance, consistent with the framework's emphasis on finite propagation limits in discrete kinematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.