ballFS_card_le_geom
plain-language theorem explainer
The theorem bounds the cardinality of the forward ball of radius n around any point x by (1 + d)^n, where d is the maximum number of neighbors per point under the step relation. Researchers deriving volume controls for causal cones or discrete light cones in Recognition Science cite this growth estimate. The proof is a direct induction on n that applies the successor cardinality inequality at each step and closes via arithmetic on natural-number powers.
Claim. Let $B_n(x)$ denote the forward ball of radius $n$ around $x$ generated by the neighbor relation. Then $|B_n(x)|$ satisfies $|B_n(x)| ≤ (1 + d)^n$ for every natural number $n$.
background
The ConeBound module supplies minimal local definitions for ball growth under a bounded-degree step relation, avoiding heavy Mathlib imports. The function ballFS is defined recursively: the ball of radius 0 is the singleton {x}, while the ball of radius n+1 is the union of the previous ball with the neighbors of all its points. The constant d bounds the out-degree of the neighbor relation B, so each successor step multiplies cardinality by at most 1 + d.
proof idea
Proof by induction on n. The base case n = 0 rewrites ballFS to the singleton and applies the card_singleton lemma. The inductive step invokes card_ballFS_succ_le to obtain the inequality (ballFS x (n+1)).card ≤ (1 + d) · (ballFS x n).card, multiplies the inductive hypothesis on the right, and simplifies the resulting expression with Nat.pow_succ and ring.
why it matters
The result supplies the basic geometric growth bound for reachable sets in the causal structure, supporting cone-volume arguments in the Causality section. It closes a foundational step for controlling finite branching under the step relation B, consistent with Recognition Science emphasis on discrete causal cones. No downstream uses are recorded yet, but the bound is available for any later estimate of light-cone sizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.