inBall
plain-language theorem explainer
The inBall predicate holds for y when it is reachable from x in at most n steps under the step relation of kinematics K. Researchers working on discrete causal cones or bounded propagation in Recognition Science cite it to derive monotonicity and equivalence results for reachability sets. The definition is introduced directly as an existential over the inductive ReachN predicate with no auxiliary lemmas.
Claim. Let $K$ be a kinematics structure on type $α$ with step relation, and let $x,y ∈ α$, $n ∈ ℕ$. The predicate inBall$(K,x,n,y)$ holds if and only if there exists $k ≤ n$ such that ReachN$(K,k,x,y)$.
background
Kinematics is the structure whose sole field is a binary step relation on $α$, encoding one-step causal transitions. ReachN is the inductive predicate for exact-step reachability: it holds at zero steps when the points coincide and extends by one application of the step relation. The Causality.Reach module supplies this definition alongside ReachN and Kinematics to support ball predicates and monotonicity statements.
proof idea
The declaration is a direct definition that unfolds to the existential quantifier over $k ≤ n$ and ReachN. No tactics or lemmas are invoked; it serves as the primitive from which reach_in_ball and reach_le_in_ball are obtained by instantiation.
why it matters
inBall supplies the bounded-reachability predicate used by ballP_subset_inBall and inBall_subset_ballP to establish equivalence with the ballP predicate. It anchors the causal analysis in the Recognition framework by formalizing finite-step propagation, which feeds into cone-bound results and the discrete kinematics underlying the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.