pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

ReachN

show as:
view Lean formalization →

ReachN inductively defines exact n-step reachability under a kinematics step relation on states. Discrete-model causality work cites it to construct in-ball sets and reachability closures. The definition is given directly by a zero-step identity constructor and a successor constructor that appends one step.

claimLet $K$ be a kinematics structure on type $α$ whose step relation is denoted $K.step$. The relation $Reach_N(K,n,x,y)$ holds precisely when there exists a chain of exactly $n$ steps from $x$ to $y$, defined by the base case $Reach_N(K,0,x,x)$ and the rule $Reach_N(K,n,x,y) ∧ K.step(y,z) → Reach_N(K,n+1,x,z)$.

background

Kinematics is the structure whose sole field is a binary step relation on an arbitrary type $α$. The Causality.Basic module introduces ReachN to capture finite chains of steps; sibling definitions such as inBall and Reaches are built directly on it. Upstream imports supply the same Kinematics signature from ConeBound and Reach, together with the concrete step operation from CellularAutomata and the constant $K=φ^{1/2}$.

proof idea

The declaration is an inductive definition whose two constructors are stated explicitly: the zero constructor gives the identity case at distance 0, while the succ constructor composes one additional step from the kinematics relation.

why it matters in Recognition Science

ReachN supplies the inductive spine for the entire causality layer. It is invoked by reaches_of_reachN, reach_in_ball, reach_le_in_ball, Reaches, and inBall, and by the BallP lemmas ballP_subset_inBall and reach_mem_ballP. The definition therefore closes the basic reachability interface required before any cone or ball arguments can proceed.

scope and limits

formal statement (Lean)

  11inductive ReachN (K : Kinematics α) : Nat → α → α → Prop
  12| zero {x} : ReachN K 0 x x
  13| succ {n x y z} : ReachN K n x y → K.step y z → ReachN K (n+1) x z
  14

used by (29)

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

depends on (13)

Lean names referenced from this declaration's body.