ballP_mono
plain-language theorem explainer
The monotonicity lemma for the ballP predicate asserts that the set of points reachable from x in at most n steps is contained in the set reachable in at most m steps whenever n ≤ m. Researchers formalizing discrete causal reachability or kinematics would cite this when comparing balls of different radii in proofs about inclusion of reachable sets. The proof proceeds by induction on the inequality n ≤ m, with the base case immediate by simplification and the successor case injecting the smaller ball into the successor ball via the left disjunct
Claim. Let $K$ be a kinematics structure on a type $α$, let $x ∈ α$, and let $n, m ∈ ℕ$ satisfy $n ≤ m$. Then the set of points $y$ such that $y$ is reachable from $x$ in at most $n$ steps under the step relation of $K$ is contained in the set of points reachable in at most $m$ steps.
background
The Causality.BallP module defines the predicate ballP via a recursive clause on the natural-number radius: at radius 0 the predicate holds only for the center point itself, while at radius $n+1$ it holds if the point lies in the radius-$n$ ball or there exists an intermediate point in the radius-$n$ ball related by the step relation. A Kinematics structure on $α$ is simply a binary relation step : $α → α → Prop$ that encodes admissible one-step transitions. The same recursive definition appears in the sibling modules ConeBound and Reach, indicating that ballP is the common primitive for expressing finite causal reachability.
proof idea
The proof applies induction directly to the hypothesis $n ≤ m$. The reflexive case reduces to set equality and is discharged by simplification. The successor case invokes the inductive hypothesis to obtain membership in the $m$-ball and then places that membership inside the $(m+1)$-ball by selecting the left disjunct of the recursive definition of ballP at the successor level.
why it matters
The result supplies the basic monotonicity property needed to compare reachable sets at different discrete times and is invoked inside the proof of inBall_subset_ballP to convert a reachability witness into membership in the corresponding ballP set. It therefore serves as a supporting lemma for all subsequent arguments that relate the inBall and ballP predicates inside the Causality module. In the Recognition Science setting it provides the elementary inclusion property for the discrete causal balls that underlie later constructions of forcing chains, although it carries no direct reference to the phi-ladder or the T5–T8 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.