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

Kinematics

show as:
view Lean formalization →

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.

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

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.

scope and limits

formal statement (Lean)

  11structure Kinematics (α : Type) where
  12  step : α → α → Prop

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.