inBall_mono
plain-language theorem explainer
Monotonicity of the in-ball predicate states that if y lies in the n-ball around x under kinematics K, and n ≤ m, then y also lies in the m-ball. Discrete causal modelers cite this when extending finite-step reachability bounds in inductive arguments over step counts. The proof unpacks the existential witness k ≤ n and applies transitivity of ≤ to obtain the larger bound.
Claim. Let $K$ be a kinematics structure on type $α$ with step relation. For $x,y ∈ α$ and $n,m ∈ ℕ$ with $n ≤ m$, if there exists $k ≤ n$ such that $y$ is reachable from $x$ in exactly $k$ steps under $K$, then there exists $k ≤ m$ with the same reachability.
background
Kinematics is the structure whose sole field is a binary step relation on $α$ that encodes allowed one-step transitions. The predicate inBall $K$ $x$ $n$ $y$ is defined as the existence of some $k ≤ n$ for which ReachN $K$ $k$ $x$ $y$ holds, where ReachN denotes exact $k$-step reachability obtained by iterating the step relation. The lemma sits in the Causality.Reach module, which imports Mathlib and re-uses the Kinematics interface also present in Basic and ConeBound.
proof idea
Term-mode proof that introduces the witness triple ⟨k, hk, hkreach⟩ from the n-ball assumption, then applies le_trans hk hnm to strengthen the inequality to k ≤ m and repackages the identical reachability witness for the m-ball.
why it matters
The result supplies the basic monotonicity property required for inductive arguments over step counts in causal reachability. It is invoked by the matching inBall_mono declaration in the Basic module, closing a foundational fact needed before cone-bound and reachability lemmas. In the Recognition framework it supports discrete approximations to light-cone structure prior to continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.