KB
plain-language theorem explainer
KB constructs a kinematics instance by copying the step relation from the bounded step B. Researchers developing cone bounds and reachability arguments in causal structures cite it to instantiate the abstract kinematics interface for ball predicates. The definition is a direct record construction with no additional obligations.
Claim. Let $B$ be the bounded step relation on a type $α$. Define the kinematics structure $K_B$ by setting its step relation to be exactly the step relation supplied by $B$.
background
Kinematics is a structure consisting of a binary relation step : α → α → Prop that encodes allowed transitions. The ConeBound module supplies minimal local definitions to derive ball growth bounds under bounded-degree step relations while avoiding heavy imports. Upstream Kinematics structures appear in the Basic, Reach, LedgerUniqueness, and LightCone modules, each supplying the same abstract step interface. The CellularAutomata step definition provides a concrete local update rule that respects neighborhoods of radius one.
proof idea
The definition is a one-line record construction that sets the step field of Kinematics to the step field of B.
why it matters
KB supplies the concrete kinematics instance required by the equivalence theorem mem_ballFS_iff_ballP, which equates membership in the finite-step ball with the ballP predicate. It supports the causality module's development of cone-bound arguments by providing a minimal instantiation. In the Recognition Science framework it contributes to local definitions for bounding reachability under step relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.