Reaches
plain-language theorem explainer
Reaches asserts that one point is reachable from another via a finite number of steps in a kinematics structure equipped with a step relation. Researchers modeling causal propagation in the Recognition Science framework cite this when establishing connected components for uniqueness theorems. The definition directly encodes an existential quantification over the inductive definition of exact-step reachability.
Claim. Let $K$ be a kinematics structure on a set $α$ consisting of a binary step relation. Then Reaches$(K,x,y)$ holds precisely when there exists a natural number $n$ such that $y$ can be reached from $x$ in exactly $n$ steps under the step relation of $K$.
background
The Kinematics structure consists of a type $α$ equipped with a binary step relation step : $α → α → Prop$. ReachN is the inductive predicate that formalizes reachability in a precise number of steps: the zero constructor states that every point reaches itself in zero steps, while the successor constructor extends a chain by one application of the step relation. This definition sits in the Causality.Reach module and supplies the basic reachability notion imported into Basic and ConeBound for causal analysis throughout the framework.
proof idea
The declaration is a direct definition expressing existential quantification over the natural numbers and the ReachN inductive predicate.
why it matters
This definition underpins the reaches_of_reachN lemma and is referenced in LedgerUniqueness for unique_up_to_const_on_component and in Potential for diff_const_on_component together with T4_unique_up_to_const_on_component. It supplies the causal reachability components that support uniqueness up to constants on connected components, consistent with the framework's use of causal structure to fix physical quantities up to additive constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.