Kinematics
plain-language theorem explainer
The kinematics structure supplies a binary step relation on an arbitrary type that parameterizes reachability and bounded propagation in the light-cone setting. Discrete causal modelers cite this declaration when they need a uniform carrier for successor steps before deriving ball or cone predicates. The entry is a bare structure definition that simply declares the relation field with no further computation.
Claim. A kinematics structure on a type $α$ consists of a binary relation step $: α → α → Prop$.
background
The structure reappears in Causality.Basic, ConeBound, Reach, and LedgerUniqueness to keep each file self-contained while sharing the same primitive. It serves as the sole input to reachability and ball constructions that count discrete steps. In the present LightCone.StepBounds module the structure is paired with the cellular-automaton step operation, which applies a local rule globally to produce the successor tape configuration.
proof idea
The declaration is a structure definition. It introduces the single field step without invoking lemmas or tactics.
why it matters
Thirty-seven downstream declarations depend on this interface, among them the ballP predicate and its monotonicity, subset, and reach-membership lemmas. The structure supplies the step primitive that lets cone bounds saturate and that relates reachability to in-ball membership. It anchors the discrete light-cone geometry used to extract spatial dimension and propagation limits in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.