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.

Weighted AM-GM needs nonnegative weights summing to $1$

Statement refuted

Refuted claim: the inequality $\prod_{k < n} x_{k}^{w_{k}} \leq \sum_{k < n} w_{k} x_{k}$ of Weighted AM-GM inequality with rational weights holds for all positive $x_{k}$ and all rational weights $w_{k}$ of sum $1$ , or for all rational weights whatsoever.

Two witnesses. (i) For $x_{0} : = x_{1} : = 4$ and $w_{0} : = w_{1} : = 1$ , whose sum is $2 \neq 1$ : the left-hand side is $4^{1} \cdot 4^{1} = 16$ and the right-hand side is $1 \cdot 4 + 1 \cdot 4 = 8$ , so $16 > 8$ . (ii) For $x_{0} : = 4$ , $x_{1} : = 1 / 4$ , $w_{0} : = 2$ and $w_{1} : = - 1$ , whose sum is $1$ but which contains a negative weight: the left-hand side is $4^{2} \cdot (1 / 4)^{- 1} = 16 \cdot 4 = 64$ and the right-hand side is $2 \cdot 4 + (- 1) \cdot (1 / 4) = 8 - 1 / 4 = 31 / 4$ , so $64 > 31 / 4$ . Both hypotheses on the weights — nonnegativity and total mass $1$ — are therefore load-bearing.

Facts & Assumptions

Given: The two witness systems: $x_{0} = x_{1} = 4$ with $w_{0} = w_{1} = 1$ , and $x_{0} = 4$ , $x_{1} = 1 / 4$ with $w_{0} = 2$ , $w_{1} = - 1$ .

[L1]

Weighted AM-GM (Weighted AM-GM inequality with rational weights): for $n \geq 1$ , reals $x_{k} > 0$ and rationals $w_{k} \geq 0$ summing to $1$ when read as real numbers, one has $\prod_{k < n} x_{k}^{w_{k}} \leq \sum_{k < n} w_{k} x_{k}$ ; both hypotheses on the weights are part of the statement.

[L2]

Rational and integer powers (Rational powers $a^{r}$ of a positive base, Laws of rational exponents, Integer powers $a^{m}$ ): for positive bases $a^{1} = a$ , and for $a \neq 0$ and $j \geq 1$ , $a^{- j} = (a^{j})^{- 1}$ ; hence $4^{1} = 4$ and $(1 / 4)^{- 1} = ((1 / 4)^{1})^{- 1} = 4$ , because $(1 / 4) \cdot 4 = 1$ exhibits the inverse.

[L3]

The embedding of $Q$ (The unique embedding of ℚ into an ordered field): the canonical embedding $ι : Q \to R$ is an injective field homomorphism, so the rationals $1$ , $2$ , $- 1$ and $1 / 4$ keep their values and their order when read as real numbers.

[L4]

Positivity and order (The multiplicative identity is positive, Inverses of positives are positive, and reciprocation reverses order): $1 > 0$ , so $2 = 1 + 1 > 0$ and $4 > 0$ ; the inverse of a positive element is positive; and the order arithmetic of $R$ compares the fractions involved.

[L5]

Rationals (The rationals as equivalence classes of pairs of integers): $1$ , $2$ , $- 1$ and $1 / 4$ are rationals, and $- 1 < 0$ ; the negative weight of witness (ii) is a legitimate rational, and its sum with $2$ is $1$ in $Q$ .

Counterexample

technique · direct

1.1L2L3L4algebra

Witness (i), dropping the total-mass hypothesis: the weights $w_{0} = w_{1} = 1$ are rationals $\geq 0$ with $1 + 1 = 2 \neq 1$ as real numbers, so the theorem [L1] does not apply; nevertheless the displayed expressions are defined and evaluate as $4^{1} \cdot 4^{1} = 16$ and $1 \cdot 4 + 1 \cdot 4 = 8$ by [L2], [L3] and field arithmetic, and $16 > 8$ by [L4], so the conclusion of [L1] fails for this positive list even though every weight is nonnegative.

1.2L2L3L4L5algebra

Witness (ii), dropping nonnegativity: the weights $w_{0} = 2$ and $w_{1} = - 1$ are rationals by [L5] with $2 + (- 1) = 1$ as real numbers, so the total-mass hypothesis holds but the weight $- 1$ is negative and [L1] does not apply; the two bases $4$ and $1 / 4$ are positive, the left-hand side is $4^{2} \cdot (1 / 4)^{- 1} = 16 \cdot 4 = 64$ by [L2], and the right-hand side is $2 \cdot 4 + (- 1) \cdot (1 / 4) = 8 - 1 / 4 = 31 / 4$ by [L3] and field arithmetic, and $64 = 256 / 4 > 31 / 4$ by [L4], so the conclusion of [L1] fails here even with total weight $1$ .

2.1step 1.1step 1.2L1L2∎

Together the two witnesses show that each hypothesis on the weights is load-bearing: (i) refutes the version with nonnegative weights of sum other than $1$ (step 1.1) and (ii) refutes the version with total mass $1$ but a negative weight (step 1.2); in both cases every base is positive and every power is a legitimate rational power or integer power evaluated by [L2], so the failures are failures of the inequality and not of definedness, exactly as [L1]'s statement anticipates.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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)

Weighted AM-GM needs nonnegative weights summing to 11