IndisputableMonolith.Causality.BoundedStep
The Causality.BoundedStep module defines a locally finite step relation whose out-degree is bounded. It supplies the basic object for modeling discrete causal progressions with finite branching. Workers on causal graphs in discrete spacetime cite this structure to enforce local finiteness. The module is a pure definition block with a single import and no internal proofs.
claimA step relation $R$ on a set $X$ is locally finite with bounded out-degree when, for every $x$, the set of immediate successors is finite and its cardinality admits a uniform upper bound independent of $x$.
background
The module resides in the Causality domain and introduces the core notion of a bounded step relation. Its single import is Mathlib; no Recognition Science modules are required. The supplied doc-comment states the purpose directly: locally-finite step relation with bounded out-degree. No upstream lemmas are referenced.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The definition supplies the basic causal object used by later constructions in the causality section. It prepares the ground for theorems that will enforce finite causal chains and connect to the eight-tick octave structure. No parent theorems are recorded yet.
scope and limits
- Does not instantiate any concrete step relation.
- Does not contain theorems or proofs.
- Does not depend on other Recognition Science modules.
- Does not fix a numerical value for the out-degree bound.