Reaches
plain-language theorem explainer
Reaches defines reachability of y from x under a kinematics structure K as the existence of a finite step count n where the inductive ReachN holds. Uniqueness lemmas for affine ledgers and potentials in Recognition Science cite this predicate when showing constancy of differences along causal components. The definition is a direct existential wrapper over the inductive ReachN relation supplied by the Kinematics structure.
Claim. Let $K$ be a kinematics structure on type $α$ whose step relation generates transitions. Then Reaches$(K,x,y)$ holds precisely when there exists a natural number $n$ such that ReachN$(K,n,x,y)$, where ReachN is the inductive predicate with base case ReachN$(K,0,x,x)$ and successor step ReachN$(K,n,x,y) ∧ K.step(y,z) → ReachN$(K,n+1,x,z)$.
background
The LedgerUniqueness module works inside a RecognitionStructure M and imports Kinematics from Causality.Basic, where Kinematics is the structure consisting solely of a binary step relation on the underlying type. ReachN is the inductive closure of that step relation: zero steps recover the diagonal, and each successor applies one step. The local Reaches definition is identical in form to the one appearing in Causality.Basic and Causality.Reach.
proof idea
This is a one-line definition that directly introduces Reaches as the existential quantification ∃ n, ReachN K n x y over the inductive ReachN predicate.
why it matters
Reaches supplies the reachability predicate required by unique_up_to_const_on_component (LedgerUniqueness) and by diff_const_on_component (Potential) to conclude that affine ledger values and potential differences are constant on reachable components. It thereby supports the T4 uniqueness results that close the forcing chain from RecognitionStructure to ledger uniqueness up to additive constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.