CounterexampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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 \ne \varnothing$ there is $x \in X$ with

$\iota(\lvert R_x\rvert) \;=\; \mu \;:=\; \frac{\iota(\lvert R\rvert)}{\iota(\lvert X\rvert)} .$

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 $\mu$ and some row fibre is at most $\mu$ ; equality is not claimed, and it can fail, because $\mu$ 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 $\lvert R\rvert = 3$ and $\lvert X\rvert = 2$ , so $\mu = 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 $\iota$ (The canonical natural $\iota(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 $\lvert A\rvert$ of a finite set, clauses (a) and (c), Injection, surjection, bijection).

[L3]

Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^{y}\rvert$ (Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert$ 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\ne\varnothing$ and $\mu=\iota(|R|)/\iota(|X|)$ , then some $x_+\in X$ satisfies $\iota(|R_{x_+}|)\ge\mu$ and some $x_-\in X$ satisfies $\iota(|R_{x_-}|)\le\mu$ (If $X$ is nonempty, some row fibre is at least the average size and some row fibre is at most the average size).

[L5]

$\mathbb{R}$ is an ordered field, so $\mu$ is defined once $\iota(\lvert X\rvert) \ne 0$ , and $\iota$ is strictly increasing with $\iota(0) = 0$ , $\iota(1) = 1$ , $\iota(2) = 1+1$ , $\iota(3) = 1+1+1$ (Ordered field, Field, Laws of finite sums and products in $\mathbb{N}$ , and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$ , clauses 0 and 7).

Counterexample

technique · constructive

1.1

The fibres. $R_0 = \{0\}$ and $R_1 = \{0,1\}$ , so $\lvert R_0\rvert = 1$ and $\lvert R_1\rvert = 2$ by [L1] and [L2]; and $\lvert R\rvert = 3$ , the three listed pairs being distinct.

givenL1L2construct

1.2

The average. $\lvert X\rvert = 2 \ne 0$ , so $\mu = \iota(3)/\iota(2)$ is defined by [L5]; and $\iota(2)\,\iota(1) = \iota(2) < \iota(3) < \iota(2) + \iota(2) = \iota(2)\,\iota(2)$ , so dividing by the positive $\iota(2)$ gives $\iota(1) < \mu < \iota(2)$ by [L5].

givenL2L5

1.3

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

givenL1L2L3

2.1

No row fibre has size $\mu$ . The values $\iota(\lvert R_0\rvert) = \iota(1)$ and $\iota(\lvert R_1\rvert) = \iota(2)$ are the only candidates by step 1.1, and step 1.2 places $\mu$ 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 $\iota(\lvert R_{1}\rvert) = \iota(2) > \mu$ , and $x_{-} := 0$ has $\iota(\lvert R_{0}\rvert) = \iota(1) < \mu$ . 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. $\mu$ is a quotient of two natural numbers formed in $\mathbb{R}$ , and nothing forces it to be the canonical natural of a natural number. Here $\lvert X\rvert$ does not divide $\lvert R\rvert$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 69 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)