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

Kinematics

show as:
view Lean formalization →

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.

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

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.

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.