pith. sign in
module module moderate

IndisputableMonolith.Causality.Basic

show as:
view Lean formalization →

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

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (8)