reach_le_in_ball
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume reflexivity, symmetry, or any other property of the step relation.
- Does not extend reachability to infinite steps or continuous limits.
- Does not bound the minimal number of steps required to reach a point.
- Does not address reverse reachability or cone closure properties.
formal statement (Lean)
21lemma reach_le_in_ball {K : Kinematics α} {x y : α} {k n : Nat}
22 (hk : k ≤ n) (h : ReachN K k x y) : inBall K x n y := ⟨k, hk, h⟩
proof body
23