ballP
plain-language theorem explainer
ballP defines the predicate asserting that y lies within n steps of x under the step relation of a kinematics structure K. Workers on causal structure and discrete propagation cite it to bound reachability in step graphs. The definition is supplied directly by recursion on n with base case equality and successor clause using existential quantification over one step.
Claim. Let $K$ be a kinematics structure on type $α$ whose sole field is the relation $K.step : α → α → Prop$. The predicate $ballP(K,x,n,y)$ holds precisely when $y=x$ for $n=0$, and when $ballP(K,x,n,y)$ or there exists $z$ with $ballP(K,x,n,z)$ and $K.step(z,y)$ for $n+1$.
background
Kinematics, imported from Causality.Basic, is the structure whose single field step encodes allowed local transitions. The BallP module supplies the finite-horizon ball predicate built from this relation. Parallel recursive definitions of the same shape appear in the ConeBound and Reach modules, each using the identical base and successor clauses.
proof idea
The declaration is a direct recursive definition. Base case equates the zero-ball to the singleton at x. Successor case forms the disjunction of the n-ball with the image of the n-ball under one application of step.
why it matters
ballP is the primitive object from which monotonicity (ballP_mono), equivalence to inBall (ballP_subset_inBall, inBall_subset_ballP), and reachability membership (reach_mem_ballP) are derived. It is reused verbatim in ConeBound to equate membership in ballFS with the step-ball predicate, supplying the discrete causal-cone construction required for later bounds on propagation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.