Kinematics
plain-language theorem explainer
Kinematics α packages a binary step relation on type α as the basic interface for discrete causal evolution. Researchers building reachability sets or light-cone bounds in the causality layer cite this structure to parameterize their constructions. The definition is a direct record declaration with a single field and no proof obligations.
Claim. A kinematics structure on a type $α$ consists of a binary relation $step : α → α → Prop$.
background
In Causality.Basic the Kinematics structure supplies the minimal interface for causal steps. Identical structures appear in ConeBound, Reach, LedgerUniqueness and LightCone.StepBounds, each exposing the same step field. The field aligns with the global step operation in CellularAutomata, which applies a local rule to each cell's radius-1 neighborhood.
proof idea
Direct structure definition; no tactics or lemmas are applied.
why it matters
Kinematics is the root parameter for the causality layer. It is used to define ballP (the n-step ball) and inBall (bounded reachability via ReachN), which in turn support monotonicity lemmas and subset relations. The structure therefore anchors light-cone and uniqueness arguments in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.