CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

AM-GM fails for negative entries: $(- 1, - 4)$ has geometric mean $2$ and arithmetic mean $- 5 / 2$

Statement refuted

Refuted claim: the conclusion $\sqrt{a b} \leq \frac{a + b}{2}$ of the two-term arithmetic-geometric mean inequality holds for arbitrary real $a, b$ , with the square root as in Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ and the rational power as in Rational powers $a^{r}$ of a positive base.

Witness: $a : = - 1$ , $b : = - 4$ . The product is $a b = 4$ , so the geometric mean is $4^{1 / 2} = 2$ , while the arithmetic mean is $(- 1 - 4) / 2 = - 5 / 2$ ; thus $G = 2 > - 5 / 2 = A$ and the inequality fails. The failure is not an accident of the witness: for any two negative entries $a, b < 0$ the product is positive, so $G > 0$ , while $A < 0$ , giving $G > A$ . A second failure mode is non-existence: for $a : = - 1$ , $b : = 1$ the product is $- 1$ , which has no real square root (FALSE: every real number has a real square root), so $G$ is not defined at all. By contrast the equivalent squared form $a b \leq A^{2}$ of The arithmetic mean, geometric mean inequality survives for all real $a, b$ , since $A^{2} - a b = (a - b)^{2} / 4 \geq 0$ ; the hypothesis $a, b \geq 0$ is spent exactly on passing from that squared form to the geometric-mean form, which needs a nonnegative arithmetic mean and a real geometric mean.

Facts & Assumptions

Given: The real numbers $a : = - 1$ , $b : = - 4$ for the witness; general real numbers $a, b$ in the systematic discussion, with $A : = (a + b) / 2$ and $G : = (a b)^{1 / 2}$ whenever the latter is defined.

[L1]

Arithmetic-geometric mean (The arithmetic mean, geometric mean inequality): for two nonnegative entries $u, v$ one has $(u v)^{1 / 2} \leq (u + v) / 2$ , equivalently $u v \leq ((u + v) / 2)^{2}$ , with equality exactly when $u = v$ .

[L2]

Roots and rational powers (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Rational powers $a^{r}$ of a positive base): for $c \geq 0$ the symbol $c^{1 / 2} = \sqrt{c}$ is the unique $s \geq 0$ with $s^{2} = c$ , and $s > 0$ when $c > 0$ ; in particular $4^{1 / 2} = 2$ , because $2 \geq 0$ and $2 \cdot 2 = 4$ .

[L3]

Sign rules (Sign rules for products and monotonicity of multiplication): a product of two negative reals is positive and a product of two positive reals is positive; $x < 0$ holds exactly when $- x > 0$ ; and multiplication by a positive factor preserves the strict order in both directions.

[L4]

Order arithmetic (Order is preserved by adding a constant and by adding inequalities, Ordered field): adding a constant preserves the strict order, adding two strict inequalities preserves them, and the order is total and transitive.

[L5]

Squares and negatives (Squares of nonzero elements are positive, Multiplication by zero: $0 \cdot a = 0$ , Sign rules for products: $(- a) b = - (a b)$ and $(- a) (- b) = a b$ ): $u^{2} > 0$ for every $u \neq 0$ , while $0^{2} = 0 \cdot 0 = 0$ , so $u^{2} \geq 0$ for every real $u$ ; and $(- u) v = - (u v)$ , $(- u) (- v) = u v$ .

[L6]

Positivity of the identity (The multiplicative identity is positive): $1 > 0$ , hence $2 = 1 + 1 > 0$ , and by repeated addition every nonzero numeral is positive.

[L7]

Negatives have no real square root (FALSE: every real number has a real square root): there is no real $y$ with $y^{2} = - 1$ ; the existence theorem Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ produces square roots only for nonnegative arguments.

Counterexample

technique · direct

1.1L2L3L4L5L6algebra

At the witness: $a b = (- 1) (- 4) = 4$ by [L5], so $G = 4^{1 / 2} = 2$ by [L2]; the arithmetic mean is $A = (- 1 + (- 4)) / 2 = - 5 / 2$ ; and $2 > - 5 / 2$ , because $- 5 / 2 < 0$ by [L3] (using $2 (- 5 / 2) = - 5 < 0$ and the equivalence $u < 0 ⟺ 2 u < 0$ , where $2, 5 > 0$ by [L6] and [L4]) while $2 > 0$ by [L6], so transitivity in [L4] gives $G = 2 > - 5 / 2 = A$ ; thus the claimed inequality fails at $(- 1, - 4)$ .

1.2L2L3L4L5algebra

For arbitrary negative entries $a, b < 0$ : the product is positive, $a b > 0$ , by [L3]; the root $G = (a b)^{1 / 2}$ is then defined and positive by [L2]; and $a + b < 0$ by adding the inequalities $a < 0$ and $b < 0$ in [L4], so $2 A = a + b < 0$ , while $A \geq 0$ would give $2 A \geq 0$ because a product of nonnegatives is nonnegative by [L3] and [L5]; hence $A < 0$ , and transitivity gives $G > A$ ; so the root form fails for every pair of negative entries, not only at the displayed witness.

1.3L7algebra

The second failure mode: at $a = - 1$ , $b = 1$ the product is $a b = - 1$ , so $G = (- 1)^{1 / 2}$ would be a real square root of $- 1$ , which does not exist by [L7]; the conclusion of the claimed inequality cannot even be stated there.

1.4L1L5algebra

The squared form survives for all real $a, b$ : with $A = (a + b) / 2$ one has $A^{2} - a b = ((a + b)^{2} - 4 a b) / 4 = (a - b)^{2} / 4 = ((a - b) / 2)^{2} \geq 0$ by [L5]; hence $a b \leq A^{2}$ for arbitrary reals, the two-entry squared form of [L1] without any sign hypothesis.

2.1step 1.1step 1.2step 1.3step 1.4L1L2∎

Collecting: the root form of the two-term arithmetic-geometric mean inequality fails outright at the witness (step 1.1, where $G = 2 > - 5 / 2 = A$ ), fails systematically for every pair of negative entries (step 1.2), and can fail by undefinedness (step 1.3); what the hypothesis $a, b \geq 0$ buys is precisely the passage from the squared form $a b \leq A^{2}$ , which survives without it (step 1.4), to the root form $G \leq A$ , which needs $G$ to exist and $A$ to be nonnegative; the hypothesis is therefore load-bearing and cannot be dropped.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

John K. Hunter, An Introduction to Real Analysis (author-hosted complete lecture notes, University of California at Davis) (standard reference, not scraped)
Jiří Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I, version 6.3, 15 May 2026 (author-hosted complete book) (standard reference, not scraped)

AM-GM fails for negative entries: (−1,−4)(−1,−4) has geometric mean 22 and arithmetic mean −5/2−5/2