ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

For a finite symmetric irreflexive relation the sum of the neighbour counts is twice the number of unordered related pairs

Example

Let $V$ be a finite set and $R \subseteq V \times V$ symmetric and irreflexive (A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , clause (d)), with neighbour counts $d (x) : = ∣ R_{x} ∣$ . Put

$E : = {S \in [V]^{2} : S = {x, y} for some (x, y) \in R},$

the set of two-element subsets of $V$ whose elements are related. Then, in $N$ ,

$\sum_{x \in V} d (x) = 2 ∣ E ∣ .$

A concrete instance. With $V : = 4 = {0, 1, 2, 3}$ and $R$ the symmetric irreflexive relation whose related unordered pairs are ${0, 1}$ , ${1, 2}$ and ${2, 3}$ , the neighbour counts are $d (0) = 1$ , $d (1) = 2$ , $d (2) = 2$ , $d (3) = 1$ , summing to $6 = 2 \cdot 3$ , and $∣ E ∣ = 3$ .

The extreme instance. If $R$ relates every pair of distinct elements of $V$ then $E = [V]^{2}$ and $d (x) = N - 1$ for every $x$ , where $N : = ∣ V ∣$ ; the identity then reads $N (N - 1) = 2 (\binom{N}{2})$ , which is A finite set with $n$ elements has exactly $(\binom{n}{2})$ two-element subsets, and $2 (\binom{n}{2}) = n (n - 1)$ .

Facts & Assumptions

Given: A finite set $V$ , a symmetric irreflexive relation $R \subseteq V \times V$ , the neighbour counts $d (x) = ∣ R_{x} ∣$ , and the set $E$ above.

[L1]

Double counting: $\sum_{x \in V} ∣ R_{x} ∣ = ∣ R ∣$ in $N$ (Double counting: $\sum_{x \in X} ∣ R_{x} ∣ = ∣ R ∣ = \sum_{y \in Y} ∣ R^{y} ∣$ for a relation between finite sets, A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

[L2]

$R$ is finite, and so is $[V]^{2}$ and hence its subset $E$ (A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , clause (a), The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ , A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ).

[L3]

The sum rule for a finite partition, and a constant natural summand $\sum_{p \in S} c = ∣ S ∣ \cdot c$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, clause 2, The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, clause (c)). In particular, if $x \in V$ and $∣ V ∣ = N$ , then the disjoint union $V = {x} ⊔ (V ∖ {x})$ gives $∣ V ∖ {x} ∣ = N - 1$ (The cardinality $∣ A ∣$ of a finite set, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L4]

If $x \neq y$ , then $0 \mapsto x$ , $1 \mapsto y$ is a bijection $2 \to {x, y}$ , so $∣ {x, y} ∣ = ∣ 2 ∣ = 2$ ; more generally, a bijection from a finite set transports its cardinality to the codomain (The cardinality $∣ A ∣$ of a finite set, clauses (a) and (c), Injection, surjection, bijection).

[L5]

$∣ [V]^{2} ∣ = (\binom{N}{2})$ and $2 (\binom{N}{2}) = N (N - 1)$ for every $N \in N$ (A finite set with $n$ elements has exactly $(\binom{n}{2})$ two-element subsets, and $2 (\binom{n}{2}) = n (n - 1)$ ).

Verification

technique · direct

1.1

The pairing map. For $(x, y) \in R$ irreflexivity gives $x \neq y$ , so ${x, y}$ has exactly two elements by [L4] and lies in $E$ ; write $Ψ (x, y) : = {x, y}$ , a map $R \to E$ . It is surjective, since every $S \in E$ is ${x, y}$ for some $(x, y) \in R$ by the definition of $E$ .

givenL2L4construct

1.2

Every fibre of $Ψ$ has exactly two elements. Let $S = {x, y} \in E$ with $x \neq y$ . A pair $(u, v) \in R$ with ${u, v} = S$ has $u \neq v$ , so $(u, v)$ is $(x, y)$ or $(y, x)$ ; and both of these lie in $R$ , since at least one of them does and $R$ is symmetric. So $Ψ^{- 1} [{S}] = {(x, y), (y, x)}$ , which has two elements because $x \neq y$ .

givenL4

2.1

Counting $R$ by the fibres of $Ψ$ . The fibres of $Ψ$ are pairwise disjoint finite sets indexed by the finite set $E$ , with union $R$ , so [L3] gives $∣ R ∣ = \sum_{S \in E} ∣ Ψ^{- 1} [{S}] ∣ = \sum_{S \in E} 2 = ∣ E ∣ \cdot 2$ .

step 1.1step 1.2L2L3

3.1

Combining with [L1], $\sum_{x \in V} d (x) = ∣ R ∣ = 2 ∣ E ∣$ , which is the identity. In the extreme case where $R$ relates every pair of distinct elements, $E = [V]^{2}$ and the neighbours of $x$ are exactly $V ∖ {x}$ , so $d (x) = N - 1$ by [L3]; the identity therefore reads $N (N - 1) = 2 (\binom{N}{2})$ by [L3] and [L5].

step 2.1L1L3L5given∎

Remarks

Where symmetry is spent. Only in step 1.2, to know that both ordered pairs over a related unordered pair lie in $R$ ; without it a fibre could have one element and the factor $2$ would be wrong. Irreflexivity is spent in step 1.1, to know that ${x, y}$ really is a two-element set.
This is double counting of one set, not two computations of two sets. The relation $R$ is counted once by its row fibres, which gives the sum of the neighbour counts, and once by the fibres of $Ψ$ , which gives twice the number of related unordered pairs. Both are instances of the sum rule over a partition.
No graph vocabulary is used. The data are a finite set and a symmetric irreflexive relation on it, and $E$ is a set of two-element subsets. Nothing among this page's declared prerequisites defines a graph, and nothing here needs one.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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

Handshaking lemma (Wikipedia) (standard reference, not scraped)
Double counting (proof technique) (Wikipedia) (standard reference, not scraped)
Graph Theory, Chapter 1 (King Saud University notes) (standard reference, not scraped)