inBall
plain-language theorem explainer
inBall defines y as lying in the causal n-ball around x under a kinematics K precisely when y is reachable from x in at most n steps. Researchers working on discrete causality and cone bounds in Recognition Science cite the predicate to control propagation distances. The definition is a direct existential quantification over the ReachN inductive relation.
Claim. Let $K$ be a kinematics structure on type $α$. For points $x,y ∈ α$ and natural number $n$, $y$ lies in the ball of radius $n$ around $x$ if there exists $k ≤ n$ such that $y$ is reachable from $x$ in exactly $k$ steps under the step relation of $K$.
background
The Kinematics structure on a type $α$ consists of a binary step relation that models single causal transitions. ReachN is the inductive predicate for reachability in a fixed number of steps: the zero constructor identifies a point with itself, and the successor constructor extends reachability by one application of the step relation.
proof idea
The definition is a direct encoding of the bounded existential quantifier over ReachN. No lemmas are applied and no tactics are used; it simply packages the condition $∃ k ≤ n$, ReachN K k x y as the primitive predicate.
why it matters
This predicate underpins the equivalence lemmas ballP_subset_inBall and inBall_subset_ballP that relate it to the ballP predicate. It also supports the monotonicity result inBall_mono and the inclusions reach_in_ball and reach_le_in_ball. In the Recognition framework it supplies the discrete causal ball required for cone bounds and step-count propagation analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.