Kinematics
plain-language theorem explainer
Kinematics equips an arbitrary type α with a binary step relation that generates discrete transitions. Reachability and causality developments cite it as the minimal interface for ball predicates and uniqueness arguments. The declaration is a direct structure definition consisting of a single field.
Claim. A kinematics structure on a type α consists of a binary relation step : α → α → Prop.
background
The LedgerUniqueness module introduces this structure after importing Causality.Basic, Potential, and Recognition. The step field is the generator for the inductive ReachN predicate and the existential inBall definition that bounds reachability by a natural number. Identical Kinematics structures appear in Causality.Basic, Causality.ConeBound, Causality.Reach, and LightCone.StepBounds, while CellularAutomata.step supplies a concrete instance obtained by applying a local rule to each cell's neighborhood.
proof idea
This is a direct structure definition; no proof is required.
why it matters
Kinematics parametrizes the ballP definition and its monotonicity, subset, and reachability lemmas in Causality.BallP, as well as the inBall predicate in Causality.Basic. It thereby supports the uniqueness results unique_on_reachN and unique_on_inBall inside LedgerUniqueness. The structure supplies the discrete transition relation underlying light-cone and cone-bound arguments that constrain the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.