mem_ballFS_iff_ballP
plain-language theorem explainer
The theorem equates membership in the iteratively built finite ball around x with the inductive reachability predicate under the kinematics KB induced by the step relation. Researchers deriving cardinality bounds on causal cones in discrete graphs cite it to interchange set and Prop formulations. The proof runs by induction on radius n, splitting on union membership and invoking the inductive hypothesis plus the step_iff_mem equivalence in each direction.
Claim. Let $B$ be a graph equipped with a neighbor relation. Define the finite ball $ballFS(x,n)$ recursively by $ballFS(x,0) = {x}$ and $ballFS(x,n+1) = ballFS(x,n) ∪ ⋃_{z∈ballFS(x,n)} neighbors(z)$. Let $KB$ be the kinematics whose step relation is exactly $B.step$. Let $ballP(KB,x,n,y)$ be the inductive predicate that holds when $y=x$ at step 0 and, at successor steps, when it holds at the predecessor level or a predecessor $z$ satisfies the step to $y$. Then $y ∈ ballFS(x,n) ↔ ballP(KB,x,n,y)$ for all $n$ and $y$.
background
The ConeBound module supplies minimal local definitions for ball growth under a bounded-degree step relation, avoiding heavy imports. The finite ball ballFS is the noncomputable recursive Finset that begins with the singleton at radius 0 and at each successor step unions the previous ball with the neighbors of its members. The predicate ballP, drawn from the BallP and Reach modules, is the standard inductive definition of reachability: it holds at 0 precisely when the target equals the center, and at successor steps when it held previously or a predecessor in the prior ball has a step to the target.
proof idea
Proof is by induction on n. The zero case simplifies directly to singleton membership, matching the base clause of ballP. For the successor step the forward direction splits on Finset.mem_union, applies the inductive hypothesis to the previous-ball disjunct, and for the neighbor-union disjunct extracts the witness z, converts via the inductive hypothesis, and rewrites with B.step_iff_mem. The reverse direction splits on the disjunction inside ballP, rebuilds the union membership from the inductive hypothesis, and uses the same step_iff_mem equivalence to populate the neighbor set.
why it matters
The result lives inside the Causality.ConeBound module whose purpose is to supply ball-growth bounds for causal cones. It lets later cardinality lemmas interchange the Finset representation (convenient for counting) with the inductive Prop (convenient for logical manipulation). In the broader Recognition framework it supports analysis of discrete reachability, consistent with the forcing chain's passage from bounded-step relations to spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.