IndisputableMonolith.Causality.Basic
Causality.Basic supplies the foundational predicates for discrete reachability and ball membership in the Recognition Science causality layer. Researchers building T4 uniqueness arguments on reach sets cite it as the base. The module consists of definitions plus elementary monotonicity facts with no complex proofs.
claimDefines the n-step reachability predicate ReachN(p, q, n), the ball membership inBall(r, p, q), and its transitive closure Reaches(p, q).
background
The module opens the Causality domain and introduces the discrete reachability apparatus used throughout the framework. ReachN encodes finite-step causal propagation while inBall bounds that propagation inside a radius; Reaches is the existential closure. Kinematics supplies the underlying motion rules and inBall_mono records the obvious monotonicity in the radius. The module imports only Mathlib and carries no upstream RS theorems.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
Supplies the reachability primitives required by IndisputableMonolith.Causality.BallP, IndisputableMonolith.LedgerUniqueness, and IndisputableMonolith.Potential. The last of these applies the definitions to obtain dependency-light T4 uniqueness lemmas on discrete reach sets, placing the material at the T4 stage of the forcing chain.
scope and limits
- Does not prove any T4 uniqueness statements.
- Does not reference the J-cost or phi-ladder.
- Does not treat continuous or relativistic causality.
- Does not import physics constants or the RCL.