Pipeline-generated

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.

✓ 4 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Convolution and finite-group equivariance

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Discrete convolutional layer with local receptive fields, channel mixing, stride, and padding

Definition

Let $D, O \subseteq Z^{2}$ be input and output index sets, let $C_{i n}, C_{o u t}$ be positive integers, and let $x : D \to R^{C_{i n}}$ assign a row vector of input channels to each input site. A boundary extension is a function $\tilde{x} : Z^{2} \to R^{C_{i n}}$ whose restriction to $D$ is $x$ ; zero padding is the extension that is zero off $D$ . Choose a finite receptive-field offset set $K \subseteq Z^{2}$ , a positive integer stride vector $s \in Z_{> 0}^{2}$ , an origin $a \in Z^{2}$ , one matrix $W_{δ} \in R^{C_{i n} \times C_{o u t}}$ for each $δ \in K$ , and an output bias row vector $b \in R^{C_{o u t}}$ . The discrete convolutional layer is the map $y : O \to R^{C_{o u t}}$ given by

y (p) = b + \sum_{δ \in K} \tilde{x} (a + s ⊙ p + δ) W_{δ} (p \in O),

where $s ⊙ p$ is coordinatewise multiplication. Thus each output uses only the input sites in its receptive field, mixes input channels by matrix multiplication, and uses the same weights and bias at every output site. With unit stride on the full lattice and no boundary truncation, this formula is a discrete cross-correlation; many machine-learning software packages call it convolution. Mathematical convolution instead reverses the kernel offsets. The choices of $O$ , the extension $\tilde{x}$ , and the stride specify cropping, padding, and subsampling, and need not preserve a symmetry of the full lattice.

Definition references

functions and declared domains/codomains

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

Cohen and Welling, “Group Equivariant Convolutional Networks,” §5

DefinitionDefinition: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The left action on feature maps induced by an action on sites

Definition

Let $G$ be a group acting on the left on a set $S$ , and let $V$ be a set of feature values. A feature map is a function $f : S \to V$ . For $u \in G$ , the induced transformation of feature maps is

(L_{u} f) (x) = f (u^{- 1} \cdot x) (x \in S) .

It is a left action on the set of feature maps: the group acts by reindexing sites and leaves the feature values unchanged. In particular, for maps $F : G \to V$ on the group itself with its left multiplication action, $(L_{u} F) (g) = F (u^{- 1} g)$ .

Definition references

left action of a group on a set

functions and declared domains/codomains

Cohen and Welling, “Group Equivariant Convolutional Networks,” §4.4, Eqs. (4)–(5)

Goodfellow, Bengio, and Courville, Deep Learning, Chapter 9 §9.2

Facts & Assumptions

Given: A group $G$ acts on the left on a set $S$ , and $f : S \to V$ is a feature map. Verify that the displayed transformations form a left action.

[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 \in G$ and $x \in S$ .

[F2]

Group and abelian group: A group operation is associative, has an identity, and every element has a two-sided inverse.

Proof

1.1givenF1algebra

For each $x \in S$ , $(L_{e} f) (x) = f (e^{- 1} \cdot x) = f (x)$ by the identity law in [F1], so $L_{e} f = f$ .

2.1givenF1F2algebra∎

For $u, v \in G$ , the element $v^{- 1} u^{- 1}$ is a two-sided inverse of $u v$ , since $(u v) (v^{- 1} u^{- 1}) = u (v v^{- 1}) u^{- 1} = e$ and $(v^{- 1} u^{- 1}) (u v) = v^{- 1} (u^{- 1} u) v = e$ . Two two-sided inverses $a, b$ of an element $z$ coincide because $a = a (z b) = (a z) b = b$ ; hence $(u v)^{- 1} = v^{- 1} u^{- 1}$ . Therefore, for each $x \in S$ , $(L_{u} (L_{v} f)) (x) = f (v^{- 1} \cdot (u^{- 1} \cdot x)) = f ((v^{- 1} u^{- 1}) \cdot x) = f ((u v)^{- 1} \cdot x) = (L_{u v} f) (x)$ by [F1]. Thus $L_{u} L_{v} = L_{u v}$ .

DefinitionDefinition: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The p4 and p4m square-lattice symmetry groups

Definition

Let $ρ = (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array})$ be the quarter-turn matrix and $σ = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ a reflection matrix. Let $C_{4} = {ρ^{j} : j = 0, 1, 2, 3}$ and $D_{4} = {ρ^{j}, ρ^{j} σ : j = 0, 1, 2, 3}$ , with matrix multiplication. For $A = C_{4}$ or $D_{4}$ , define $P_{A} = Z^{2} \times A$ with multiplication

(t, M) (s, N) = (t + M s, M N) .

Each pair $(t, M)$ acts on lattice sites by $x \mapsto M x + t$ . The p4 lattice-symmetry group is $P_{C_{4}}$ , generated by integer translations and quarter-turns. The p4m lattice-symmetry group is $P_{D_{4}}$ , generated by integer translations, quarter-turns, and reflections. The point groups $C_{4}$ and $D_{4}$ have four and eight elements, respectively, but both full groups are infinite because they contain every integer translation.

Definition references

group axioms

left actions of groups on sets

functions and declared domains/codomains

Cohen and Welling, “Group Equivariant Convolutional Networks,” §§4.1–4.3

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

Facts & Assumptions

Given: The matrices $ρ, σ$ , the sets $C_{4}, D_{4}$ , and the pair multiplication displayed in the Definition. Prove that these are groups acting on $Z^{2}$ , and that the full groups are infinite.

[F1]

Group and abelian group: A group operation is associative, has an identity, and every element has a two-sided inverse.

[F2]

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 \in G$ and $x$ in the acted-on set.

Proof

1.1givenF1algebra

The matrices satisfy $ρ^{4} = I$ , $σ^{2} = I$ , and $σ ρ σ = ρ^{- 1}$ . The rotation matrices are $I, ρ, - I, - ρ$ , hence distinct; their products add exponents modulo $4$ , and $(ρ^{j})^{- 1} = ρ^{- j}$ . The four matrices $σ, ρ σ, - σ, - ρ σ$ are distinct, have determinant $- 1$ , and differ from the rotations, which have determinant $1$ . Thus $C_{4}$ has four elements and $D_{4}$ has eight. Writing elements of $D_{4}$ as $ρ^{j} σ^{ϵ}$ with $ϵ \in {0, 1}$ , the relation $σ ρ^{j} = ρ^{- j} σ$ shows products stay in $D_{4}$ , and $(ρ^{j} σ^{ϵ})^{- 1} = ρ^{- (- 1)^{ϵ} j} σ^{ϵ}$ also lies in $D_{4}$ . Both matrix groups preserve $Z^{2}$ because $ρ$ and $σ$ are signed permutation matrices.

2.1givenF1step 1.1algebra

For either matrix group $A$ , the pair multiplication is closed on $Z^{2} \times A$ . It is associative because both parenthesizations of three factors $(t, M), (s, N), (r, Q)$ equal $(t + M s + M N r, M N Q)$ . Its identity is $(0, I)$ . For every pair $(t, M)$ , the pair $(- M^{- 1} t, M^{- 1})$ belongs to the same set by 1.1, and $(t, M) (- M^{- 1} t, M^{- 1}) = (0, I) = (- M^{- 1} t, M^{- 1}) (t, M)$ . Thus $P_{C_{4}}$ and $P_{D_{4}}$ satisfy the group axioms in [F1].

3.1givenF2step 2.1algebra∎

The identity pair acts identically because $(0, I) \cdot x = x$ . The affine maps respect pair multiplication because $M (N x + s) + t = M N x + M s + t$ , so $((t, M) (s, N)) \cdot x = (t, M) \cdot ((s, N) \cdot x)$ and [F2] holds. The translations $(t, I)$ are distinct as $t$ ranges over $Z^{2}$ , so each full group is infinite.

DefinitionDefinition: Literature-sourcedProof: Not applicableOpen item page →

Equivariant neural layers between group-action feature spaces

Definition

Let a group $G$ act on sets $X$ and $Y$ by left actions $T$ and $T^{'}$ , respectively. A layer is a function $Φ : X \to Y$ . It is $G$ -equivariant when

Φ (T_{g} x) = T_{g}^{'} Φ (x) (g \in G, x \in X) .

The input and output actions need not be the same. The layer is $G$ -invariant when $Φ (T_{g} x) = Φ (x)$ for every $g \in G$ and $x \in X$ ; equivalently, it is equivariant into $Y$ equipped with the trivial action.

Definition references

equivariant maps between acted-on sets

the induced action on feature maps

functions and declared domains/codomains

Cohen and Welling, “Group Equivariant Convolutional Networks,” §2

Goodfellow, Bengio, and Courville, Deep Learning, Chapter 9 §9.2

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

First-layer and group-to-group cross-correlation

Definition

Let $G$ be a discrete group acting on the lattice $Z^{2}$ on the left. Let $C_{i n}, C_{o u t}$ be positive integers, and regard channel vectors as row vectors. For a feature map $f : G \to R^{C_{i n}}$ and a filter $Ψ : G \to R^{C_{i n} \times C_{o u t}}$ , the group-to-group cross-correlation is the map $C_{Ψ} f : G \to R^{C_{o u t}}$ defined by

(C_{Ψ} f) (g) = \sum_{h \in G} f (h) Ψ (g^{- 1} h) .

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 is the map $E_{Ψ} f : G \to R^{C_{o u t}}$ defined by

(E_{Ψ} f) (g) = \sum_{x \in Z^{2}} f (x) Ψ (g^{- 1} \cdot x) .

Each displayed sum is required to have finite support or to converge absolutely in every output coordinate. The first operation takes group-indexed features and filters; the second takes lattice-indexed image features and filters and returns group-indexed features. These are cross-correlations, with the filter argument displayed as written; they need not be commutative, and no finiteness of $G$ is assumed.

Definition references

groups and their multiplication and inverses

left actions on feature maps

discrete cross-correlation and channel mixing

functions and declared domains/codomains

Cohen and Welling, “Group Equivariant Convolutional Networks,” §6.1, Eqs. (10)–(12)

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

DefinitionDefinition: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Pointwise nonlinearities, neighborhood pooling, subgroup sampling, and coset pooling

Definition

Let $G$ be a group and let $F : G \to R^{C}$ be a feature map with $C$ channels. A pointwise nonlinearity determined by $ν : R \to R$ is $N_{ν} F$ , where $(N_{ν} F) (g)_{c} = ν (F (g)_{c})$ . For a nonempty finite set $U \subseteq G$ , non-strided neighborhood max pooling is $P_{U} F$ , where $(P_{U} F) (g)_{c} = \max_{u \in U} F (g u)_{c}$ ; the output is still indexed by $G$ . For a subgroup $H \leq G$ , subgroup sampling is the restriction $R_{H} F = F ∣_{H}$ , indexed by $H$ .

The left-coset set is $G / H = {g H : g \in G}$ , where $g H = {g h : h \in H}$ . Its left $G$ -action is $a \cdot (g H) = (a g) H$ . For finite $H$ , left-coset max pooling is the map $Q_{H} F : G / H \to R^{C}$ given by $(Q_{H} F) (g H)_{c} = \max_{h \in H} F (g h)_{c}$ . All maxima are taken separately in each channel. When $H = G$ is finite, $G / H$ has one element and $Q_{H} F$ is a group-invariant summary.

Definition references

left actions on group-indexed feature maps

left actions of groups on sets

subgroup identity, closure, and inverse conditions

left cosets $g H$ of a subgroup

functions and declared domains/codomains

Cohen and Welling, “Group Equivariant Convolutional Networks,” §§6.2–6.3

Goodfellow, Bengio, and Courville, Deep Learning, Chapter 9 §9.3

Facts & Assumptions

Given: A group $G$ , a finite subgroup $H \leq G$ , a nonempty finite $U \subseteq G$ , and a feature map $F : G \to R^{C}$ . Verify that the coset action and pooling formulas are well-defined.

[F1]

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

[F2]

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

[F3]

Left group actions, transitive actions, and faithful actions: A left action satisfies $e \cdot z = z$ and $(a b) \cdot z = a \cdot (b \cdot z)$ for each acted-on element $z$ .

Proof

1.1givenF1F2F3algebra

If $g H = g^{'} H$ , then $g^{'} = g^{'} e \in g^{'} H = g H$ , so [F2] gives $g^{'} = g h_{0}$ for some $h_{0} \in H$ . By [F1], $h_{0} H \subseteq H$ ; conversely, every $k \in H$ equals $h_{0} (h_{0}^{- 1} k)$ with $h_{0}^{- 1} k \in H$ , so $H \subseteq h_{0} H$ . Hence $h_{0} H = H$ and $(a g^{'}) H = (a g h_{0}) H = a g (h_{0} H) = a g H$ , proving that $a \cdot (g H) = (a g) H$ is independent of the representative. It satisfies the identity and composition laws in [F3] because $e g = g$ and $(a b) g = a (b g)$ . Thus it is a left action on $G / H$ .

1.2givenF1F2algebra

If $g^{'} = g h_{0}$ with $h_{0} \in H$ , then $h_{0} H = H$ : closure gives $h_{0} H \subseteq H$ , and for $k \in H$ , $k = h_{0} (h_{0}^{- 1} k) \in h_{0} H$ by [F1]. Hence ${g^{'} h : h \in H} = {g h : h \in H}$ , so the componentwise maximum defining $Q_{H} F (g H)$ is independent of the representative.

2.1givenF1step 1.1step 1.2algebra∎

By [F1], $H$ contains the identity, so $H$ and the given set $U$ are nonempty and finite. Each displayed maximum therefore exists in $R$ ; the pointwise operation and subgroup restriction are also functions on their stated domains. Thus all four operators in the Definition are well-defined.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

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.

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.

4 · Examples, counterexamples and false statements

None yet.

Convolution and finite-group equivariance

2 · Logical flowchart

3 · Definitions, theorems and proofs

Discrete convolutional layer with local receptive fields, channel mixing, stride, and padding

Definition

Definition references

The left action on feature maps induced by an action on sites

Definition

Definition references

Facts & Assumptions

Proof

The p4 and p4m square-lattice symmetry groups

Definition

Definition references

Facts & Assumptions

Proof

Equivariant neural layers between group-action feature spaces

Definition

Definition references

First-layer and group-to-group cross-correlation

Definition

Definition references

Pointwise nonlinearities, neighborhood pooling, subgroup sampling, and coset pooling

Definition

Definition references

Facts & Assumptions

Proof

Group cross-correlation and compatible layers are equivariant

Statement

Statement references

Equivariance diagram

Facts & Assumptions

Proof

4 · Examples, counterexamples and false statements

Sources