BoundedStep
plain-language theorem explainer
BoundedStep equips any type α with a step relation whose successors are exactly the members of a neighbor set whose cardinality is bounded by a fixed natural number. Researchers constructing causal cones or discrete dynamical models cite the class to enforce locally finite out-degree. The declaration consists of a bare class packaging four fields with no computational content or proof obligations.
Claim. A type $α$ equipped with a binary relation $step:α→α→Prop$ and a map $neighbors:α→Finset α$ such that $step(x,y)↔y∈neighbors(x)$ for all $x,y$ and $|neighbors(x)|≤degree_bound$ for every $x$.
background
The Causality module models discrete propagation via step relations on state spaces. BoundedStep requires each state to possess only finitely many immediate successors and imposes a uniform upper bound on that number. The class imports the step predicate from CellularAutomata.step (the global application of a local rule to a tape) and the neighbors function from StakeGraph.neighbors (the list of adjacent stakeholders connected by an edge). The identical interface already appears in ConeBound.BoundedStep, indicating this module supplies a reusable packaging of the same bounded-degree requirement.
proof idea
The declaration is a class definition containing no proof body. It directly assembles the four fields step, neighbors, the equivalence step_iff_mem, and the cardinality assertion degree_bound_holds.
why it matters
The class supplies the bounded out-degree hypothesis required by ballP in ConeBound, which builds the reachable set under iterated steps, and is instantiated in the SimpleTicks example for alternating tick schedules. It thereby supports finite-branching causal cones inside the Recognition framework, consistent with the locally finite relations presupposed by the forcing chain from T0 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.