ballP_mono
plain-language theorem explainer
Monotonicity of ballP asserts that for kinematics K on type α, point x, and naturals n ≤ m, the set of points reachable from x in at most n steps via the step relation is contained in the set reachable in at most m steps. Researchers formalizing discrete causal propagation would cite this when lifting radius bounds between reachability predicates. The proof is by induction on the inequality n ≤ m, with the successor case using the left disjunct in the recursive clause of ballP.
Claim. Let $K$ be a kinematics structure on type $α$ with binary step relation. For $x ∈ α$ and natural numbers $n ≤ m$, the set $ { y | ballP(K, x, n, y) } $ is contained in $ { y | ballP(K, x, m, y) } $, where ballP(K, x, k, y) holds precisely when y is reachable from x in at most k steps.
background
Kinematics is the structure consisting of a single binary step relation on the carrier type α. The predicate ballP K x n y is defined by recursion on n: it equals the equality predicate y = x when n = 0, and for successor n it is the disjunction of ballP at the predecessor together with the existence of an intermediate z reachable in the predecessor steps such that the step relation holds from z to y. The same recursive definition appears in the sibling BallP and ConeBound modules. This lemma sits inside the Causality.Reach module whose focus is relating several notions of finite-step reachability.
proof idea
Proof by induction on the hypothesis hnm : n ≤ m. The reflexive case reduces to set equality and is discharged by simpa. In the successor step case the inductive hypothesis supplies inclusion into the m-ball; the definition of ballP at m+1 then includes that m-ball as the left disjunct of the or, so the inclusion lifts directly.
why it matters
The lemma is invoked inside inBall_subset_ballP (both in BallP and Reach) to raise the witness radius k to the target n after applying reach_mem_ballP. It therefore closes the gap between the reachability predicate Reaches and the ballP predicate used for cone bounds. In the Recognition Science setting this monotonicity is a prerequisite for constructing causal cones and for any argument that enlarges a finite propagation distance while preserving membership.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.