ballP
plain-language theorem explainer
ballP defines the predicate for points reachable from a center x in at most n steps under a kinematics step relation K on type alpha. Discrete causality researchers cite it when deriving growth bounds for reachable sets in bounded-degree graphs. The definition is supplied by direct recursion on the radius, with base case equality and successor case adjoining one step.
Claim. Let $K$ be a kinematics structure on type $alpha$ with step relation. For $x in alpha$ the predicate $ballP(K,x,n,y)$ holds if $y=x$ when $n=0$, and otherwise if $y$ lies in the ball of radius $n-1$ or is reached by one step from some point in that ball.
background
The ConeBound module supplies minimal local definitions to obtain ball growth bounds under bounded-degree step relations while avoiding heavy imports. Kinematics is the structure consisting solely of a step relation on alpha. BoundedStep is the class that adds a neighbors map to finite sets together with the axiom that every point has at most d neighbors and that step holds exactly on those neighbors.
proof idea
The definition is given by pattern matching on the natural-number radius. Radius zero returns equality to the center. The successor clause unions the previous ball with the image of that ball under the step relation of K.
why it matters
This definition supplies the core reachability predicate invoked by ballP_mono, ballP_subset_inBall, inBall_subset_ballP and the equivalence mem_ballFS_iff_ballP. It supports the construction of causal cones under bounded step relations and feeds the cardinality bounds developed in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.