Hopfield networks (spec-level)

This file gives a Hopfield network model as a set of explicit mathematical definitions.

• A state is a Boolean vector Fin n → Bool (activation true ↦ +1, false ↦ -1).
• Parameters are a weight matrix W : Fin n → Fin n → α and thresholds θ : Fin n → α.
• An asynchronous update picks a neuron u and updates only that coordinate.

Intended use: mathematical scalars (ℚ, ℝ, etc.) and theorem statements/proofs. For computation, instantiate α := ℚ (or Rat) and evaluate seqStates / energy via #eval in an example file.

TensorState and TensorParams supply the tensor representation used by the executable definitions in Exec below.

References

• Hopfield (1982), "Neural networks and physical systems with emergent collective computational abilities": https://www.pnas.org/doi/10.1073/pnas.79.8.2554
• Hopfield (1984), "Neurons with graded response have collective computational properties like those of two-state neurons": https://www.pnas.org/doi/10.1073/pnas.81.10.3088
• Ramsauer et al. (2020), "Hopfield Networks is All You Need": https://arxiv.org/abs/2008.02217

Relationship to the Hopfield formalization case study

This file provides the definitions (update rule, energy, trajectories). The global-dynamics results (energy monotonicity, fixed-point convergence bounds, tie-handling lemmas, etc.) are proved in NN/MLTheory/Proofs/Hopfield/* against these definitions.

If you’re reading this alongside “Formalized Hopfield Networks and Boltzmann Machines” (2025), the correspondence is:

• updateAt / seqStates formalize the asynchronous update dynamics,
• energy is the Lyapunov/energy functional used for convergence arguments,
• theorems in NN.MLTheory.Proofs.Hopfield.Energy and NN.MLTheory.Proofs.Hopfield.Convergence capture the classic “energy decreases ⇒ convergence” theorem pattern for finite state spaces.

Implementation status

There is no NN.API model builder for Hopfield networks. The definitions are used by the structural proofs in NN/MLTheory/Proofs/Hopfield/* and the guide's rational-arithmetic examples. Exec provides the tensor-facing operations.

Core data

def Spec.Hopfield.act {α : Type} [One α] [Neg α] : Bool → α

Boolean activations interpreted as ±1.

We intentionally store Hopfield states as Bool (instead of α) because many proofs are simpler when the only possible activations are +1 and -1. The embedding into a numeric scalar α is explicit via act.

@[simp]

theorem Spec.Hopfield.act_true {α : Type} [One α] [Neg α] : act true = 1

A true unit activates to +1.

@[simp]

theorem Spec.Hopfield.act_false {α : Type} [One α] [Neg α] : act false = -1

A false unit activates to -1; the network is the classical bipolar Hopfield model.

@[reducible, inline]

abbrev Spec.Hopfield.State (n : ℕ) : Type

Hopfield state as a Boolean activation vector.

@[reducible, inline]

abbrev Spec.Hopfield.TensorState (n : ℕ) : Type

Hopfield state as a vector Tensor Bool [n].

This representation connects the functional Hopfield state with TorchLean's tensor-shaped spec APIs.

def Spec.Hopfield.TensorState.toFun {n : ℕ} (s : TensorState n) : State n

Convert a tensor state to the underlying function representation.

def Spec.Hopfield.TensorState.ofFun {n : ℕ} (s : State n) : TensorState n

Convert a function state to a tensor state.

@[simp]

theorem Spec.Hopfield.TensorState.toFun_ofFun {n : ℕ} (s : State n) : (ofFun s).toFun = s

Packing a state into a tensor and reading it back returns the same function.

@[simp]

theorem Spec.Hopfield.TensorState.ofFun_toFun {n : ℕ} (s : TensorState n) : ofFun s.toFun = s

Reading a tensor state out and packing it back returns the same tensor.

The two directions together say the function and tensor views of a state carry the same information, so an energy argument written over Fin n → Bool transfers to the executable representation.

def Spec.Hopfield.actVec {α : Type} [One α] [Neg α] {n : ℕ} (s : State n) : Fin n → α

The ±1 activation vector associated to a Boolean state.

structure Spec.Hopfield.Params (α : Type) (n : ℕ) : Type

Hopfield parameters:

• W is the weight matrix
• θ is the per-unit threshold / bias

Classic convergence results typically assume W is symmetric and has a zero diagonal. Those assumptions are not baked into this structure; they are stated and proved where needed.

• W : Fin n → Fin n → α

  Weight from unit j to unit i, indexed as W i j.

• θ : Fin n → α

  Activation threshold for each unit.

structure Spec.Hopfield.TensorParams (α : Type) [TorchLean.Storage α] (n : ℕ) : Type

Hopfield parameters as tensor-shaped weights and thresholds.

• W : TorchLean.Tensor α [n, n]

  Weight matrix, with destination units on the first axis and source units on the second.

• θ : TorchLean.Tensor α [n]

  Rank-one tensor of per-unit activation thresholds.

Hopfield update dynamics

def Spec.Hopfield.net {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] {n : ℕ} (p : Params α n) (s : State n) (u : Fin n) : α

Net input to unit u: (W * x)_u, where x = actVec s is the ±1 encoding of the state.

def Spec.Hopfield.updateAt {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Params α n) (s : State n) (u : Fin n) : State n

Asynchronous update at a single coordinate u.

We implement the standard thresholded sign rule:

s[u] := (θ_u ≤ net_u)

Interpreting true ↦ +1 and false ↦ -1, this corresponds to:

x_u := +1 if net_u ≥ θ_u, otherwise x_u := -1.

Tie-handling (net_u = θ_u) matters for formal convergence arguments; we pick the convention "ties go to +1" via ≤.

def Spec.Hopfield.IsStable {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Params α n) (s : State n) : Prop

A state is stable (a fixed point) if updating any single coordinate does nothing.

def Spec.Hopfield.pluses {n : ℕ} (s : State n) : ℕ

Count how many units are in the true (+1) state.

Hopfield energy

def Spec.Hopfield.energy {α : Type} [Field α] {n : ℕ} (p : Params α n) (s : State n) : α

The classical Hopfield energy for a state s (quadratic term + linear threshold term).

With x = actVec s the ±1 encoding, the energy is:

E(s) = -1/2 * Σ_i Σ_j W_ij x_i x_j + Σ_i θ_i x_i.

When W is symmetric and has a zero diagonal, asynchronous updates are known to monotonically decrease (or not increase) E, which is the classic Lyapunov-style argument for convergence.

def Spec.Hopfield.seqStates {α : Type} [AddCommMonoid α] [Mul α] [One α] [Neg α] [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : Params α n) (useq : ℕ → Fin n) (s0 : State n) : ℕ → State n

State sequence induced by an asynchronous update schedule useq.

useq : Nat → Fin n picks which coordinate to update at each discrete time step.

PyTorch analogy: there is no direct equivalent in typical NN libraries, but you can think of it as an explicit, deterministic "update schedule" for coordinate descent.

def Spec.Hopfield.cyclicUseq (n : ℕ) (hn : 0 < n) : ℕ → Fin n

A cyclic update schedule (0,1,2,...,n-1,0,1,...) for n > 0.

Executable Hopfield (backend-friendly)

The definitions above (net, energy, …) are written in a math-first style using ∑ over Fin n. That is the right presentation for proofs, but it bakes in algebraic typeclasses like AddCommMonoid and uses Finset sums.

When we execute Hopfield over IEEE-like scalars (e.g. Float, ExecFloat.Binary 8 23), we do not want to pretend those algebraic laws hold exactly: NaNs and rounding make addition non-associative and non-commutative in general. So for runtime execution we provide a “plain loop” variant that:

• requires only the operations from [TorchLean.Storage α] [Context α],
• uses explicit List.foldl iteration over Fin n.

This is the same model, written with the runtime arithmetic assumptions exposed.

References:

• IEEE 754-2019 (why NaNs/rounding break algebraic laws): https://doi.org/10.1109/IEEESTD.2019.8766229
• Goldberg (1991), classic floating-point background: https://doi.org/10.1145/103162.103163

def Spec.Hopfield.Exec.net {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (p : TensorParams α n) (s : TensorState n) (u : Fin n) : α

Net input to unit u computed by explicit iteration.

This uses the formula of Hopfield.net with an ascending, zero-seeded left fold, so it can execute over IEEE-like scalars without assuming associative addition.

def Spec.Hopfield.Exec.updateAt {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : TensorParams α n) (s : TensorState n) (u : Fin n) : TensorState n

Asynchronous update of a single coordinate u, using the same “ties go to +1” convention as the spec definition (θ_u ≤ net_u).

def Spec.Hopfield.Exec.seqStates {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {n : ℕ} (p : TensorParams α n) (useq : ℕ → Fin n) (s0 : TensorState n) : ℕ → TensorState n

State sequence induced by an update schedule useq : Nat → Fin n (loop-based).

def Spec.Hopfield.Exec.energy {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (p : TensorParams α n) (s : TensorState n) : α

Hopfield energy computed by explicit iteration.

This matches the standard formula: E(s) = -1/2 * Σ_i Σ_j W_ij x_i x_j + Σ_i θ_i x_i, with x_i ∈ {+1,-1} obtained from the Boolean state.