BoundedStep
plain-language theorem explainer
A class equips any type alpha with a step relation whose successors are exactly the members of a finite neighbor set whose cardinality is capped by a fixed natural number. Researchers constructing causal cones or discrete propagation models cite the class to guarantee finite out-degree at every point. The declaration is a direct class packaging four fields with no separate proof obligations.
Claim. A type $alpha$ carries a bounded-step relation of out-degree at most $d$ when equipped with a binary relation step, a map neighbors from $alpha$ to finite subsets of $alpha$, a proof that step$(x,y)$ holds precisely when $y$ belongs to neighbors$(x)$, and a proof that the cardinality of neighbors$(x)$ is at most $d$ for every $x$.
background
In the Causality module the step relation encodes local transitions between states while the neighbors function returns the finite set of immediate successors. The equivalence field forces the relation to coincide exactly with set membership, and the degree-bound field caps branching uniformly. This interface reuses the global step operation defined in CellularAutomata, which applies a local rule to each cell of a tape, and the neighbor extraction defined in StakeGraph, which filters adjacent nodes in a directed graph.
proof idea
The declaration is a class definition with an empty proof body. It simply assembles the step predicate, the neighbor function, the membership equivalence, and the cardinality inequality into a single structure that downstream code can instantiate.
why it matters
The class supplies the bounded-step interface required by ballP in ConeBound, which builds reachable sets by iterated application of the step relation. It also appears in the SimpleTicks example that models periodic two-state schedules. Within the framework the bounded out-degree supports finite causal cones and controlled propagation speed, consistent with the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.