Hopfield Dynamics🔗

A TorchLean Hopfield state is a Boolean vector, and its parameters are a weight matrix together with a threshold vector. The energy argument follows Hopfield (1982) for asynchronous updates. The following commands check the state and parameter types:

State : ℕ → Type

State n unfolds to Fin n → Bool. The numeric activation map reads true as +1 and false as -1, so the Boolean carrier is a storage choice rather than a claim that the model is Boolean valued. Params α n holds the fields W : Fin n → Fin n → α and θ : Fin n → α, and it is polymorphic in the scalar: the same structure serves the executable Rat runs below and the real-valued theorems that follow.

Fin n is the type of valid neuron indices, so a state is a function that returns one bit for each neuron without admitting an out-of-range coordinate. List.ofFn in the examples merely displays those bits in index order. It does not change the state representation or supply the numeric activation map. This distinction matters when reading the energy table: a printed false contributes minus one to the sums, not zero. In the type of energy, [Field α] requests the arithmetic operations and laws used to form the expression. An energy-decrease result additionally needs an order and assumptions connecting the weights to the update rule; those appear in the real theorem rather than in the parameter record.

For state s, write x_i\in\{-1,+1\} for its numeric activation. The net input to neuron u is

\operatorname{net}_u(s)=\sum_j W_{uj}x_j.

updateAt p s u changes only coordinate u, using

x_u'= \begin{cases} +1,&\theta_u\leq\operatorname{net}_u(s),\\ -1,&\operatorname{net}_u(s)<\theta_u. \end{cases}

The non-strict comparison fixes a detail often omitted on paper: ties go to +1. That convention becomes important in the convergence proof.

The energy is

E(s) =-\frac12\sum_i\sum_j W_{ij}x_i x_j +\sum_i\theta_i x_i.

The factor of one half is why the scalar has to be more than a ring:

@energy : {α : Type} → [Field α] → {n : ℕ} → Params α n → State n → α

Rat supplies this field structure and supports exact executable arithmetic. It therefore lets the experiments below evaluate the energy without rounding.

Under symmetric weights and zero diagonal,

W_{ij}=W_{ji}, \qquad W_{ii}=0,

the theorem energy_updateAt_le proves

E(\operatorname{updateAt}(p,s,u))\leq E(s).

@energy_updateAt_le : ∀ {n : ℕ} (p : Params ℝ n),
  SymmetricW p → DiagonalZero p → ∀ (s : State n) (u : Fin n), energy p (updateAt p s u) ≤ energy p s

Params allows arbitrary weights; SymmetricW and DiagonalZero restrict the networks covered by the theorem. This separation also lets us execute asymmetric networks and examine where the energy argument fails.

The proof expands the quadratic energy difference. Symmetry makes the changed row and column contribute the same net-input term, while the zero diagonal removes the self-interaction. When the coordinate changes and the net input is not tied with the threshold, energy_updateAt_lt_of_change_of_ne strengthens the inequality to a strict decrease.

Writing the old and new activations at the changed coordinate as x_u and x'_u, the cancellation gives

E(s')-E(s)=(x'_u-x_u)(\theta_u-\operatorname{net}_u(s)).

If a negative activation becomes positive, the first factor is two and the threshold comparison makes the second nonpositive. If a positive activation becomes negative, the first factor is minus two and the second is positive. Both cases give a nonpositive product. A tied negative activation can become positive with the second factor zero, explaining why an actual state change need not decrease energy strictly. This calculation tells us exactly where the tie example and the secondary progress measure enter the argument.

Two-Neuron Hopfield Updates🔗

Start with two mutually excitatory neurons, zero thresholds, and initial state [+1,-1]. Each neuron receives the other neuron's activation with weight one:

The states before and after updating neuron 1:

[true, false]

[true, true]

And their energies:

1

-1

Neuron 1 receives net input +1, so its activation changes from -1 to +1. The two off-diagonal products in the energy change from negative to positive, lowering the exact rational energy from 1 to -1. Changing W 0 1 without changing W 1 0 still produces an executable state sequence, but it prevents use of energy_updateAt_le: Lean asks for SymmetricW p. Setting a diagonal weight to a nonzero value similarly leaves the program runnable while invalidating the theorem's DiagonalZero p premise.

Energy Ties And Convergence🔗

If every state change strictly lowered energy, finiteness would immediately rule out cycles. Ties make the argument subtler. With the convention “ties go to +1,” a state may change while energy stays equal. TorchLean therefore uses the number of positive neurons,

\operatorname{pluses}(s) =|\{i\mid s_i=\texttt{true}\}|,

as a secondary progress measure. For one full cyclic sweep, cycleUpdate_progress proves:

• either energy strictly decreases;

• or energy is unchanged and pluses strictly increases.

@cycleUpdate_progress : ∀ {n : ℕ} (p : Params ℝ n),
  SymmetricW p →
    DiagonalZero p →
      ∀ (s : State n),
        cycleUpdate p s ≠ s →
          energy p (cycleUpdate p s) < energy p s ∨
            energy p (cycleUpdate p s) = energy p s ∧ pluses (cycleUpdate p s) > pluses s

The second case occurs when all weights and thresholds are zero, so every net input ties with its threshold:

The state changes, because a tie resolves to +1:

[false, false]

[true, false]

Every term in the energy has a zero coefficient, so both energies are zero:

0

0

The positive count increases even though the energy stays fixed:

0

1

This single-coordinate example exhibits equal energy with an increased positive count. A strict comparison would instead send ties to -1: this initial state would stay fixed, but tied positive states could still change at equal energy. Such a convention needs the opposite count as its secondary measure. Keeping the previous activation on ties would avoid tie-induced changes.

The lexicographic pair

\bigl(E(s),-\operatorname{pluses}(s)\bigr)

therefore progresses whenever a sweep changes the state. Since State n is finite, cycleUpdate_no_nontrivial_cycles rules out a nontrivial cycle, and cycleUpdate_exists_fixedpoint_le_card gives a fixed point within at most Fintype.card (State n) sweeps. The more explicit cycleUpdate_exists_fixedpoint_le_pow states the corresponding 2^n bound.

The following declarations expose the strict-decrease lemma, the exclusion of cycles, and the two fixed-point bounds:

@cycleUpdate_exists_fixedpoint_le_pow : ∀ {n : ℕ} (p : Params ℝ n),
  SymmetricW p → DiagonalZero p → ∀ (s0 : State n), ∃ m ≤ 2 ^ n, (f p)^[m + 1] s0 = (f p)^[m] s0

(f p)^[m] is Mathlib's iterated-function notation, so the conclusion reads: within 2^n sweeps, one more sweep changes nothing. The _le_card variant says the same thing with Fintype.card (State n) in place of 2^n; the explicit power is the one to quote, and the cardinality form is the one the proof actually produces.

A decreasing real sequence need not reach its limit after finitely many steps. What makes this argument terminate is that the energy and count are evaluated on a finite set of states. Before a fixed point is reached, a repeated state would close a cycle, contradicting the progress result. There are only 2 ^ n possible Boolean functions, so enough distinct sweep states exhaust the possibilities. The existential ∃ m ≤ 2 ^ n supplies a stopping index, and the equality compares successive iterates at that index. It does not say that the fixed point is unique, nor that every starting state reaches the same one.

These are theorems about asynchronous coordinate updates arranged into cyclic sweeps. They do not apply automatically to synchronous updates, stochastic schedules, modern continuous-state Hopfield layers such as the one of Ramsauer et al. (2021), or a floating-point kernel. Each variation needs its own transition relation and energy argument.

Hebbian Storage And Recall🔗

To use the dynamics as an associative memory, store a pattern \xi\in\{-1,+1\}^n by the Hebbian outer product

W_{ij}=\xi_i\xi_j\ (i\neq j), \qquad W_{ii}=0, \qquad \theta=0,

which is symmetric and has zero diagonal. These are the weight conditions needed by the real convergence theorem. The following rational experiment uses the same construction with four neurons, storing (+1,+1,-1,-1):

noisy is the stored pattern with one bit wrong. One sweep repairs it:

[true, false, false, false]

[true, true, false, false]

true

The energy decreases and the positive count increases in this run. Strict energy decrease is already sufficient for progress; the theorem only needs the count when the energy stays equal:

0

-6

1

2

For a single stored pattern, the energies can be calculated from its overlap with the current state. The double sum collapses because \sum_{i,j}\xi_i\xi_jx_ix_j=(\xi\cdot x)^2 and the zero diagonal removes the n self terms:

E(s)=\frac{n-(\xi\cdot x)^2}{2}.

With n=4, the pattern itself has \xi\cdot x=4 and energy (4-16)/2=-6, while noisy has \xi\cdot x=2 and energy 0. The formula also says what the minima are: energy is smallest exactly when |\xi\cdot x| is largest, which happens at x=\xi and at x=-\xi. For this zero-threshold, single-pattern network, both patterns are stable, as checked here:

-6

true

true

stable is IsStable from the spec, evaluated: no single-coordinate update changes the state. Both \xi and -\xi pass it. Since State 4 has sixteen inhabitants, we can enumerate every initial state and check where one sweep takes it:

true

8

8

Every one of the sixteen states is at a fixed point after a single sweep, and eight states reach each attractor.

cycleUpdate_exists_fixedpoint_le_pow promises a fixed point within 2^n=16 sweeps; this network needs one. The bound counts states because its proof uses finiteness and lexicographic progress. It does not analyze the particular weights or update order that make this example converge quickly. A sharper bound for a family of networks would need that additional analysis.

The three outputs of hebbBasins answer three different questions. The Boolean asks whether every enumerated start is stable after one sweep. The two natural numbers count starts whose result equals each named pattern. Here allStates decodes all four-bit integers, so its sixteen entries cover this state space rather than a sample of it. The split of eight and eight is a cardinality statement. Interpreting it as a fifty-percent recall probability would require choosing a uniform distribution on those starts. A noise process concentrated near the stored pattern could have a different recall probability even with exactly the same dynamics.

The theorem guarantees that the sweep sequence stops, but does not identify the final state. Half of these starts recover \xi and half recover -\xi, and for a memory with several stored patterns there are spurious mixture states too. Convergence and correct recall are different claims, and only the first one is proved here.

[[0, 2, -2, 0], [2, 0, -2, 0], [-2, -2, 0, 0], [0, 0, 0, 0]]

-6

-6

false

true

[true, true, false, true]

12

16

2

# Mutate coordinates in order so each neuron reads the
# preceding updates in the same sweep.
import torch

xi = torch.tensor([1., 1., -1., -1.])
W = torch.outer(xi, xi)
W.fill_diagonal_(0.)

x = torch.tensor([1., -1., -1., -1.])
for u in range(4):
    x[u] = 1.0 if W[u] @ x >= 0 else -1.0

assert torch.equal(x, xi)

[[true, true], [true, false], [false, true], [true, false], [false, true]]

-1

1

[[true, true], [false, false], [true, true], [false, false]]

[[true, true], [false, true], [false, true], [false, true]]

Exact ReLU Network Algebra🔗

The approximation developments use exact ReLU identities to assemble larger networks. The module ReLUMlpBridge proves

\operatorname{ReLU}(u)-\operatorname{ReLU}(-u)=u.

In Lean:

relu_sub_relu_neg : ∀ (u : ℝ),
  NN.MLTheory.Proofs.UniversalApproximation.relu u - NN.MLTheory.Proofs.UniversalApproximation.relu (-u) = u

The fully qualified relu in that output is the definition used by the approximation development. Reusing that definition lets these real-valued lemmas compose without an additional equivalence lemma.

Since relu u is max u 0, one split on the sign of the input proves the identity:

le_total 0 u produces the two possible order relations, including equality in both branches. In the first branch, h proves that the positive hinge equals u, while neg_nonpos.mpr h proves that the other hinge is zero. In the second, the roles reverse and subtracting -u recovers u. The proof therefore covers zero without an extra exceptional case. Each rewrite names the order fact that permits selecting an argument of max.

In relu u - relu (-u) one of the two operands is always the exact zero, so for finite IEEE values the result has the same numerical value, including at zero. Bitwise signed-zero preservation is a separate question:

2.500000

[true, true, true, true, true, true]

Lean's Float is binary64, and the list covers zero, magnitudes that would be subnormal in binary32, a decimal that no binary format stores exactly, and a magnitude near the binary32 maximum. These comparisons use exact numerical equality: x - 0 and 0 - x are exact for every finite x in every IEEE 754 format, so the identity holds in binary32 and binary16 for the same reason it holds here. These tests do not establish a bitwise identity for signed zero or NaNs, nor do they extend the real theorem to a backend without a refinement argument. This identity lets a ReLU network carry an affine term exactly even though each hidden unit clips negative values. Two units retain its positive and negative parts; subtracting their outputs recovers the affine term. The bounded-box multiplication construction uses this identity:

@relu_mul_universal_approximation_box : ∀ {M : ℝ},
  0 < M → ∀ ε > 0, ∃ hidDim l1 l2, ∀ x ∈ box M, |mulFun x - mlpEval l1 l2 x| < ε

The assumption 0 < M specifies a nondegenerate bounded box. A finite ReLU network is piecewise affine; along the diagonal of \mathbb R^2, multiplication grows quadratically. Its error therefore cannot remain uniformly small on the whole plane. Restricting the domain to a box makes the stated approximation possible.

The construction reduces multiplication to two one-dimensional square approximations through uv=((u+v)^2-(u-v)^2)/4. If |u|,|v|\leq M, both arguments of the square lie in [-2M,2M], which is why a bounded input box gives a common interval for the two approximants. The source chooses square error below 2\varepsilon for each occurrence. Subtraction adds the two absolute-error bounds, and division by four leaves error below \varepsilon. The returned layers have input dimension two and output dimension one; hidDim records the width needed to combine the constructions. This is a concrete way that a scalar approximation lemma becomes a component for a model with several input features.

Read the existential witnesses in order: Lean first chooses the hidden dimension, then two layers whose types use that dimension. Only after those choices does the statement quantify over inputs in box M. A proof cannot satisfy it by selecting a new network for each input point. The same returned pair of layers must meet the error budget throughout the entire box.

relu_mul_universal_approximation_box uses this algebra inside a uniform approximation argument. For its construction, quantitative hypotheses, and the distinction between existence, checkpoint verification, and finite-precision execution, return to Approximation Theory.

Causality In State-Space Models🔗

A recurrent sequence model should not revise an earlier output after future tokens arrive. For a simple state-space recurrence,

h_{t+1}=A_t h_t+B_t x_t,\qquad y_t=C_t h_{t+1}+D_t x_t,

the causal claim can be phrased without derivatives or probability:

\operatorname{take}_{|xs|} \bigl(\operatorname{outputs}(\operatorname{run}(xs\mathbin{++}ys))\bigr) = \operatorname{outputs}(\operatorname{run}(xs)).

The theorem says that appending a future suffix ys preserves every output already produced for the prefix xs.

MambaCausality proves this statement for three increasingly rich specifications, following the selective state-space construction of Gu and Dao (2024):

• DiagonalS4Spec, the diagonal case of the structured state space of Gu et al. (2022);

• MambaBlockSpec;

• SelectiveMambaBlockSpec, including its carried convolution history.

The selective theorem includes both recurrent state and convolution history. The following example states its prefix equality and proves it by applying the library theorem:

The five dimensions are arbitrary natural numbers. The scalar type needs Storage and Context instances, which provide the tensor representation and operations used by the specification. The same statement therefore covers Float, Rat, and ℝ instances.

Its content is one equation. runArray returns the final recurrent state together with the array of outputs, and the statement is about the outputs component: run the block on xs ++ ys, keep the first xs.size outputs, and you get exactly what running it on xs alone produces. Appending future tokens cannot disturb an earlier output.

The example declaration is itself a proposition whose proof is the named theorem on its final line. There is no by block because applying that theorem already produces a term of exactly the required equality type. Square-bracketed arguments such as [Context α] are instances Lean supplies from the scalar type, while m, h0, xs, and ys are the actual model and data. The same m and h0 occur on both sides. Comparing two runs that also change the initial state would be a different statement: earlier outputs can depend on that state even when they cannot depend on a later suffix.

The theorem is polymorphic over any scalar α with a TorchLean Context. Its proof is structural: induct on xs, unfold one recurrent step, and apply the induction hypothesis to the updated state and history. It does not require commutative or exact arithmetic because causality depends on evaluation order, not algebraic rearrangement.

The selective block's causal convolution needs a window of recent inputs, so the internal runner threads a newest-first history alongside the recurrent state. That runner is where the induction happens, and it is stated separately:

The public theorem above is the history := #[] instance of this one, obtained by simpa [Models.SelectiveMambaBlockSpec.runArray]. A streaming implementation may resume with earlier inputs still in its convolution window; the history theorem covers that case.

A carried history is part of the starting configuration, just like the recurrent tensor. runArrayWithHistory compares runs with the same history on both sides, so a previously buffered input may affect an early convolution output in both runs. The induction can keep this invariant because one step consumes the current token and passes the updated state and history to the next step. No step receives the unprocessed suffix as an additional argument. This identifies what a streaming implementation must preserve when splitting a sequence into chunks: dropping or reordering the history changes the initial configuration to which the theorem applies.

The reusable array argument is factored through Scan, which proves append and prefix laws for state-threading scans. MambaCausality instantiates that structure with the S4/Mamba state and convolution history; it does not assert that an optimized selective-scan kernel refines the specification.

The two simpler specifications satisfy the same output equation with a smaller state:

Both equations compare the output prefix in the same way; the state shape and the spec structure change. DiagonalS4Spec carries a single [stateDim] vector, MambaBlockSpec adds the selection projections but keeps the same state shape, and the selective block above is the one that grows to [innerDim, stateDim] plus a history.

The prefix length matters: the next output may depend on the first token of the suffix. To see this, take an S4 block with one channel, A = B = C = 1, D = 0, and unit projections. Its state accumulates the inputs, so output t is the running total of tokens 0 through t.

#[1.000000, 3.000000, 8.000000]

#[1.000000, 3.000000, 12.000000]

true

false

The two futures follow the same prefix #[1.0, 2.0]. The first two outputs agree, 1.0 and 1.0 + 2.0. The third does not: 1 + 2 + 5 = 8 against 1 + 2 + 9 = 12. So .take 2, which is .take xs.size, matches the prefix-only run, while .take 3, which is .take (xs.size + 1), differs across the two futures.

Using zero-based indices, output xs.size is the first output that may depend on the suffix. The theorem fixes all earlier outputs. Extending the equality by one position would fail in this accumulator example.

# Compare outputs for one shared prefix under the same model
# and starting configuration.
t = 8
y_short = model(x[:, :t])
y_long = model(x)
torch.testing.assert_close(y_long[:, :t], y_short)

Proof Boundary🔗

The three developments establish different kinds of structure:

The Hopfield example executes over Rat; the energy theorem is stated over ℝ. The Mamba causality theorem works over an abstract Context, but a runtime refinement theorem is still needed to connect a backend kernel to the spec runner. The ReLU theorem constructs real-valued layers, while quantization and rounded execution require the finite-precision bridge described in the approximation chapter.

A backend proof can use these results once it establishes that the relevant executable operation implements the specification, with any arithmetic error accounted for.