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.

In a finite set with a symmetric irreflexive relation and at least two elements, two elements have equally many neighbours

Example

Let $V$ be a finite set with $N : = ∣ V ∣ \geq 2$ , and let $R \subseteq V \times V$ be 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)). Write $d (x) : = ∣ R_{x} ∣$ for the number of neighbours of $x$ . Then there are $x \neq y$ in $V$ with $d (x) = d (y)$ .

The point is that the possible values of $d$ are $0, 1, \dots, N - 1$ , which is as many values as $V$ has elements, so counting alone does not settle it. What settles it is that the two extreme values cannot both occur: if some $x_{0}$ has no neighbour then no $y$ can be a neighbour of everything else, since it would then be a neighbour of $x_{0}$ .

Concretely, with $V : = 3 = {0, 1, 2}$ and $R : = {(0, 1), (1, 0)}$ , the neighbour counts are $d (0) = 1$ , $d (1) = 1$ and $d (2) = 0$ , and the elements $0$ and $1$ have equally many neighbours.

Facts & Assumptions

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

[L1]

$R_{x} \subseteq V ∖ {x}$ by irreflexivity, and $R_{x}$ is finite, so $d (x) \leq ∣ V ∖ {x} ∣$ (A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clauses 1 and 2).

[L2]

$∣ V ∖ {x} ∣ = N - 1$ , since ${x}$ and $V ∖ {x}$ are disjoint with union $V$ and $∣ {x} ∣ = 1$ (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 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$ for the truncated difference).

[L3]

If $d (y) = N - 1$ then [L1] gives $R_{y} \subseteq V ∖ {y}$ , while [L2] gives $∣ R_{y} ∣ = N - 1 = ∣ V ∖ {y} ∣$ ; hence $R_{y} = V ∖ {y}$ (A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , 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, The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 3).

[L4]

Symmetry: $x \in R_{y}$ if and only if $y \in R_{x}$ (A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , clause (d)).

[L5]

The counting form of the strong pigeonhole principle: if $∣ A ∣ > 1 \cdot ∣ B ∣$ then some fibre of any $f : A \to B$ has more than one element (If $∣ A ∣ > k ∣ B ∣$ then every $f : A \to B$ has a fibre with more than $k$ elements, and for nonempty $B$ some fibre has at least $⌈ ∣ A ∣ / ∣ B ∣ ⌉$ elements, clause 1, Injection, surjection, bijection).

[L6]

Order and membership in $N$ : $k \leq N - 2$ if and only if $k < N - 1$ , that is $k \in N - 1$ ; $N \geq 2$ gives $N - 1 \geq 1$ and $(N - 1) - 1 = N - 2$ ; and exactly one of $p < q$ , $p = q$ , $q < p$ holds (On $N$ the order is membership: $m < n ⟺ m \in n$ , Order on the natural numbers, Trichotomy of the order on $N$ , Order is compatible with addition, The natural numbers $N$ (von Neumann), Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L7]

Every natural number is a finite set whose cardinality is itself; in particular $∣ N - 1 ∣ = N - 1$ (The cardinality $∣ A ∣$ of a finite set, clause (a)).

Verification

technique · cases

1.1

By [L1] and [L2], $d (x) \leq N - 1$ for every $x \in V$ ; and $N \geq 2$ , so $N - 1 \geq 1$ by [L6].

givenL1L2L6

1.2

The two extreme values cannot both be attained. Suppose $d (x_{0}) = 0$ and $d (y) = N - 1$ for some $x_{0}, y \in V$ . Then $x_{0} \neq y$ , since $0 \neq N - 1$ by [L6]; by [L3] we have $R_{y} = V ∖ {y}$ , so $x_{0} \in R_{y}$ , so $y \in R_{x_{0}}$ by [L4], so $d (x_{0}) \geq 1$ , contradicting $d (x_{0}) = 0$ .

L1L3L4L6

2.1

Case (a): no $x \in V$ has $d (x) = 0$ . Then $1 \leq d (x) \leq N - 1$ for every $x$ , so $d (x) - 1 \leq N - 2$ , that is $d (x) - 1 \in N - 1$ by [L6]; thus $x \mapsto d (x) - 1$ maps $V$ into the set $N - 1$ , whose cardinality is $N - 1$ . Since $N > N - 1$ , [L5] gives two distinct $x \neq y$ with $d (x) - 1 = d (y) - 1$ , and since both counts are at least $1$ this forces $d (x) = d (y)$ .

assume-case posstep 1.1L5L6L7

2.2

Case (b): some $x_{0} \in V$ has $d (x_{0}) = 0$ . Then by step 1.2 no $y$ has $d (y) = N - 1$ , so $d (x) \leq N - 2$ for every $x$ by [L1], [L2] and [L6], that is $d (x) \in N - 1$ ; thus $d$ maps $V$ into the set $N - 1$ , of cardinality $N - 1$ . Since $N > N - 1$ , [L5] gives two distinct $x \neq y$ with $d (x) = d (y)$ .

assume-case zerostep 1.1step 1.2L1L2L5L6L7

3.1

The two cases are exhaustive, so in either case two distinct elements of $V$ have equally many neighbours.

step 2.1step 2.2cases-exhaustive∎

Remarks

Where $N \geq 2$ is spent. Twice: to make $N - 1$ at least $1$ , so that the set of possible values is nonempty and the shift by $1$ in case (a) lands inside $N - 1$ ; and to make $0$ and $N - 1$ different, which is what step 1.2 needs.
Why the naive count is not enough. The values of $d$ lie in a set of $N$ naturals and $V$ has $N$ elements, so the pigeonhole principle says nothing until the range is cut down. Both cases cut it to $N - 1$ values, one by removing $0$ and one by removing $N - 1$ , and the exclusion of the other extreme is what licenses the cut.
Symmetry and irreflexivity are both used. Irreflexivity gives the bound $d (x) \leq N - 1$ ; symmetry is what turns " $x_{0}$ is a neighbour of $y$ " into " $y$ is a neighbour of $x_{0}$ " in step 1.2. Neither can be dropped.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

Pigeonhole principle (Wikipedia) (standard reference, not scraped)
Handshaking lemma (Wikipedia) (standard reference, not scraped)
Graph Theory, Chapter 1 (King Saud University notes) (standard reference, not scraped)