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