inBall_mono
plain-language theorem explainer
The monotonicity lemma for ball membership states that if a point y lies in the causal ball of radius n around x under kinematics K, then it lies in the ball of any larger radius m where n ≤ m. Discrete causal modelers and reachability theorists cite this when extending finite-step bounds in step-relation structures. The proof is a direct term-mode wrapper that lifts the witness radius k via transitivity of the natural-number order.
Claim. Let $K$ be a kinematics structure on type $α$ with step relation $step: α → α → Prop$. For points $x, y ∈ α$ and natural numbers $n ≤ m$, if there exists $k ≤ n$ such that $y$ is reachable from $x$ in $k$ steps under $K$, then there exists $k' ≤ m$ satisfying the same reachability condition.
background
In the Causality.Basic module a kinematics structure on type $α$ is defined by a single binary step relation $step: α → α → Prop$ that encodes allowed one-step transitions. The predicate inBall $K$ $x$ $n$ $y$ holds exactly when there exists a natural number $k ≤ n$ such that ReachN $K$ $k$ $x$ $y$, where ReachN records exact-step reachability. This lemma depends on the inBall definition and the Kinematics structure; it appears in the same module as the Reach submodule that re-exports the same predicate.
proof idea
The term proof introduces the existential witness triple for inBall at radius $n$, yielding a concrete $k$ together with the inequality $k ≤ n$ and the reachability fact. It then applies the transitivity lemma le_trans to obtain $k ≤ m$ and repackages the updated triple as a witness for the ball of radius $m$.
why it matters
The result supplies the monotonicity step needed to enlarge causal balls in the Reach submodule, which in turn feeds cone-bound constructions that rely on the eight-tick octave and the forcing of three spatial dimensions. It closes a basic inclusion property required before any scaling arguments that connect discrete reachability to the Recognition Science constants or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.