TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Group cross-correlation and compatible layers are equivariant

Statement

Let $G$ be a discrete group acting on the left on the square lattice $Z^{2}$ , and let feature maps take values in finite-dimensional row-vector channel spaces. Assume every group or lattice sum below has finite support or converges absolutely in each output coordinate. For group-indexed features $f : G \to R^{C_{i n}}$ and a matrix-valued filter $Ψ : G \to R^{C_{i n} \times C_{o u t}}$ , group-to-group cross-correlation satisfies

C_{Ψ} (L_{u} f) = L_{u} (C_{Ψ} f) (u \in G) .

For an image feature map $f : Z^{2} \to R^{C_{i n}}$ and a lattice filter $Ψ : Z^{2} \to R^{C_{i n} \times C_{o u t}}$ , the first-layer image-to-group cross-correlation also satisfies

E_{Ψ} (L_{u} f) = L_{u} (E_{Ψ} f) (u \in G),

where the input action is induced by the action on $Z^{2}$ and the output action is the left action on maps on $G$ . The bias-free sum in the ordinary full-lattice, unit-stride discrete layer with origin $a = 0$ is the translation-group instance of this formula; any fixed origin shift and the layer's constant output bias preserve translation equivariance. Componentwise pointwise nonlinearities and finite-neighborhood max pooling without subsampling commute with the left action. Restricting a group feature map to a subgroup $H \leq G$ preserves $H$ -equivariance; for finite $H$ , left-coset max pooling produces a $G$ -equivariant feature map on $G / H$ , and when $H = G$ is finite it is invariant. Finite compositions of equivariant layers remain equivariant.

The full p4 and p4m lattice symmetry groups are infinite because they contain all integer translations; no finiteness assumption on $G$ is made. On a finite grid, the theorem applies only when the domain, output sampling, and boundary convention respect the stated actions. Arbitrary cropping, padding, or stride need not do so. No continuous-rotation, universal-approximation, or empirical-superiority claim follows.

Statement references

group axioms and inverses

left group actions

the generic intertwining condition

functions and declared domains/codomains

left actions on feature maps

the discrete layer and boundary conventions

equivariant neural layers

group and image-to-group correlation

pointwise and pooling operators

subgroups

left cosets

the p4 and p4m lattice groups

Cohen and Welling, “Group Equivariant Convolutional Networks,” §§2, 4–6 and Appendix A

Goodfellow, Bengio, and Courville, Deep Learning, Chapter 9 §§9.1–9.5

Equivariance diagram

For each $u \in G$ , this square records the equation $Φ \circ T_{u} = T_{u}^{'} \circ Φ$ : the vertical maps act on input and output feature spaces, respectively. It is a notation summary; the convolution claims below are proved by direct reindexing.

diagram failed to render:
\begin{tikzcd}
X \arrow[r,"\Phi"] \arrow[d,"T_u"'] & Y \arrow[d,"T'_u"] \\
X \arrow[r,"\Phi"'] & Y
\end{tikzcd}

Facts & Assumptions

Given: The group actions, feature maps, filters, finite-support or absolute-convergence conditions, and operators stated above. Prove the equivariance claims and the composition rule.

[F1]

Left group actions, transitive actions, and faithful actions: A left action satisfies $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ for every $g, h$ and acted-on point $x$ .

[F2]

Group and abelian group: Group multiplication is associative and each element has a two-sided inverse.

[F3]

The left action on feature maps induced by an action on sites: The induced action is $(L_{u} f) (x) = f (u^{- 1} \cdot x)$ , and on group-indexed maps $(L_{u} F) (g) = F (u^{- 1} g)$ .

[F4]

First-layer and group-to-group cross-correlation: Group-to-group correlation is $(C_{Ψ} f) (g) = \sum_{h \in G} f (h) Ψ (g^{- 1} h)$ when the sum is finite or absolutely convergent.

[F5]

First-layer and group-to-group cross-correlation: Image-to-group correlation is $(E_{Ψ} f) (g) = \sum_{x \in Z^{2}} f (x) Ψ (g^{- 1} \cdot x)$ when the sum is finite or absolutely convergent.

[F6]

Pointwise nonlinearities, neighborhood pooling, subgroup sampling, and coset pooling: Pointwise maps act componentwise, $N_{ν} F (g)_{c} = ν (F (g)_{c})$ , and non-strided pooling is $(P_{U} F) (g)_{c} = \max_{v \in U} F (g v)_{c}$ for finite nonempty $U$ . For a finite subgroup $H \leq G$ , left-coset pooling is $Q_{H} F : G / H \to R^{C}$ , where $G / H = {g H : g \in G}$ and $(Q_{H} F) (g H)_{c} = \max_{h \in H} F (g h)_{c}$ ; the induced left action on the index set is $a \cdot (g H) = (a g) H$ .

[F7]

Equivariant neural layers between group-action feature spaces: Equivariance between input and output actions is $Φ (T_{g} x) = T_{g}^{'} Φ (x)$ for every $g$ and $x$ .

[F8]

Discrete convolutional layer with local receptive fields, channel mixing, stride, and padding: The discrete layer uses a finite offset set $K$ and computes $y (p) = b + \sum_{δ \in K} \tilde{x} (a + s ⊙ p + δ) W_{δ}$ with the declared extension and stride.

[F9]

The p4 and p4m square-lattice symmetry groups: The full p4 and p4m groups contain every translation $(t, I)$ for $t \in Z^{2}$ and are infinite.

[F10]

Equivariant maps and isomorphisms of group actions: An equivariant map between $G$ -sets satisfies $f (g \cdot x) = g \cdot f (x)$ for every $g$ and $x$ .

[F11]

Subgroup: A subgroup contains the identity and is closed under the group operation and inverses.

[F12]

Left and right cosets $g H$ and $H g$ of a subgroup: The left coset of $H$ represented by $g$ is $g H = {g h : h \in H}$ .

Proof

1.1givenF1F2F3F4algebra

For group-to-group correlation, $(C_{Ψ} (L_{u} f)) (g) = \sum_{h \in G} f (u^{- 1} h) Ψ (g^{- 1} h)$ . Reindex by the bijection $h = u k$ to obtain $\sum_{k \in G} f (k) Ψ (g^{- 1} u k)$ . The identity $(u^{- 1} g)^{- 1} = g^{- 1} u$ follows because both products of $u^{- 1} g$ and $g^{- 1} u$ are $e$ by associativity and the two-sided inverse laws; two two-sided inverses $a, b$ of $z$ coincide since $a = a (z b) = (a z) b = b$ . Hence the sum is $\sum_{k \in G} f (k) Ψ ((u^{- 1} g)^{- 1} k) = (C_{Ψ} f) (u^{- 1} g) = (L_{u} (C_{Ψ} f)) (g)$ . The reindexing is valid for finite support or absolute convergence.

1.2givenF3F6algebra

For every channel $c$ , $(N_{ν} (L_{u} F)) (g)_{c} = ν (F (u^{- 1} g)_{c}) = (L_{u} (N_{ν} F)) (g)_{c}$ . Likewise, $(P_{U} (L_{u} F)) (g)_{c} = \max_{v \in U} F (u^{- 1} g v)_{c} = (P_{U} F) (u^{- 1} g)_{c} = (L_{u} (P_{U} F)) (g)_{c}$ . Thus both operators commute with the left action.

1.3givenF3F6F11F12algebra

For $a \in H$ and $h \in H$ , $(R_{H} (L_{a} F)) (h) = F (a^{- 1} h) = (L_{a} (R_{H} F)) (h)$ because $a^{- 1} h \in H$ by [F11]; this proves only $H$ -equivariance after subgroup restriction. For finite $H$ and arbitrary $a \in G$ , $(Q_{H} (L_{a} F)) (g H)_{c} = \max_{h \in H} F (a^{- 1} g h)_{c} = (Q_{H} F) ((a^{- 1} g) H)_{c} = (L_{a}^{G / H} (Q_{H} F)) (g H)_{c}$ , using the left-coset indexing in [F12] and the action stated in [F6]. If $H = G$ is finite then $G / H$ is a singleton, whose action is trivial, so the output is invariant.

2.1givenF1F2F3F5F8step 1.1algebra

For the first-layer operation, $(E_{Ψ} (L_{u} f)) (g) = \sum_{x \in Z^{2}} f (u^{- 1} \cdot x) Ψ (g^{- 1} \cdot x)$ . The map $x = u \cdot y$ is a bijection of $Z^{2}$ with inverse $y = u^{- 1} \cdot x$ by [F1], so reindexing gives $\sum_{y \in Z^{2}} f (y) Ψ (g^{- 1} \cdot (u \cdot y)) = \sum_{y \in Z^{2}} f (y) Ψ ((g^{- 1} u) \cdot y) = (E_{Ψ} f) (u^{- 1} g) = (L_{u} (E_{Ψ} f)) (g)$ , using the inverse identity in 1.1. Absolute convergence or finite support justifies the reindexing. For $G = Z^{2}$ acting by translations, $Ψ (δ) = W_{δ}$ with finite support, full-lattice input and output domains, unit stride, and origin $a = 0$ , setting $x = p + δ$ identifies the sum in this formula with the cross-correlation term of the layer in [F8]. For any fixed origin $a$ , that sum is instead $(E_{Ψ} f) (p + a)$ , which remains translation-equivariant because translations of $Z^{2}$ commute. The layer's output bias is constant across $p$ , so the induced translation action fixes it; adding it preserves equivariance of the full layer.

3.1givenF7F8F9F10step 1.1step 1.2step 1.3step 2.1algebra∎

If $Φ$ and $Ψ$ are equivariant maps for compatible input, intermediate, and output actions, then $(Ψ \circ Φ) (T_{g} x) = Ψ (T_{g}^{'} Φ (x)) = T_{g}^{''} (Ψ \circ Φ) (x)$ by [F7] and [F10]; induction gives equivariance of any finite stack. The reindexings in steps 1.1 and 2.1 require actual group actions on the full index sets, while [F8] permits arbitrary finite-grid boundary and stride choices; therefore those choices are covered only when compatible with the actions. In particular [F9] shows no finite-group assumption was used for p4 or p4m.

Depends on

Used by

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Taco S. Cohen and Max Welling, Group Equivariant Convolutional Networks (standard reference, not scraped)
Ian Goodfellow, Yoshua Bengio, and Aaron Courville, Deep Learning (standard reference, not scraped)