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

ReachN

show as:
view Lean formalization →

ReachN is the inductive definition of exact n-step reachability under a kinematics step relation on type α. Researchers formalizing causal cones and reachable sets in discrete models cite it when deriving ball inclusions and reachability lemmas. The definition is supplied directly by the zero and succ constructors with no separate proof obligations.

claimLet $K$ be a kinematics structure on a type $α$ consisting of a binary step relation. The predicate ReachN$_K(n,x,y)$ holds if and only if there exists a chain of exactly $n$ steps from $x$ to $y$ under that relation.

background

Kinematics is the structure supplying a step relation on an arbitrary type α; the same structure appears in the sibling Basic and ConeBound modules. ReachN is defined in the Causality.Reach module and is the primitive used to build inBall (existence of some k ≤ n) and Reaches (existence of some n). Upstream results include the step definition from CellularAutomata, which applies a local rule to produce successor states, and the constant K = φ^{1/2}.

proof idea

This is an inductive definition whose two constructors are given explicitly. The zero constructor asserts reflexivity at distance zero. The succ constructor takes a chain of length n together with one additional step and produces a chain of length n+1.

why it matters in Recognition Science

ReachN is the foundational inductive relation for all subsequent causality constructions; it is used by inBall, Reaches, reach_in_ball, reaches_of_reachN, ballP_subset_inBall and reach_mem_ballP. These lemmas in turn support cone bounds and ball inclusions that realize the discrete causal structure required by the Recognition Science forcing chain.

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.