CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck 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.

A relation whose row fibres all differ from the average size, so the averaging principle gives a bound that no fibre meets exactly

Statement refuted

Refuted claim: that the averaging principle produces a row fibre of exactly the average size, that is, that for every relation $R \subseteq X \times Y$ between finite sets with $X \neq \emptyset$ there is $x \in X$ with

$ι (∣ R_{x} ∣) = μ : = \frac{ι (∣ R ∣)}{ι (∣ X ∣)} .$

What If $X$ is nonempty, some row fibre is at least the average size and some row fibre is at most the average size asserts is only that some row fibre is at least $μ$ and some row fibre is at most $μ$ ; equality is not claimed, and it can fail, because $μ$ is a real number while a fibre size is a natural number.

The witness is $X : = 2 = {0, 1}$ , $Y : = 3 = {0, 1, 2}$ and

$R : = {(0, 0), (1, 0), (1, 1)} \subseteq X \times Y .$

Here $∣ R ∣ = 3$ and $∣ X ∣ = 2$ , so $μ = 3 / 2$ , while the row fibres have sizes $1$ and $2$ .

Facts & Assumptions

Given: $X = 2$ , $Y = 3$ , $R = {(0, 0), (1, 0), (1, 1)}$ , and the canonical natural $ι$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L1]

Row and column fibres, and their finiteness (A relation $R \subseteq X \times Y$ between finite sets, its row fibres $R_{x}$ and its column fibres $R^{y}$ , clause (a)).

[L2]

A listed set with distinct entries has as many elements as entries (The cardinality $∣ A ∣$ of a finite set, clauses (a) and (c), Injection, surjection, bijection).

[L3]

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

[L4]

If $R \subseteq X \times Y$ is a finite incidence relation with $X \neq \emptyset$ and $μ = ι (∣ R ∣) / ι (∣ X ∣)$ , then some $x_{+} \in X$ satisfies $ι (∣ R_{x_{+}} ∣) \geq μ$ and some $x_{-} \in X$ satisfies $ι (∣ R_{x_{-}} ∣) \leq μ$ (If $X$ is nonempty, some row fibre is at least the average size and some row fibre is at most the average size).

[L5]

$R$ is an ordered field, so $μ$ is defined once $ι (∣ X ∣) \neq 0$ , and $ι$ is strictly increasing with $ι (0) = 0$ , $ι (1) = 1$ , $ι (2) = 1 + 1$ , $ι (3) = 1 + 1 + 1$ (Ordered field, Field, Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clauses 0 and 7).

Counterexample

technique · constructive

1.1

The fibres. $R_{0} = {0}$ and $R_{1} = {0, 1}$ , so $∣ R_{0} ∣ = 1$ and $∣ R_{1} ∣ = 2$ by [L1] and [L2]; and $∣ R ∣ = 3$ , the three listed pairs being distinct.

givenL1L2construct

1.2

The average. $∣ X ∣ = 2 \neq 0$ , so $μ = ι (3) / ι (2)$ is defined by [L5]; and $ι (2) ι (1) = ι (2) < ι (3) < ι (2) + ι (2) = ι (2) ι (2)$ , so dividing by the positive $ι (2)$ gives $ι (1) < μ < ι (2)$ by [L5].

givenL2L5

1.3

The column fibres check the count. $R^{0} = {0, 1}$ , $R^{1} = {1}$ and $R^{2} = \emptyset$ , of sizes $2$ , $1$ and $0$ , and $2 + 1 + 0 = 3 = ∣ R ∣$ , in agreement with [L3].

givenL1L2L3

2.1

No row fibre has size $μ$ . The values $ι (∣ R_{0} ∣) = ι (1)$ and $ι (∣ R_{1} ∣) = ι (2)$ are the only candidates by step 1.1, and step 1.2 places $μ$ strictly between them. So the refuted claim fails on this relation.

step 1.1step 1.2L5

3.1

What [L4] does give here, and it is sharp as stated: $x_{+} : = 1$ has $ι (∣ R_{1} ∣) = ι (2) > μ$ , and $x_{-} : = 0$ has $ι (∣ R_{0} ∣) = ι (1) < μ$ . Both inequalities hold strictly, and neither can be improved to an equality by another choice of $x$ , since step 1.1 lists all the row fibres.

step 1.1step 1.2step 2.1L4discharge-construct∎

Remarks

Why equality was never available. $μ$ is a quotient of two natural numbers formed in $R$ , and nothing forces it to be the canonical natural of a natural number. Here $∣ X ∣$ does not divide $∣ R ∣$ in any sense the page supplies, and the average falls strictly between two consecutive fibre sizes.
The two elements produced by the averaging principle are distinct here, and in general they need not be: if every fibre has the same size then a single $x$ serves as both. What the witness shows is only that neither inequality can be strengthened to an equality in general.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

Double counting (proof technique) (Wikipedia) (standard reference, not scraped)
Pigeonhole principle (Wikipedia) (standard reference, not scraped)
Mathematics for Computer Science (MIT OpenCourseWare) (standard reference, not scraped)