§5.7, p. 92 — an unpadded RNN need not commute with a left shift

Proved

GeomDL.RNN.unpadded_shift_failure

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

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

A left shift of an input sequence need not shift an RNN's hidden-state sequence by the same amount. There exist a scalar input sequence $z$ , a scalar hidden-state seed $h_0$ , and an update map $R:\mathbb R\times\mathbb R\to\mathbb R$ such that, with $z'(t)=z(t+1)$ ,

h_{z'}(1)\ne h_z(2).

Here each run starts from the same seed and follows $h(0)=h_0$ , $h(t+1)=R(z(t+1),h(t))$ . This counterexample records the boundary obstruction identified by equations (40)–(41).

Preamble

import Mathlib
import Definitions.Def_GeomDL_RNN_Recurrence

Formal statement

namespace GeomDL.RNN

/-- Equations (40)–(41), p. 92: an unpadded left shift need not be equivariant. -/
theorem unpadded_shift_failure :
    ∃ (R : (Fin 1 → ℝ) → (Fin 1 → ℝ) → (Fin 1 → ℝ))
      (z : ℕ → Fin 1 → ℝ) (h0 : Fin 1 → ℝ),
      run R h0 (fun t => z (t + 1)) 1 ≠ run R h0 z 2 := by sorry

end GeomDL.RNN

Source

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

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