ballFS
plain-language theorem explainer
The recursive definition constructs the set of elements reachable from a given point x in at most n steps through successive applications of the neighbor relation. It is referenced in proofs that establish exponential upper bounds on the size of causal cones within the Recognition Science framework. The construction is given by initializing with the singleton containing x and, for each increment in the step count, adjoining all neighbors of the current set's elements.
Claim. Let $B$ be a structure on type $α$ equipped with a neighbor function $N_B$. The forward ball of radius $n$ around $x$ is the function $B_n(x)$ defined recursively by $B_0(x) = {x}$ and $B_{n+1}(x) = B_n(x) ∪ ⋃_{z ∈ B_n(x)} N_B(z)$.
background
The ConeBound module supplies minimal definitions for analyzing the growth of reachable sets under a step relation with bounded degree, avoiding reliance on external graph libraries. The neighbor relation is drawn from the StakeGraph construction, which filters connected stakeholders via edge predicates. The successor on natural numbers follows the standard inductive definition from arithmetic foundations, where successor is one more application of the generator. This setup enables local control over cone expansion in causal structures of the Recognition framework.
proof idea
The definition matches on the natural number input. For zero steps it returns the Finset singleton of the center point x. For the successor step it computes the previous ball and forms the union of that set with the biUnion over all its members of their individual neighbor sets.
why it matters
This definition provides the explicit set whose cardinality is controlled by the geometric bound theorem, which proves that the number of elements is at most (1 + d)^n where d bounds the degree. It supports the causal cone analysis required for the eight-tick octave structure in Recognition Science by ensuring finite propagation at each phase. The result feeds directly into cardinality lemmas that close the induction for cone size estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.