Prove2Me

Β§5.4, p. 81 β€” on the complete graph A = πŸ™πŸ™α΅€ the aggregate βŠ•α΅₯ ψ(xα΅₯) is the same for all nodes u

Proved
GeomDL.Sets.complete_graph_aggregate_constant

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

deep-setsgeometric-deep-learninggraph-neural-networksp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Consider the convolutional-type layer hu=Ο•(xu,⨁v∈Nuψ(xv))\mathbf h_u=\phi\big(\mathbf x_u,\bigoplus_{v\in\mathcal N_u}\psi(\mathbf x_v)\big), where ψ:Rdβ†’M\psi:\mathbb R^d\to M and the permutation-invariant aggregator ⨁\bigoplus acts on the multiset { ⁣{ψ(xv):v∈Nu} ⁣}\{\!\{\psi(\mathbf x_v):v\in\mathcal N_u\}\!\} with values in Mβ€²M'. On the complete graph A=11⊀\mathbf A=\mathbf 1\mathbf 1^\top, every neighbourhood is V\mathcal V, so for any input X\mathbf X and nodes u,wu,w,

⨁v∈Nuψ(xv)=⨁v∈Nwψ(xv).\bigoplus_{v\in\mathcal N_u}\psi(\mathbf x_v)=\bigoplus_{v\in\mathcal N_w}\psi(\mathbf x_v).

Thus the layer receives the same aggregate as its second input at every node, as stated in Β§5.4, p. 81.

Formalization Note This item covers the page's constant-aggregate clause. Its subsequent claim that the complete-graph layer has the same expressive power as a node-only layer fails across inputs: with two nodes and sum aggregation, changing only the second node can change the first node's output.

Preamble
import Mathlib
import Definitions.Def_GeomDL_Sets_Defs
Formal statement
namespace GeomDL.Sets

/-- Β§5.4, p. 81 (and side-note): on the complete graph `A = πŸ™πŸ™α΅€` (so `N_u = V`),
the permutation-invariant aggregate `βŠ•_{v ∈ V} ψ(x_v)` supplied as the second input to
`h_u = Ο†(x_u, βŠ•_{v ∈ V} ψ(x_v))` is identical at every node `u`. -/
theorem complete_graph_aggregate_constant {n d : β„•} {M M' : Type*}
    (ψ : (Fin d β†’ ℝ) β†’ M) (agg : Multiset M β†’ M')
    (X : Matrix (Fin n) (Fin d) ℝ) :
    βˆ€ u w : Fin n,
      agg ((neighbourhood (allOnes n) u).val.map (fun v => ψ (X v))) =
        agg ((neighbourhood (allOnes n) w).val.map (fun v => ψ (X v))) := by sorry

end GeomDL.Sets
Source
Bronstein et al., Geometric Deep Learning (arXiv:2104.13478v2), Β§5.4, Complete edge set, p. 81 and side-note
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