IndisputableMonolith.Causality.BallP
This module introduces the ballP predicate for bounded causal reachability in the Recognition Science framework. It defines when y is reachable from x in at most n steps under a given step relation K.step, along with monotonicity and inclusion lemmas. Researchers modeling finite causal influence would cite these constructions when working with discrete propagation in causality arguments. The module is built as a direct definition plus elementary lemmas derived from the imported step relation.
claimLet $K$ be a structure equipped with a step relation. The predicate $ballP(K,x,n,y)$ holds if and only if $y$ is reachable from $x$ by at most $n$ applications of the step relation. The module also records that $ballP$ is monotone in the step count $n$ and that the $n$-ball is contained in the corresponding inBall set.
background
The Causality section of Recognition Science models discrete propagation via a step relation introduced in the Basic module. BallP extends this by supplying a finite-horizon ball predicate that counts the exact number of steps. The central definition states that ballP K x n y holds precisely when y lies within n steps of x under K.step. Companion lemmas establish monotonicity (larger n yields larger balls) and the inclusion relations between ballP and the inBall predicate.
proof idea
This is a definition module, no proofs. The core object is the inductive definition of ballP together with direct lemmas on monotonicity in n and the two inclusion statements relating ballP to inBall.
why it matters in Recognition Science
The module supplies the ballP construction used to express finite causal reachability throughout the Causality section. It provides the basic bounded-ball tools that higher-level arguments on causal horizons and propagation rely upon in the Recognition Science development.
scope and limits
- Does not define the underlying step relation (imported from Basic).
- Does not treat infinite-step closures or continuous limits.
- Does not establish global transitivity or cycle properties.