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.

Minkowski fails for $p = 1 / 2$ : the hypothesis $p \geq 1$ is load-bearing

Statement refuted

Refuted claim: the inequality of Minkowski's inequality for finite sums (rational exponent) holds for every positive rational $p$ .

Witness: $p : = 1 / 2$ , with the two-entry lists $x_{0} : = 1$ , $x_{1} : = 0$ and $y_{0} : = 0$ , $y_{1} : = 1$ . The left-hand side $(\sum_{k < 2} ∣ x_{k} + y_{k} ∣^{1 / 2})^{1 / (1 / 2)} = (\sum_{k < 2} ∣ x_{k} + y_{k} ∣^{1 / 2})^{2}$ is $(1 + 1)^{2} = 4$ , while the right-hand side $(\sum_{k < 2} ∣ x_{k} ∣^{1 / 2})^{2} + (\sum_{k < 2} ∣ y_{k} ∣^{1 / 2})^{2}$ is $1 + 1 = 2$ ; so the inequality fails. Every expression is defined: $1 / 2$ is a positive rational, $∣ z ∣^{1 / 2} = \sqrt{∣ z ∣}$ is the rational power of Rational powers $a^{r}$ of a positive base with its supplementary clause $0^{1 / 2} = 0$ , and the outer exponent $1 / p = 2$ is an integer power.

Facts & Assumptions

Given: The rational exponent $p : = 1 / 2$ , its reciprocal $1 / p = 2 = 1 / (1 / 2)$ , and the lists $x_{0} = 1$ , $x_{1} = 0$ , $y_{0} = 0$ , $y_{1} = 1$ .

[L1]

Minkowski's inequality (Minkowski's inequality for finite sums (rational exponent)): for rational $p \geq 1$ and reals $a_{k}, b_{k}$ , $(\sum_{k < n} ∣ a_{k} + b_{k} ∣^{p})^{1 / p} \leq (\sum_{k < n} ∣ a_{k} ∣^{p})^{1 / p} + (\sum_{k < n} ∣ b_{k} ∣^{p})^{1 / p}$ ; the hypothesis $p \geq 1$ is part of the statement.

[L2]

Two-entry sums (Finite sums and finite products, by recursion, Laws of finite sums and finite products): $\sum_{k < 2} c_{k} = c_{0} + c_{1}$ .

[L3]

Absolute values (Basic properties of the absolute value, Absolute value in an ordered field): $∣ x ∣ \geq 0$ , $∣ 0 ∣ = 0$ , $∣ 1 ∣ = 1$ , and $∣ x ∣ = 0$ only for $x = 0$ .

[L4]

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$ , Laws of rational exponents): $1^{1 / 2} = 1$ and $0^{1 / 2} = 0$ . For a nonnegative base $a$ and a positive rational $r = m / N$ with $m, N \geq 1$ , $a^{r} = (a^{1 / N})^{m}$ , a root followed by an integer power. In particular $1 / (1 / 2) = 2$ , so for the nonnegative sums used below the outer power is the integer square.

[L5]

Integer powers and order (Integer powers $a^{m}$ , The multiplicative identity is positive): $2^{2} = 4$ by the recursion clause, $1 > 0$ , and adding inequalities gives $4 = 2 + 2 > 2$ .

Counterexample

technique · direct

1.1L2L3L4L5algebra

The left-hand side: by [L2] the sums of the entries are $x_{0} + y_{0} = 1$ and $x_{1} + y_{1} = 1$ , so $∣ x_{k} + y_{k} ∣^{1 / 2} = 1$ for $k = 0, 1$ by [L3] and [L4] and $\sum_{k < 2} ∣ x_{k} + y_{k} ∣^{1 / 2} = 1 + 1 = 2$ ; raising to the exponent $1 / (1 / 2) = 2$ by [L4] gives the left-hand value $2^{2} = 4$ by [L5].

1.2L2L3L4algebra

The right-hand side: $\sum_{k < 2} ∣ x_{k} ∣^{1 / 2} = 1^{1 / 2} + 0^{1 / 2} = 1 + 0 = 1$ and $\sum_{k < 2} ∣ y_{k} ∣^{1 / 2} = 0^{1 / 2} + 1^{1 / 2} = 0 + 1 = 1$ by [L2], [L3] and [L4], and each is raised to the power $2$ by [L4], so the right-hand value is $1^{2} + 1^{2} = 1 + 1 = 2$ .

1.3L5algebra

The comparison: $4 > 2$ by [L5].

2.1step 1.1step 1.2step 1.3L1L4∎

Conclusion: the inequality of [L1] fails at $p = 1 / 2$ with the displayed lists, since the left-hand value $4$ of step 1.1 exceeds the right-hand value $2$ of step 1.2 by step 1.3; every expression is defined — the inner powers use the rational power at the positive exponent $1 / 2$ together with the supplementary clause $0^{1 / 2} = 0$ , and the outer exponent $1 / p = 2$ is an integer power — so this is a genuine failure of the inequality for $p < 1$ and not an artefact of undefined powers, and the hypothesis $p \geq 1$ of [L1] is load-bearing.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

Minkowski fails for p=1/2p=1/2: the hypothesis p≥1p≥1 is load-bearing