BoundedStep
plain-language theorem explainer
A class equipping a type alpha with a binary step relation and neighbor function such that the relation holds exactly on the neighbors and every node has out-degree at most the supplied bound. Researchers modeling causal cones or discrete automata cite it to guarantee finite reachable sets under local steps. The declaration is the direct encoding of those four fields with no further derivation.
Claim. Let $alpha$ be a type and $d$ a natural number. A $d$-bounded step structure on $alpha$ consists of a relation $step : alpha to alpha to Prop$, a function $neighbors : alpha to Finset(alpha)$, such that $step(x,y)$ holds if and only if $y in neighbors(x)$, and $|neighbors(x)| leq d$ for every $x$.
background
The ConeBound module supplies minimal local definitions to derive ball growth bounds without heavy imports. It rests on the BoundedStep class, described upstream as a locally-finite step relation with bounded out-degree. The step definition from CellularAutomata applies a local rule to produce successor tapes, while the neighbors function from StakeGraph selects adjacent stakeholders via edge membership.
proof idea
This is the definition of the BoundedStep class. It directly specifies the four fields: the step predicate, the neighbors map, the equivalence lemma step_iff_mem, and the cardinality bound degree_bound_holds.
why it matters
The class is the prerequisite for ballP, which builds reachable sets by iterated application of the step relation, and appears in the SimpleTicks modeling example. It supplies the finite-degree hypothesis needed for cone bounds in the causality setting, consistent with the framework's use of discrete local steps to control growth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.