ballP_subset_inBall
The lemma shows that membership in the recursively defined ballP of radius n implies existence of a ReachN witness with at most n steps under any Kinematics step relation. Researchers formalizing discrete causal propagation would cite it to interchange the two ball predicates. The proof is by induction on n, with case analysis on the disjunction inside the successor clause of ballP and direct construction of the ReachN term via zero or succ constructors.
claimLet $K$ be a kinematics structure on a type $α$ with step relation, and let $x,y ∈ α$. For every natural number $n$, if $y$ belongs to the $n$-ball generated from $x$ by iterated steps, then there exists $k ≤ n$ such that $y$ is reachable from $x$ in exactly $k$ steps.
background
Kinematics is the structure consisting solely of a binary step relation on a type α. The ballP predicate is defined recursively on the radius: it holds at radius 0 precisely when the target equals the source, and at radius n+1 when either it already holds at radius n or there is an intermediate point z reachable at radius n with a single step from z to the target. This encodes the set of points reachable in at most n steps via the step relation. The inBall predicate is the existential form: there exists some k ≤ n together with a ReachN witness of exact length k. ReachN is the inductive definition of exact-step reachability, with a zero constructor for distance 0 and a succ constructor that prepends one step.
proof idea
Proof by induction on n. The zero case reduces immediately to y = x and applies the ReachN.zero constructor with bound 0. In the successor case the inductive hypothesis is available; the ballP disjunction splits into the previous-radius case (apply the hypothesis and weaken the bound via Nat.le_trans) or the fresh-step case (apply the hypothesis to the predecessor, then close with ReachN.succ).
why it matters in Recognition Science
The result equates the recursive ballP definition with the existential inBall formulation, permitting free interchange in causal arguments. It is invoked by the corresponding lemma in the Reach module, which in turn supports broader reachability theorems. Within the Recognition Science development it supplies the basic inclusion needed to bound propagation distances inside causal cones.
scope and limits
- Does not prove the converse inclusion from inBall to ballP.
- Does not extend the result to non-discrete or continuous step relations.
- Does not assume any specific properties of the step relation beyond the Kinematics structure.
- Does not address cycles, infinite paths, or reachability beyond finite n.
formal statement (Lean)
35lemma ballP_subset_inBall {K : Kinematics α} {x y : α} :
36 ∀ {n}, ballP K x n y → inBall K x n y := by
proof body
Term-mode proof.
37 intro n
38 induction n generalizing y with
39 | zero =>
40 intro hy; rcases hy with rfl; exact ⟨0, le_rfl, ReachN.zero⟩
41 | succ n ih =>
42 intro hy
43 cases hy with
44 | inl hy' =>
45 rcases ih hy' with ⟨k, hk, hkreach⟩
46 exact ⟨k, Nat.le_trans hk (Nat.le_succ _), hkreach⟩
47 | inr h' =>
48 rcases h' with ⟨z, hz, hstep⟩
49 rcases ih hz with ⟨k, hk, hkreach⟩
50 exact ⟨k + 1, Nat.succ_le_succ hk, ReachN.succ hkreach hstep⟩
51
52end Causality
53end IndisputableMonolith