reach_in_ball
plain-language theorem explainer
Reachability in exactly n steps under a kinematics step relation implies membership in the n-ball. Researchers modeling discrete causal propagation cite this when establishing bounded cones. The argument is a direct witness construction using reflexivity of the natural order.
Claim. Let $K$ be a kinematics structure on a set with step relation. If $y$ is reachable from $x$ in exactly $n$ steps, then there exists $k$ with $k$ at most $n$ such that $y$ is reachable from $x$ in $k$ steps.
background
In the Causality module a Kinematics structure on type α consists solely of a binary step relation. ReachN is the inductive predicate with zero-step reflexivity at the same point and successor steps that increment the count by one. inBall relaxes the exact count to an existential bound of at most n steps.
proof idea
One-line wrapper that applies the definition of inBall by exhibiting n as the witness, using le_rfl for the inequality and the supplied ReachN hypothesis directly.
why it matters
The lemma feeds the identically named declaration in the Basic module and supplies the basic inclusion needed for cone-bound arguments. It forms part of the causal layer that precedes the forcing chain landmarks T5 through T8 and the introduction of phi-based constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.