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

ReachN

show as:
view Lean formalization →

ReachN defines the inductive n-step reachability predicate under a kinematics structure K on type α. Researchers deriving light-cone bounds and ball inclusions in discrete causal models cite it to relate exact step counts to membership in reachable sets. The definition is a standard inductive construction with a zero base case and a successor rule that appends one application of the step relation.

claimLet $K$ be a kinematics structure on type $α$ whose step relation encodes allowed transitions. The predicate ReachN$(K,n,x,y)$ holds if $y$ is reachable from $x$ in exactly $n$ steps, defined inductively by the base case ReachN$(K,0,x,x)$ for any $x$ and the rule: if ReachN$(K,n,x,y)$ and $K$.step$(y,z)$ then ReachN$(K,n+1,x,z)$.

background

Kinematics is the structure on a type $α$ that supplies a binary step relation, as introduced in Causality.Basic and mirrored in ConeBound and Reach. The LightCone.StepBounds module defines this local ReachN to support subsequent step-bound and cone-saturation lemmas. Upstream, the step operation from CellularAutomata is documented as applying the local rule globally to create a successor tape.

proof idea

The declaration is an inductive definition. The zero constructor directly asserts reflexivity at step count zero. The succ constructor extends any existing ReachN chain by one application of the kinematics step relation, increasing the count by one.

why it matters in Recognition Science

ReachN supplies the exact-reachability predicate that downstream results in BallP and Causality.Basic convert into ball membership and Reaches. It is invoked by ballP_subset_inBall, reach_mem_ballP, reach_in_ball, and reaches_of_reachN to close the light-cone inclusions. In the Recognition framework it anchors the step-bound analysis that connects cellular-automaton evolution to causal cones.

scope and limits

formal statement (Lean)

  13inductive ReachN {α} (K : Kinematics α) : Nat → α → α → Prop
  14| zero {x} : ReachN K 0 x x
  15| succ {n x y z} : ReachN K n x y → K.step y z → ReachN K (n+1) x z
  16end Local
  17

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.