ballP_subset_inBall
plain-language theorem explainer
The lemma shows that the recursive ballP predicate on a kinematics step relation is contained in the existential inBall predicate. Workers on discrete causal reachability would cite it to interchange the two bounded-step definitions. The argument proceeds by induction on the radius n, reducing the disjunction in ballP to ReachN constructors via case analysis and bound weakening.
Claim. Let $K$ be a kinematics structure on type $α$ with step relation. For $x,y ∈ α$ and $n ∈ ℕ$, if $y$ lies in the recursive ballP of radius $n$ from $x$ then there exists $k ≤ n$ such that ReachN holds for exactly $k$ steps from $x$ to $y$.
background
Kinematics is the structure consisting solely of a binary step relation on a type $α$. The ballP predicate is defined recursively: ballP K x 0 y holds precisely when y = x, while ballP K x (n+1) y holds when either ballP K x n y or there exists z with ballP K x n z and K.step z y. The inBall predicate is the existential form ∃ k ≤ n, ReachN K k x y. ReachN itself is the inductive relation with base ReachN K 0 x x and successor step ReachN K (n+1) x z whenever ReachN K n x y and K.step y z.
proof idea
Induction on n. The zero case matches the equality in ballP to ReachN.zero with witness k = 0. The successor case splits on the disjunction inside ballP: the left disjunct applies the inductive hypothesis and weakens the bound via Nat.le_trans; the right disjunct applies the inductive hypothesis to the predecessor ball and then invokes ReachN.succ to attach the final step.
why it matters
The result is invoked by the identically named lemma in the BallP module, permitting downstream cone-bound arguments to treat the recursive and existential forms interchangeably. It supplies the inclusion needed to relate the two reachability predicates inside the Causality layer. No direct connection to the T0-T8 forcing chain or phi constants is present; the lemma remains foundational infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.