reaches_of_reachN
plain-language theorem explainer
The lemma shows that exact n-step reachability under a kinematics step relation implies existential reachability in some finite number of steps. Discrete causality formalizations cite it to move between inductive step counts and existence statements without tracking n explicitly. The proof is a one-line wrapper applying the existential constructor directly to the ReachN hypothesis.
Claim. Let $K$ be a kinematics structure on a type $α$ whose step relation is a binary predicate. If $y$ is reachable from $x$ in exactly $n$ steps under the inductive ReachN predicate, then $y$ is reachable from $x$ under the existential Reaches predicate.
background
Kinematics is the structure supplying a binary step relation on an arbitrary type $α$. ReachN is the inductive predicate for exact finite chains: the zero constructor gives reflexivity at zero steps, while the successor constructor extends a chain by one application of the step relation. Reaches is defined as the existential closure asserting that some natural number of steps suffices.
proof idea
The proof is a one-line wrapper that applies the existential constructor ⟨n, h⟩ to the given hypothesis h : ReachN K n x y, directly matching the definition of Reaches as ∃ n, ReachN K n x y.
why it matters
This lemma bridges the inductive ReachN to the existential Reaches, allowing downstream proofs in the Reach module to work with existence rather than concrete step counts. It supports the construction of causal cones and bounds within the Causality.Basic module of the Recognition Science monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.