System

Spec-level dynamical systems.

Global dynamics are properties of the spec transition function, independent of runtime encodings or execution order.

Why this layer exists (global dynamics context)

The paper "Formalized Hopfield Networks and Boltzmann Machines" (Cipollina--Karatarakis--Wiedijk, 2025, arXiv:2512.07766) is a useful reference point for the kind of global dynamical claims this layer is meant to support. That paper includes deterministic Hopfield convergence, Hebbian-learning, and stochastic Boltzmann/Perron--Frobenius developments.

This repository uses the layer for checked Hopfield trajectory facts and reusable transition-system interfaces. The checked results cover the deterministic asynchronous Hopfield trajectory facts under NN.MLTheory.Proofs.Hopfield, while this file provides reusable transition-system interfaces and trajectory lemmas for other models. We do not claim the Boltzmann, Hebbian, ergodicity, or Perron--Frobenius parts are implemented here.

All of these topics share the same shape: they are statements about trajectories generated by repeatedly applying an update rule, not about a specific runtime implementation. That is why this file abstracts the core notion down to step : SpecTensor s → SpecTensor s.

This file deliberately contains two kinds of objects:

• executable semantics (iterate, trajectory, iterateWithInput, and adapters such as DrivenSystem.freeze), and
• proof interfaces (IsFixedPoint, contraction, Lyapunov stability).

The predicates remain propositions because stability is a mathematical claim, but the file should not stop at predicates. It also proves the algebra of discrete trajectories, so SSMs, diffusion samplers, Hopfield systems, and ODE discretizations can reuse the same recurrence lemmas instead of re-proving bookkeeping facts locally.

structure NN.Spec.Dynamics.DynamicalSystem (s : Spec.Shape) : Type

Discrete-time dynamical system on spec tensors.

• step : Spec.SpecTensor s → Spec.SpecTensor s

  One autonomous transition of the system state.

structure NN.Spec.Dynamics.DrivenSystem (s u : Spec.Shape) : Type

Driven system with exogenous input.

• step : Spec.SpecTensor s → Spec.SpecTensor u → Spec.SpecTensor s

  One transition of the system state, parameterized by the current external input.

def NN.Spec.Dynamics.iterate {s : Spec.Shape} (sys : DynamicalSystem s) (n : ℕ) (x : Spec.SpecTensor s) : Spec.SpecTensor s

Iteration semantics for a discrete-time system.

@[simp]

theorem NN.Spec.Dynamics.iterate_zero {s : Spec.Shape} (sys : DynamicalSystem s) (x : Spec.SpecTensor s) : iterate sys 0 x = x

Zero iterations leave the initial state unchanged.

@[simp]

theorem NN.Spec.Dynamics.iterate_succ {s : Spec.Shape} (sys : DynamicalSystem s) (n : ℕ) (x : Spec.SpecTensor s) : iterate sys (n + 1) x = sys.step (iterate sys n x)

One more iteration applies one system step after the previous trajectory state.

theorem NN.Spec.Dynamics.iterate_add {s : Spec.Shape} (sys : DynamicalSystem s) (m n : ℕ) (x : Spec.SpecTensor s) : iterate sys (m + n) x = iterate sys m (iterate sys n x)

Running m+n steps is the same as running n steps and then m more.

def NN.Spec.Dynamics.trajectory {s : Spec.Shape} (sys : DynamicalSystem s) (x0 : Spec.SpecTensor s) : ℕ → Spec.SpecTensor s

The trajectory (orbit) of an initial condition under sys.

@[simp]

theorem NN.Spec.Dynamics.trajectory_zero {s : Spec.Shape} (sys : DynamicalSystem s) (x0 : Spec.SpecTensor s) : trajectory sys x0 0 = x0

The first point of a trajectory is its initial condition.

@[simp]

theorem NN.Spec.Dynamics.trajectory_succ {s : Spec.Shape} (sys : DynamicalSystem s) (x0 : Spec.SpecTensor s) (n : ℕ) : trajectory sys x0 (n + 1) = sys.step (trajectory sys x0 n)

Successive trajectory points are related by the system transition.

def NN.Spec.Dynamics.iterateWithInput {s u : Spec.Shape} (sys : DrivenSystem s u) (input_seq : ℕ → Spec.SpecTensor u) : ℕ → Spec.SpecTensor s → Spec.SpecTensor s

Iteration semantics for a driven system with an input stream.

def NN.Spec.Dynamics.drivenTrajectory {s u : Spec.Shape} (sys : DrivenSystem s u) (input_seq : ℕ → Spec.SpecTensor u) (x0 : Spec.SpecTensor s) : ℕ → Spec.SpecTensor s

The trajectory (orbit) of a driven system under a fixed input stream.

@[simp]

theorem NN.Spec.Dynamics.iterateWithInput_zero {s u : Spec.Shape} (sys : DrivenSystem s u) (input_seq : ℕ → Spec.SpecTensor u) (x : Spec.SpecTensor s) : iterateWithInput sys input_seq 0 x = x

Zero driven steps leave the initial state unchanged.

@[simp]

theorem NN.Spec.Dynamics.drivenTrajectory_zero {s u : Spec.Shape} (sys : DrivenSystem s u) (input_seq : ℕ → Spec.SpecTensor u) (x0 : Spec.SpecTensor s) : drivenTrajectory sys input_seq x0 0 = x0

The first point of a driven trajectory is its initial condition.

@[simp]

theorem NN.Spec.Dynamics.iterateWithInput_succ {s u : Spec.Shape} (sys : DrivenSystem s u) (input_seq : ℕ → Spec.SpecTensor u) (n : ℕ) (x : Spec.SpecTensor s) : iterateWithInput sys input_seq (n + 1) x = sys.step (iterateWithInput sys input_seq n x) (input_seq n)

A driven trajectory advances by applying the next input to the previous driven state.

@[simp]

theorem NN.Spec.Dynamics.drivenTrajectory_succ {s u : Spec.Shape} (sys : DrivenSystem s u) (input_seq : ℕ → Spec.SpecTensor u) (x0 : Spec.SpecTensor s) (n : ℕ) : drivenTrajectory sys input_seq x0 (n + 1) = sys.step (drivenTrajectory sys input_seq x0 n) (input_seq n)

Successive driven trajectory points follow the driven transition and input stream.

def NN.Spec.Dynamics.DrivenSystem.freeze {s u : Spec.Shape} (sys : DrivenSystem s u) (input : Spec.SpecTensor u) : DynamicalSystem s

Freeze a driven system at a fixed input, turning it into an autonomous system.

@[simp]

theorem NN.Spec.Dynamics.DrivenSystem.freeze_step {s u : Spec.Shape} (sys : DrivenSystem s u) (input : Spec.SpecTensor u) (x : Spec.SpecTensor s) : (sys.freeze input).step x = sys.step x input

A frozen driven system takes the same step as the original system at the frozen input.

theorem NN.Spec.Dynamics.iterateWithInput_const_eq_iterate {s u : Spec.Shape} (sys : DrivenSystem s u) (input : Spec.SpecTensor u) (n : ℕ) (x : Spec.SpecTensor s) : iterateWithInput sys (fun (x : ℕ) => input) n x = iterate (sys.freeze input) n x

Constant-input driven iteration agrees with iteration of the frozen autonomous system.

theorem NN.Spec.Dynamics.drivenTrajectory_const_eq_trajectory {s u : Spec.Shape} (sys : DrivenSystem s u) (input : Spec.SpecTensor u) (x0 : Spec.SpecTensor s) (n : ℕ) : drivenTrajectory sys (fun (x : ℕ) => input) x0 n = trajectory (sys.freeze input) x0 n

Constant-input driven trajectories agree with trajectories of the frozen autonomous system.

def NN.Spec.Dynamics.IsFixedPoint {s : Spec.Shape} (sys : DynamicalSystem s) (x : Spec.SpecTensor s) : Prop

x is a fixed point (equilibrium) of sys if step x = x.

structure NN.Spec.Dynamics.FixedPointCertificate {s : Spec.Shape} (sys : DynamicalSystem s) : Type

A proof-carrying fixed-point witness.

• point : Spec.SpecTensor s

  Candidate equilibrium.

• isFixed : IsFixedPoint sys self.point

  Machine-checked proof that the candidate is a fixed point.

theorem NN.Spec.Dynamics.fixedPoint_iterate {s : Spec.Shape} {sys : DynamicalSystem s} {x : Spec.SpecTensor s} (h : IsFixedPoint sys x) (n : ℕ) : iterate sys n x = x

Fixed points remain fixed under any number of iterations.

theorem NN.Spec.Dynamics.fixedPoint_trajectory {s : Spec.Shape} {sys : DynamicalSystem s} {x : Spec.SpecTensor s} (h : IsFixedPoint sys x) (n : ℕ) : trajectory sys x n = x

A trajectory initialized at a fixed point is constant.

def NN.Spec.Dynamics.isContractive {s : Spec.Shape} (sys : DynamicalSystem s) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (factor : Spec.SpecScalar) : Prop

Contraction property for spec dynamics.

def NN.Spec.Dynamics.isLyapunovStable {s : Spec.Shape} (sys : DynamicalSystem s) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (equilibrium : Spec.SpecTensor s) : Prop

Lyapunov stability for spec dynamics.

def NN.Spec.Dynamics.isAsymptoticallyStable {s : Spec.Shape} (sys : DynamicalSystem s) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (equilibrium : Spec.SpecTensor s) : Prop

Asymptotic stability for spec dynamics.

def NN.Spec.Dynamics.isGloballyStable {s : Spec.Shape} (sys : DynamicalSystem s) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (equilibrium : Spec.SpecTensor s) : Prop

Global stability for spec dynamics.