ballP_subset_inBall
plain-language theorem explainer
The lemma shows that the recursively defined ballP predicate (points reachable in at most n steps via the step relation) is contained in the inBall predicate (existence of some k ≤ n with exact ReachN reachability). Researchers formalizing discrete causal reachability would cite it when switching between the two ball definitions. The proof is a direct induction on n that applies the inductive hypothesis to each disjunct of the successor clause and adjusts the witness count with Nat.le_trans or ReachN.succ.
Claim. Let $K$ be a kinematics structure on type $α$ with step relation. For $x,y ∈ α$ and $n ∈ ℕ$, if $y$ satisfies the recursive ball predicate of radius $n$ around $x$ (i.e., $y=x$ at radius 0, or reachable from some prior point in the ball via one step), then there exists $k ≤ n$ such that the inductive reachability relation ReachN holds for exactly $k$ steps from $x$ to $y$.
background
Kinematics $α$ is the structure containing only a binary step relation. The ballP predicate is defined recursively: ballP $K$ $x$ 0 $y$ holds precisely when $y=x$, while ballP $K$ $x$ (succ $n$) $y$ holds when either ballP $K$ $x$ $n$ $y$ or there exists $z$ with ballP $K$ $x$ $n$ $z$ and step $z$ $y$. The inBall predicate is the existential form ∃ $k$ ≤ $n$, ReachN $K$ $k$ $x$ $y$. ReachN itself is the inductive exact-step reachability: zero gives ReachN 0 $x$ $x$, and succ lifts a ReachN $n$ $x$ $y$ by one step to ReachN (n+1) $x$ $z$. This lemma sits inside the Causality.BallP module whose imports are Mathlib and Causality.Basic; the two ball notions appear in parallel in ConeBound and Reach as well.
proof idea
The term-mode proof opens with intro n then performs induction on n generalizing over y. The zero case matches the ballP equality and directly supplies the ReachN.zero witness. The successor case splits on the ballP disjunction: the left disjunct applies the inductive hypothesis and weakens the witness bound by Nat.le_trans with Nat.le_succ; the right disjunct extracts the intermediate z, applies the inductive hypothesis to obtain a ReachN witness, then closes with ReachN.succ.
why it matters
The result supplies the inclusion needed to move freely between the two ball predicates inside the Causality.Reach module (the sole downstream use). It therefore supports any later argument that begins with the compact recursive ballP definition yet requires an explicit reachability witness. In the broader Recognition Science setting this inclusion is part of the discrete causal scaffolding that precedes the forcing chain (T0–T8) and the Recognition Composition Law; without it, statements about reachability inside the eight-tick octave or the phi-ladder would have to duplicate the same inductive argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.