reach_le_in_ball
plain-language theorem explainer
Reachability in exactly k steps from x to y under a kinematics step relation implies y belongs to the n-ball around x for any n at least k. Workers on discrete causal models cite it when embedding finite paths into radius bounds. The proof is a direct construction of the existential witness from the reachability hypothesis and the inequality.
Claim. Let $K$ be a kinematics structure on a type with step relation. If $k$ steps reach from $x$ to $y$ and $k$ is at most $n$, then $y$ lies in the ball of radius $n$ around $x$, where the ball is the set of all points reachable in at most $n$ steps via the inductive closure of the step relation.
background
Kinematics on a type α is the structure whose only field is a binary step relation α → α → Prop. ReachN K n x y is the inductive predicate that holds for n = 0 precisely when x = y and extends by one application of the step relation at each successor. inBall K x n y is the existential statement that some k ≤ n satisfies ReachN K k x y.
proof idea
One-line wrapper that applies the definition of inBall by packaging the given k, the inequality hk, and the ReachN hypothesis h into the existential constructor.
why it matters
The lemma is referenced from the Reach module to support monotonicity of balls under increasing radii. It supplies the elementary inclusion of shorter paths inside larger balls, a prerequisite for bounding causal propagation in the discrete kinematics setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.