Kinematics
plain-language theorem explainer
The Kinematics structure on a type α packages a single binary step relation to model discrete transitions. Researchers on causal propagation and light-cone bounds cite it to parameterize reachability predicates such as ballP and inBall. The construction is a bare structure declaration with no axioms or proof obligations.
Claim. Let α be a type. A kinematics structure on α consists of a binary relation step : α → α → Prop.
background
The ConeBound module supplies minimal local definitions to avoid heavy imports while supporting ball growth bounds under a step relation. The Kinematics structure is defined identically in Causality.Basic, Reach, LedgerUniqueness, and LightCone.StepBounds, each as a record carrying only the step field. This common interface appears in the CellularAutomata step definition that applies a local rule to produce successor states.
proof idea
The declaration is a structure definition that directly introduces the step field. No lemmas, tactics, or reductions are applied.
why it matters
It supplies the parameter type for ballP, ballP_mono, reach_mem_ballP, and inBall in the BallP and Basic modules. These constructions underpin light-cone step bounds and connect to the Recognition framework's causal structure, supporting the emergence of spatial dimensions and bounded propagation in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.