IndisputableMonolith.Causality.Basic
Causality.Basic supplies foundational definitions of discrete reachability and ball membership for causal structures. It is imported by modules on uniqueness and potentials that build T4 lemmas. The module is purely definitional with only monotonicity properties on the predicates.
claimDefinitions of the reachability predicate $Reaches(x,y)$ and ball membership $inBall(r,x,y)$ on discrete reach sets, together with the associated maps $ReachN$ and monotonicity statements $inBall_mono$.
background
The module resides in the Causality domain and imports only Mathlib. It introduces the sibling definitions Kinematics, ReachN (n-step reachability), Reaches (transitive reachability), inBall, reach_in_ball, reach_le_in_ball, and inBall_mono. These establish the discrete reach-set setting used for later uniqueness arguments. The local theoretical setting is the discrete causal structure preceding T4 lemmas on reach sets.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the base layer imported by BallP, LedgerUniqueness, and Potential. Potential in turn uses these definitions for dependency-light T4 uniqueness lemmas on discrete reach sets, placing the material at the T4 step of the forcing chain.
scope and limits
- Does not prove uniqueness or ledger theorems.
- Does not introduce phi-ladder, J-cost, or physical constants.
- Does not treat continuous or relativistic causality.
- Does not depend on upstream Recognition Science results.