ReachN
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.