TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

The arithmetic mean, geometric mean inequality

Statement

Let $n \in N$ with $n \geq 1$ and let $a_{0}, \dots, a_{n - 1} \in R$ with $a_{k} \geq 0$ for every $k < n$ . Write

$A : = \frac{1}{n} \sum_{k < n} a_{k}, G : = (\prod_{k < n} a_{k})^{1 / n},$

the arithmetic mean and the geometric mean, where the $n$ -th root exists because $\prod_{k < n} a_{k} \geq 0$ (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Laws of finite sums and finite products) and $n$ denotes the canonical field image $n \cdot 1_{R}$ of the natural number n, which is invertible since $n \geq 1$ (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field). Then

$\prod_{k < n} a_{k} \leq A^{n}, equivalently G \leq A,$

and equality holds in either form if and only if $a_{0} = a_{1} = \dots = a_{n - 1}$ .

The proof is Cauchy's forward-backward induction: the statement is proved first along a doubling sequence, by doubling, and then pulled back from a member of that sequence to every smaller $n$ by a descent that replaces the missing entry with the arithmetic mean of the others. That is why the induction below runs over the doubling scheme and not over $n$ directly.

One point of hygiene decides how the doubling scheme is written. The doubling index has to be a natural number, because it is used as the length of a list, as a bound on an index, and as the starting point of a descent. The symbol $2^{j}$ would not do: Integer powers $a^{m}$ defines powers of a real base, so $2^{j}$ denotes a power of the real field element $2 \cdot 1_{R}$ under that definition, rather than a natural-number-valued operation, and so cannot index anything. The doubling sequence is therefore defined inside $N$ , by recursion (The recursion theorem):

$N_{0} = 1, N_{j + 1} = N_{j} + N_{j} (j \in N),$

and the induction below runs over $j$ , with $N_{j}$ as the list length. No identity relating $N_{j}$ to any real power is needed anywhere, and none is claimed.

Facts & Assumptions

Given: A natural $n \geq 1$ and reals $a_{0}, \dots, a_{n - 1} \geq 0$ ; for $m \geq 1$ let $P (m)$ denote the statement "for all reals $b_{0}, \dots, b_{m - 1} \geq 0$ , $\prod_{k < m} b_{k} \leq B^{m}$ where $B = \frac{1}{m} \sum_{k < m} b_{k}$ , with equality if and only if $b_{0} = \dots = b_{m - 1}$ ".

[L1]

A product with a zero factor is zero, $0 \cdot x = 0$ (Multiplication by zero: $0 \cdot a = 0$ ). Laws of finite sums and products (Laws of finite sums and finite products, Finite sums and finite products, by recursion): splitting of sums and of products at any index; the constant sum $\sum_{k < m} λ = m λ$ ; monotonicity of sums, with a sum of nonnegatives being $0$ only if every term is $0$ ; and a product of nonnegatives is nonnegative, of positives positive.

[L2]

Roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): every $c \geq 0$ has a unique $c^{1 / m} \geq 0$ with $(c^{1 / m})^{m} = c$ , and $c^{1 / m} > 0$ when $c > 0$ .

[L3]

Power monotonicity (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Integer powers $a^{m}$ ): $x \mapsto x^{m}$ is strictly increasing and injective on ${x \geq 0}$ for $m \geq 1$ , and preserves nonnegativity and positivity.

[L4]

Integer exponent laws (Laws of integer exponents): $(x y)^{m} = x^{m} y^{m}$ and $(x^{2})^{m} = x^{2 m}$ .

[L5]

Order arithmetic: multiplying inequalities of nonnegatives, in both the strict and the nonstrict form (Multiplying inequalities of positives); adding inequalities and scaling by a positive, both of which Order is preserved by adding a constant and by adding inequalities and Sign rules for products and monotonicity of multiplication state for the STRICT order only, so the nonstrict forms used below are the strict ones together with the case of equality, which is settled by trichotomy (Ordered field); and the inverse of a positive element is positive (Inverses of positives are positive, and reciprocation reverses order).

[L6]

Squares: $x^{2} \geq 0$ , which is $x^{2} > 0$ for $x \neq 0$ (Squares of nonzero elements are positive, the only thing that item states) together with $0^{2} = 0 \cdot 0 = 0$ , a product with a zero factor (Multiplication by zero: $0 \cdot a = 0$ ); and $x^{2} = 0$ only for $x = 0$ , the contrapositive of the same statement.

[L7]

Induction principle (The principle of mathematical induction).

[L8]

The doubling naturals: by the recursion theorem (The recursion theorem) applied to the set $N$ , the starting element $1$ and the function $f (k) = k + k$ , there is a unique $j \mapsto N_{j}$ from $N$ to $N$ with $N_{0} = 1$ and $N_{j + 1} = N_{j} + N_{j}$ . Each $N_{j}$ is a natural number, available as a list length and as an index bound; no power of a real base is used as a natural-number index.

[L9]

Canonical naturals: the field image $m \cdot 1_{R}$ is positive for natural $m \geq 1$ ; the canonical embedding $ι : Q \to R$ is a field homomorphism, and $m$ in field arithmetic denotes that image (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field).

[L10]

Order and addition in $N$ (Order on the natural numbers, $\leq$ is a linear order on $N$ , Order is compatible with addition, Discreteness: $σ (n)$ is the immediate successor, Addition is associative, Addition is commutative): $\leq$ is a linear order; $m \leq n$ holds exactly when $n = m + i$ for some $i \in N$ ; $m \leq n$ holds exactly when $m + k \leq n + k$ and $m < n$ exactly when $m + k < n + k$ , BOTH forms being stated in Order is compatible with addition and the nonstrict one being the one step 1.5 uses; $m < n$ holds exactly when $m + 1 \leq n$ (Discreteness: $σ (n)$ is the immediate successor); and addition is associative and commutative.

Proof

technique · induction

1.1baseL1L9

Base case $P (1)$ : for a single entry $b_{0} \geq 0$ we have $\prod_{k < 1} b_{k} = b_{0}$ and $B = \frac{1}{1} b_{0} = b_{0}$ , so $\prod_{k < 1} b_{k} = b_{0} = B^{1}$ ; equality always holds, and the condition "all entries equal" is automatic for one entry.

1.2ih

Inductive hypothesis: fix $j \in N$ , write $N : = N_{j}$ for the $j$ -th doubling natural, and assume $P (N)$ .

1.3L1L2L3L9

Reduction to positive entries: if some $b_{k} = 0$ then $\prod_{k < m} b_{k} = 0 \leq B^{m}$ , and equality means $B^{m} = 0$ , hence $B = 0$ , hence $\sum_{k < m} b_{k} = 0$ , hence every $b_{k} = 0$ , that is, all entries equal; conversely all entries equal to $0$ gives both sides $0$ ; so $P (m)$ holds for lists with a zero entry, and it is enough to prove $P (m)$ for lists of strictly positive entries.

1.4L5L6L9

The two-entry case $P (2)$ : for $x, y \geq 0$ , $(\frac{x + y}{2})^{2} - x y = \frac{(x + y)^{2} - 4 x y}{4} = (\frac{x - y}{2})^{2} \geq 0$ , so $x y \leq (\frac{x + y}{2})^{2}$ , with equality exactly when $(\frac{x - y}{2})^{2} = 0$ , that is when $x = y$ .

1.5L7L8L10

The doubling naturals grow past their index: $N_{j} \geq 1$ and $N_{j} > j$ for every $j \in N$ , by induction on $j$ inside $N$ ; at $j = 0$ , $N_{0} = 1 \geq 1$ and $1 > 0$ ; and if $N_{j} \geq 1$ and $N_{j} > j$ , then $N_{j} \geq j + 1$ , so $N_{j + 1} = N_{j} + N_{j} \geq (j + 1) + 1 > j + 1$ and $N_{j + 1} \geq 1 + 1 \geq 1$ . This inequality is between natural numbers throughout; nothing is transported into $R$ .

2.1step 1.2step 1.3step 1.4L1L3L4L5L9

Doubling step, $P (N) \Rightarrow P (2 N)$ , where $2 N : = N + N = N_{j + 1}$ is again a natural number: let $a_{0}, \dots, a_{2 N - 1} > 0$ , put $X : = \frac{1}{N} \sum_{k < N} a_{k}$ and $Y : = \frac{1}{N} \sum_{k = N}^{2 N - 1} a_{k}$ , both positive, and let $A : = \frac{1}{2 N} \sum_{k < 2 N} a_{k}$ ; splitting the sum at $N$ gives $\sum_{k < 2 N} a_{k} = N X + N Y$ , so $A = \frac{X + Y}{2}$ ; splitting the product at $N$ and applying the hypothesis to each half gives $\prod_{k < 2 N} a_{k} = (\prod_{k < N} a_{k}) (\prod_{k = N}^{2 N - 1} a_{k}) \leq X^{N} Y^{N} = (X Y)^{N}$ ; and the two-entry case applied to $X, Y$ gives $X Y \leq (\frac{X + Y}{2})^{2} = A^{2}$ , whence $(X Y)^{N} \leq (A^{2})^{N} = A^{2 N}$ and therefore $\prod_{k < 2 N} a_{k} \leq A^{2 N}$ .

2.2step 1.3L1L3L5L9

Descent step, $P (m + 1) \Rightarrow P (m)$ for every natural $m \geq 1$ , written in this direction so that no subtraction of naturals is needed: let $b_{0}, \dots, b_{m - 1} > 0$ and put $B : = \frac{1}{m} \sum_{k < m} b_{k} > 0$ ; define $a_{k} : = b_{k}$ for $k < m$ and $a_{m} : = B$ , so that $\sum_{k < m + 1} a_{k} = m B + B = (m + 1) B$ and the arithmetic mean of $a_{0}, \dots, a_{m}$ is exactly $B$ ; applying $P (m + 1)$ gives $(\prod_{k < m} b_{k}) B = \prod_{k < m + 1} a_{k} \leq B^{m + 1}$ , and dividing by $B > 0$ gives $\prod_{k < m} b_{k} \leq B^{m}$ ; moreover equality here holds exactly when $\prod_{k < m + 1} a_{k} = B^{m + 1}$ , which by the equality clause of $P (m + 1)$ holds exactly when all of $a_{0}, \dots, a_{m}$ are equal, that is when $b_{0} = \dots = b_{m - 1} = B$ , which in turn holds exactly when the $b_{k}$ are all equal, since a constant list equals its own mean; together with the zero-entry case this is $P (m)$ .

3.1step 1.2step 1.4step 2.1L1L3L5L9

Equality in the doubling step: with the notation of the doubling step 2.1, suppose $\prod_{k < 2 N} a_{k} = A^{2 N}$ ; then both inequalities in the chain are equalities, so first $(X Y)^{N} = (A^{2})^{N}$ with $X Y, A^{2} > 0$ gives $X Y = A^{2}$ by injectivity, hence $X = Y$ by the equality clause of the two-entry case; and second, writing $P_{1} = \prod_{k < N} a_{k} \leq X^{N}$ and $P_{2} = \prod_{k = N}^{2 N - 1} a_{k} \leq Y^{N}$ with all four quantities positive, $P_{1} < X^{N}$ would give $P_{1} P_{2} < X^{N} P_{2} \leq X^{N} Y^{N}$ , so $P_{1} = X^{N}$ and likewise $P_{2} = Y^{N}$ , whence by the equality clause of $P (N)$ the first half is constant, equal to its mean $X$ , and the second half is constant, equal to $Y = X$ ; so all $2 N$ entries are equal, and conversely entries all equal to $c$ give $\prod = c^{2 N}$ and $A = c$ .

4.1step 1.1step 2.1step 3.1L7L8

By the induction principle, $P (N_{j})$ holds for every $j \in N$ : the base is $P (N_{0}) = P (1)$ and the step is the doubling argument together with its equality clause.

5.1step 1.5step 4.1step 2.2L7L10

Every $n \geq 1$ is reached: by step 1.5, $N_{n} > n$ , so $n \leq N_{n}$ and $N_{n} = n + i_{0}$ for some $i_{0} \in N$ ; now run a further induction on $i$ over the statement $Q (i)$ , "for every natural $m \geq 1$ with $m + i = N_{n}$ , $P (m)$ holds"; $Q (0)$ says $P (N_{n})$ , which is step 4.1; and if $Q (i)$ holds and $m \geq 1$ satisfies $m + (i + 1) = N_{n}$ , then $(m + 1) + i = N_{n}$ with $m + 1 \geq 1$ , so $P (m + 1)$ holds by $Q (i)$ and the descent step turns it into $P (m)$ , giving $Q (i + 1)$ ; applying $Q (i_{0})$ to $m = n$ yields $P (n)$ ; hence $\prod_{k < n} a_{k} \leq A^{n}$ with equality exactly when all $a_{k}$ are equal.

6.1step 5.1L2L3discharge-induction∎

Translation to the root form: $G = (\prod_{k < n} a_{k})^{1 / n}$ satisfies $G \geq 0$ and $G^{n} = \prod_{k < n} a_{k} \leq A^{n}$ with $A \geq 0$ , so $G \leq A$ , since $G > A$ would give $G^{n} > A^{n}$ ; and $G = A$ holds exactly when $G^{n} = A^{n}$ , by injectivity of $x \mapsto x^{n}$ on the nonnegatives, hence exactly when all $a_{k}$ are equal.

The arithmetic mean, geometric mean inequality

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources