ExampleConstruction: 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.

A weighted AM-GM computation: $8^{2 / 3} 1^{1 / 3} \leq \frac{2}{3} \cdot 8 + \frac{1}{3} \cdot 1$

Example

Take $n : = 2$ , $x_{0} : = 8$ , $x_{1} : = 1$ and the rational weights $w_{0} : = 2 / 3$ , $w_{1} : = 1 / 3$ , so that $w_{0} + w_{1} = 1$ as real numbers. Then Weighted AM-GM inequality with rational weights gives

$8^{2 / 3} \cdot 1^{1 / 3} \leq \frac{2}{3} \cdot 8 + \frac{1}{3} \cdot 1,$

where the left-hand side is $4$ and the right-hand side is $17 / 3$ ; so $4 < 17 / 3$ and the inequality is strict here. With $x_{0} : = x_{1} : = 8$ instead, both sides equal $8$ , so the bound is attained by a constant list.

Facts & Assumptions

Given: The list $x_{0} : = 8$ , $x_{1} : = 1$ for the displayed computation, the rational weights $w_{0} : = 2 / 3$ , $w_{1} : = 1 / 3$ , and the constant list $x_{0} : = x_{1} : = 8$ for the second display.

[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}$ , with the rational powers of Rational powers $a^{r}$ of a positive base.

[L2]

Rational powers and roots (Rational powers $a^{r}$ of a positive base, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): $8^{1 / 3} = 2$ and $1^{1 / 3} = 1$ , since $2^{3} = 8$ , $1^{3} = 1$ and both $2, 1$ are nonnegative; and $8^{2 / 3} = (8^{1 / 3})^{2} = 4$ at the representative $2 / 3$ .

[L3]

Rational power laws (Laws of rational exponents): $a^{r + s} = a^{r} a^{s}$ and $a^{1} = a$ for $a > 0$ and rationals $r, s$ ; in particular $8^{2 / 3} 8^{1 / 3} = 8^{1} = 8$ .

[L4]

Finite sums (Laws of finite sums and finite products): for $n = 2$ , $\sum_{k < 2} c_{k} = c_{0} + c_{1}$ , sums scale, and additivity holds, so $\sum_{k < 2} w_{k} x_{k} = w_{0} x_{0} + w_{1} x_{1}$ .

[L5]

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 $2 / 3$ and $1 / 3$ , read as real numbers, satisfy $2 / 3 + 1 / 3 = 1$ .

Verification

technique · direct

1.1L1L5algebra

The hypotheses of [L1] hold for the chosen data: $n = 2 \geq 1$ , $x_{0} = 8 > 0$ and $x_{1} = 1 > 0$ , both weights $2 / 3, 1 / 3$ are rationals $\geq 0$ , and read as real numbers they satisfy $2 / 3 + 1 / 3 = 1$ by [L5].

1.2L2algebra

The left-hand factors: $8^{1 / 3} = 2$ and $8^{2 / 3} = (8^{1 / 3})^{2} = 4$ , while $1^{1 / 3} = 1$ , all by [L2], so $8^{2 / 3} \cdot 1^{1 / 3} = 4$ .

1.3L4algebra

The right-hand side: $(2 / 3) \cdot 8 + (1 / 3) \cdot 1 = 16 / 3 + 1 / 3 = 17 / 3$ by [L4] and field arithmetic.

1.4L1L3L4algebra

The constant-list case: with $x_{0} = x_{1} = 8$ the weights still satisfy the hypotheses of [L1], and the left-hand side is $8^{2 / 3} 8^{1 / 3} = 8^{2 / 3 + 1 / 3} = 8^{1} = 8$ by [L3], while the right-hand side is $(2 / 3) \cdot 8 + (1 / 3) \cdot 8 = 8$ by [L4], so the inequality holds with equality there.

2.1step 1.1step 1.2step 1.3L1algebra

Applying [L1] to the chosen data, licensed by step 1.1, gives $8^{2 / 3} \cdot 1^{1 / 3} \leq (2 / 3) \cdot 8 + (1 / 3) \cdot 1$ , and substituting the evaluations of step 1.2 and step 1.3 gives $4 \leq 17 / 3$ , which is strict because $4 = 12 / 3 < 17 / 3$ ; the inequality is therefore strict at this list, and no equality characterisation of [L1] is claimed.

3.1step 2.1step 1.4L1∎

The displayed computation is verified with the strict outcome $4 < 17 / 3$ (step 2.1), and the constant list shows the bound can be attained (step 1.4); both computations check the hypotheses of the weighted theorem explicitly, as step 1.1 records.

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

A weighted AM-GM computation: 82/3 11/3≤23⋅8+13⋅182/311/3≤32​⋅8+31​⋅1