pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Kinematics

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

   8structure Kinematics (α : Type) where
   9  step : α → α → Prop
  10

used by (37)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 7 more

depends on (5)

Lean names referenced from this declaration's body.