ballP
plain-language theorem explainer
ballP defines the n-step reachability predicate for a kinematics structure K on type α, with x as origin. Researchers modeling causal propagation and cone bounds cite this inductive predicate to establish finite-step closure under the step relation. The definition is given directly by recursion on n, with base case equality and successor case via disjunction and existential quantification over one step.
Claim. Let $K$ be a kinematics structure on type $α$ whose single field is a binary relation step. Define the predicate $B_n(y)$ recursively by $B_0(y) ⇔ y = x$ and $B_{n+1}(y) ⇔ B_n(y) ∨ ∃ z (B_n(z) ∧ step(z,y))$.
background
Kinematics is the structure with field step : α → α → Prop that encodes allowed one-step transitions in a causal model. The predicate ballP K x n y asserts that y lies within at most n applications of step starting from x. Equivalent definitions appear in the sibling BallP and ConeBound modules, where upstream doc-comments state that ballP K x n y means y is within ≤ n steps of x via K.step.
proof idea
The definition is supplied by pattern matching on the natural number argument. The zero case reduces to equality with the origin. The successor case forms the disjunction of the n-ball with the existential closure under a single application of K.step.
why it matters
This supplies the core inductive reachability predicate used by downstream results including ballP_mono for monotonicity in n, ballP_subset_inBall and inBall_subset_ballP for equivalence with inBall, and reach_mem_ballP for connection to ReachN. It supports construction of causal cones and propagation bounds in the causality domain, consistent with the framework's discrete-step kinematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.