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.

Hölder at the conjugate pair $p = 3$ , $q = 3 / 2$ : an exact equality instance and a strict instance

Example

$p : = 3$ and $q : = 3 / 2$ are conjugate rationals, $\frac{1}{3} + \frac{2}{3} = 1$ . For the two-entry lists $a_{0} = a_{1} = b_{0} = b_{1} = 1$ , Hölder's inequality for finite sums (rational exponents) reads

$\sum_{k < 2} ∣ a_{k} b_{k} ∣ = 2 \leq (\sum_{k < 2} ∣ a_{k} ∣^{3})^{1 / 3} (\sum_{k < 2} ∣ b_{k} ∣^{3 / 2})^{2 / 3} = 2^{1 / 3} 2^{2 / 3} = 2,$

so both sides are equal here. For $a = (2, 0)$ and $b = (0, 3)$ the inequality is strict: the left-hand side is $0$ and the right-hand side is $2 \cdot 3 = 6$ .

Facts & Assumptions

Given: The two-entry lists $a_{0} = a_{1} = b_{0} = b_{1} = 1$ , and the lists $a_{0} = 2$ , $a_{1} = 0$ , $b_{0} = 0$ , $b_{1} = 3$ .

[L1]

Hölder's inequality (Hölder's inequality for finite sums (rational exponents)): for conjugate rationals $p, q > 1$ and reals $a_{k}, b_{k}$ , $\sum_{k < n} ∣ a_{k} b_{k} ∣ \leq (\sum_{k < n} ∣ a_{k} ∣^{p})^{1 / p} (\sum_{k < n} ∣ b_{k} ∣^{q})^{1 / q}$ ; it records no equality characterization.

[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}$ , sums are additive and scale, and the constant sum is $\sum_{k < 2} λ = 2 λ$ .

[L3]

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

[L4]

Rational powers (Rational powers $a^{r}$ of a positive base, Laws of rational exponents): $1^{r} = 1$ for every rational $r$ ; $a^{r + s} = a^{r} a^{s}$ and $(a^{r})^{s} = a^{r s}$ for $a > 0$ ; and $0^{t} = 0$ for rational $t > 0$ .

Verification

technique · direct

1.1L1L2L3L4algebra

The equality instance: with all four entries equal to $1$ , [L2] gives $\sum_{k < 2} ∣ a_{k} b_{k} ∣ = 1 + 1 = 2$ , $\sum_{k < 2} ∣ a_{k} ∣^{3} = 1 + 1 = 2$ and $\sum_{k < 2} ∣ b_{k} ∣^{3 / 2} = 1 + 1 = 2$ by [L3] and [L4]; the right-hand side is $2^{1 / 3} 2^{2 / 3} = 2^{1 / 3 + 2 / 3} = 2^{1} = 2$ by [L4], so [L1] holds with both sides equal to $2$ here.

1.2L1L2L3L4algebra

The strict instance: for $a = (2, 0)$ and $b = (0, 3)$ , [L2] and [L3] give $\sum_{k < 2} ∣ a_{k} b_{k} ∣ = ∣ 2 \cdot 0 ∣ + ∣ 0 \cdot 3 ∣ = 0$ , while $\sum_{k < 2} ∣ a_{k} ∣^{3} = 2^{3} + 0^{3} = 8$ and $\sum_{k < 2} ∣ b_{k} ∣^{3 / 2} = 0^{3 / 2} + 3^{3 / 2}$ by [L4]; hence the right-hand side is $8^{1 / 3} (3^{3 / 2})^{2 / 3} = 2 \cdot 3^{(3 / 2) (2 / 3)} = 2 \cdot 3^{1} = 6$ by [L4], and $0 < 6$ , so the inequality is strict at this pair.

2.1step 1.1step 1.2L1∎

Summary: at $p = 3$ , $q = 3 / 2$ the inequality of [L1] is an equality on the constant list of ones (step 1.1) and strict on the disjoint-support pair $(2, 0)$ , $(0, 3)$ (step 1.2); since [L1] records no equality characterization, only the two evaluations and the inequality itself are asserted, and the exact agreement in step 1.1 is a computation and not a claimed equality criterion.

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)

Hölder at the conjugate pair p=3p=3, q=3/2q=3/2: an exact equality instance and a strict instance