inBall_subset_ballP
plain-language theorem explainer
Researchers cite inBall_subset_ballP when bridging the existential formulation of bounded reachability to its inductive counterpart under a kinematics step relation. If y lies in the existential ball of radius n around x, then y lies in the inductive ballP of the same radius. The term proof extracts the witness k, invokes reach_mem_ballP to obtain the exact-level ball, and applies ballP_mono to lift the radius bound.
Claim. If there exists $k$ with $k ≤ n$ such that ReachN$(K, k, x, y)$ holds, then ballP$(K, x, n, y)$ holds, where ballP is the inductive predicate with ballP$(K, x, 0, y) ≡ y = x$ and ballP$(K, x, n+1, y) ≡$ ballP$(K, x, n, y) ∨ ∃z.$ ballP$(K, x, n, z) ∧ K.step$(z, y)$.
background
Kinematics is the structure on type α whose only field is the step relation α → α → Prop. The predicate inBall K x n y is the existential claim that some k ≤ n satisfies ReachN K k x y. By contrast ballP K x n y is defined inductively: it holds at level 0 exactly when y equals x, and at successor levels when it already holds at the predecessor level or a single step reaches y from a point in the predecessor ball.
proof idea
The term proof begins by introducing the triple ⟨k, hk, hreach⟩. It applies reach_mem_ballP to hreach, yielding ballP K x k y. It then feeds the inequality hk into ballP_mono, which supplies the inclusion of the k-ball into the n-ball, and composes to obtain the goal.
why it matters
The lemma is invoked by the identically named result in the Reach module. It guarantees compatibility between the existential ball used in Basic and the inductive ballP employed in ConeBound and Reach, supporting the discrete causal cones required for the forcing chain steps that derive spatial dimension from step relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.