§5.7, p. 93 — a fixed-point seed makes a padded RNN shift-equivariant

Proved

GeomDL.RNN.shift_equivariant_of_fixed_point

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

equivariancegeometric-deep-learningp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1recurrent-neural-network

Let $R:\mathbb R^k\times\mathbb R^m\to\mathbb R^m$ be an RNN update map, and pad an input sequence $z$ on the left with $d\ge1$ zero vectors to obtain $\bar z$ . If the common seed $h_0$ of both runs is a fixed point of the zero-input update, $R(0,h_0)=h_0$ , then

h_{\bar z(\cdot+1)}(t)=h_{\bar z}(t+1)\qquad\text{for every }t\ge0.

This is the boundary condition under which an RNN commutes with a one-step left shift of a padded input.

Formalization Note The claim includes $t=0$ . The book's $z(1)$ is Lean's input at index $1$ , with $z(0)$ unused.

Preamble

import Mathlib
import Definitions.Def_GeomDL_RNN_Recurrence

Formal statement

namespace GeomDL.RNN

/-- The one-step left-shift equivariance on p. 93. -/
theorem shift_equivariant_of_fixed_point {k m : ℕ}
    (R : (Fin k → ℝ) → (Fin m → ℝ) → (Fin m → ℝ))
    (h0 : Fin m → ℝ) (z : ℕ → Fin k → ℝ)
    (delay : ℕ) (hpad : 1 ≤ delay) (hfix : R 0 h0 = h0) :
    ∀ t : ℕ,
      run R h0 (fun u => pad delay z (u + 1)) t =
        run R h0 (pad delay z) (t + 1) := by sorry

end GeomDL.RNN

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §5.7, paragraph following equations (40)–(41), p. 93

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph