Reaches
Reaches defines the proposition that x is reachable from y under kinematics K whenever some finite n exists with ReachN K n x y. Downstream lemmas in LedgerUniqueness and Potential cite it to establish constancy of differences along causal chains. The definition is an immediate existential packaging of the inductive ReachN.
claimFor a kinematics structure $K$ on type $α$ equipped with step relation, Reaches$(K,x,y)$ holds precisely when there exists $n ∈ ℕ$ such that ReachN$(K,n,x,y)$ is satisfied.
background
Kinematics is the structure with a single field step : α → α → Prop modeling discrete transitions. ReachN is the inductive definition of exact-n reachability: base case ReachN K 0 x x, and inductive step ReachN K (n+1) x z from ReachN K n x y and step y z. The module Causality.Basic sets up these primitives for the Recognition Science treatment of causality. Upstream results reuse the same Kinematics structure in ConeBound and Reach modules.
proof idea
This is a one-line definition that directly introduces the existential quantifier over the natural number n in the ReachN predicate.
why it matters in Recognition Science
It provides the reachability predicate used by reaches_of_reachN and by uniqueness lemmas such as unique_up_to_const_on_component in LedgerUniqueness, which shows potentials agree up to constant on reachable components. This supports the causal structure in the framework, linking to the phi-ladder and forcing chain by formalizing connectivity from the step relation. It closes no scaffolding but enables T4-type uniqueness results.
scope and limits
- Does not bound the step count n.
- Does not assume transitivity or other properties of the step relation.
- Does not induce a metric on α.
- Does not restrict the type α.
formal statement (Lean)
24def Reaches (K : Kinematics α) (x y : α) : Prop := ∃ n, ReachN K n x y
proof body
Definition body.
25