§5.7, side-note p. 93 — equivariance under an s-step left shift

Proved

GeomDL.RNN.shift_equivariant_s_steps

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 any RNN update map, $h_0\in\mathbb R^m$ its seed, and $\bar z$ an input sequence padded on the left by $d$ zero vectors. If $0\le s\le d$ and $R(0,h_0)=h_0$ , then the RNN run on the sequence shifted left by $s$ steps is the correspondingly shifted original run:

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

This extends the one-step statement to all shifts that fit inside the zero padding.

Formalization Note Time is indexed by natural numbers, and the original input begins at time $1$ ; its value at time $0$ is unused.

Preamble

import Mathlib
import Definitions.Def_GeomDL_RNN_Recurrence

Formal statement

namespace GeomDL.RNN

/-- The side-note on p. 93: padding by at least `s` permits an `s`-step left shift. -/
theorem shift_equivariant_s_steps {k m : ℕ}
    (R : (Fin k → ℝ) → (Fin m → ℝ) → (Fin m → ℝ))
    (h0 : Fin m → ℝ) (z : ℕ → Fin k → ℝ)
    (delay s : ℕ) (hpad : s ≤ delay) (hfix : R 0 h0 = h0) :
    ∀ t : ℕ,
      run R h0 (fun u => pad delay z (u + s)) t =
        run R h0 (pad delay z) (t + s) := by sorry

end GeomDL.RNN

Source

Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), §5.7, side-note, 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