IndisputableMonolith.Causality.BoundedStep
The module introduces a step relation that is locally finite with uniformly bounded out-degree for use in discrete causal models. Physicists modeling finite propagation in Recognition Science cite it to enforce no infinite branching from any event. The module contains only the core definition and imports Mathlib for the underlying relation type; no theorems are proved here.
claimA binary 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 bound independent of $x$.
background
Within the Causality domain, Recognition Science represents discrete transitions by step relations. The module supplies the BoundedStep definition that guarantees each point has only finitely many direct successors and that the maximum number of such successors is globally bounded. This setting draws on standard set-theoretic relations from Mathlib and prepares the ground for later results on causal cones and finite propagation.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
BoundedStep supplies the finite-branching hypothesis required by downstream causality theorems that establish bounded causal influence and finite light-cone structure. It directly supports the framework's insistence on locally finite discrete steps before any appeal to the eight-tick octave or phi-ladder scaling.
scope and limits
- Does not prove any properties of the relation beyond the definition itself.
- Does not specify the concrete set $X$ or the generating step function.
- Does not link the bound to Recognition Science constants such as phi or the J-cost.
- Does not treat infinite out-degree cases or continuous limits.