Kinematics
plain-language theorem explainer
Kinematics equips any type α with a binary step relation that generates reachability and causal balls. Researchers constructing discrete light cones or reach sets in the Causality domain cite this structure when defining n-step neighborhoods from local transitions. The declaration is a bare structure definition with a single field and no proof obligations.
Claim. A structure $Kinematics(α)$ consisting of a binary relation $step : α → α → Prop$.
background
In the Causality.Reach module the Kinematics structure supplies the step relation used to define reachability predicates and balls. This matches the Kinematics structures in Basic, ConeBound, LedgerUniqueness and LightCone.StepBounds, each providing the identical step field. The CellularAutomata.step definition shows how such a relation arises by applying a local rule to produce successor states.
proof idea
The declaration is a structure definition. It introduces Kinematics α with the single field step : α → α → Prop and carries no proof body or additional obligations.
why it matters
This structure serves as the input type for ballP, ballP_mono, reach_mem_ballP and inBall in the BallP and Basic modules. It supplies the kinematic primitive for the reachability chain, supporting cone bounds and step limits from the underlying transition relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.