inBall
plain-language theorem explainer
The reachability predicate asserts that y is reachable from x in at most n steps under the step relation of a kinematics structure K. Researchers working on causal neighborhoods and uniqueness in discrete systems cite it when bounding finite-horizon propagation. It is introduced directly as an existential quantification over the inductive exact-step reachability predicate.
Claim. Let $K$ be a kinematics structure on type $α$ equipped with a binary step relation. For points $x,y∈α$ and natural number $n$, the predicate holds precisely when there exists $k≤n$ such that $y$ is reachable from $x$ in exactly $k$ steps under the inductive closure of the step relation.
background
Kinematics is the structure supplying a binary step relation on the carrier type $α$. ReachN is the inductive predicate closing this relation under iteration: the zero case holds by reflexivity at identical points, while the successor case extends reachability by one application of the step relation. The present definition packages these primitives into a bounded-reachability statement. It appears in the LedgerUniqueness module after importing the core causality and recognition primitives, serving as a local handle for later uniqueness arguments on causal components. Upstream results in Causality.Basic and Causality.Reach supply identical definitions of the same predicate and inductive relation, indicating reuse across modules for organizing ledger-specific proofs.
proof idea
This is a direct definition that packages the existential quantification over the inductive ReachN predicate together with the inequality constraint on the step count. No lemmas or tactics are invoked; the body is the defining equation itself.
why it matters
The predicate supplies the target for the equivalence lemmas ballP_subset_inBall and inBall_subset_ballP that identify the two ball notions. It is also the subject of the monotonicity lemma inBall_mono and the reach lemmas reach_in_ball and reach_le_in_ball in the basic causality module. Within the Recognition Science development it anchors the finite causal neighborhoods required by the uniqueness theorems unique_on_inBall and unique_up_to_const_on_component in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.