inBall_subset_ballP
plain-language theorem explainer
The inclusion shows that existential bounded reachability under a kinematics step relation implies membership in the corresponding inductive ball. Researchers formalizing discrete causal cones cite it to move properties between the two ball predicates. The term proof extracts the witness count, converts exact reachability to the inductive form, and lifts the bound by monotonicity.
Claim. Let $K$ be a kinematics structure on type $α$ (i.e., a binary step relation). For points $x,y∈α$ and natural number $n$, if there exists $k≤n$ such that $y$ is reachable from $x$ in exactly $k$ steps, then $y$ belongs to the $n$-ball around $x$ under the inductive closure of the step relation.
background
Kinematics $α$ is the structure whose only field is a binary step relation on $α$. The existential predicate holds precisely when a witness $k≤n$ exists together with exact $k$-step reachability. The inductive predicate is defined by recursion on the bound: it holds at level 0 exactly when the points coincide, and at successor level when it holds at the predecessor or an intermediate point is connected by one step.
proof idea
The term proof introduces the witness triple consisting of the step count $k$, the inequality $k≤n$, and the exact reachability fact. It applies the conversion lemma that turns exact reachability into inductive membership at level $k$, then composes with the monotonicity lemma that enlarges the ball when the bound is increased, and returns the resulting membership at level $n$.
why it matters
The lemma supplies the inclusion that lets inductive properties transfer to the existential formulation inside the causality development. It is invoked by the corresponding statement in the BallP module and thereby supports all subsequent cone-bound and reachability arguments that rely on the inductive ball predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.