card_ballFS_succ_le
plain-language theorem explainer
The theorem bounds the cardinality of the forward ball of radius n+1 by a factor of (1 + d) times the ball of radius n, where d is the maximum degree in the underlying step relation. Researchers deriving exponential growth controls for causal cones in discrete models would cite this result. The proof decomposes the successor ball as a union of the prior ball with its collective neighbors, applies separate cardinality bounds on the union and the neighbor collection, and simplifies the arithmetic via a calculation block.
Claim. For a graph with maximum degree at most $d$, any vertex $x$, and natural number $n$, $|ball_{FS}(x, n+1)| ≤ (1+d) · |ball_{FS}(x, n)|$, where the forward ball is defined recursively by $ball_{FS}(x,0) := {x}$ and $ball_{FS}(x, n+1) := ball_{FS}(x,n) ∪ ⋃_{z ∈ ball_{FS}(x,n)} N(z)$, with $N(z)$ the neighbor set of $z$.
background
The ConeBound module introduces minimal local definitions for forward balls in a graph whose step relation has bounded degree d. The definition ballFS constructs these balls iteratively: the radius-zero ball is the singleton containing the center x, and each successor ball is obtained by adjoining all neighbors of the current ball's vertices. This construction is tailored to support cone-size estimates in causality arguments.
proof idea
The proof first simplifies the recursive definition of ballFS at the successor step. It introduces prev as the ball of radius n and new_neighbors as the biUnion of the neighbor function over prev. Separate applications of card_union_le and card_bind_neighbors_le produce bounds on the union and on the neighbor collection. These are combined by le_trans into a single inequality prev.card + d * prev.card, after which the calc tactic rewrites the right-hand side to (1 + d) * prev.card using ring.
why it matters
This declaration supplies the key inductive step for the geometric bound theorem ballFS_card_le_geom, which concludes that ball cardinalities grow at most exponentially as (1 + d)^n. In the broader Recognition Science setting it contributes to the control of causal cone volumes, consistent with the discrete eight-tick structure and the derivation of spatial dimension D = 3. It addresses a basic growth estimate required before global causality constraints can be imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.