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.

The two-term Lagrange identity and Cauchy-Schwarz

Example

For all reals $a_{0}, a_{1}, b_{0}, b_{1}$ , with two-entry sums as in Finite sums and finite products, by recursion,

$(a_{0}^{2} + a_{1}^{2}) (b_{0}^{2} + b_{1}^{2}) - (a_{0} b_{0} + a_{1} b_{1})^{2} = (a_{0} b_{1} - a_{1} b_{0})^{2};$

consequently

$(a_{0} b_{0} + a_{1} b_{1})^{2} \leq (a_{0}^{2} + a_{1}^{2}) (b_{0}^{2} + b_{1}^{2}),$

with equality exactly when $a_{0} b_{1} = a_{1} b_{0}$ . That equality criterion is the two-entry form of the proportionality clause of The Cauchy-Schwarz inequality for finite sums: by the equality clause of that theorem, equality in its squared inequality holds if and only if the two lists are proportional, and the display above shows that for two entries equality holds if and only if $a_{0} b_{1} - a_{1} b_{0}$ vanishes. The instance $a_{0} : = 1$ , $a_{1} : = 2$ , $b_{0} : = 3$ , $b_{1} : = 4$ reads $5 \cdot 25 - 121 = 4 = (- 2)^{2}$ .

Facts & Assumptions

Given: Reals $a_{0}, a_{1}, b_{0}, b_{1}$ , with $A : = a_{0}^{2} + a_{1}^{2}$ , $B : = b_{0}^{2} + b_{1}^{2}$ , $C : = a_{0} b_{0} + a_{1} b_{1}$ and $D : = a_{0} b_{1} - a_{1} b_{0}$ .

[L1]

Two-entry sums and their laws (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 a sum of nonnegative terms is nonnegative.

[L2]

Definition of powers (Integer powers $a^{m}$ ): $x^{0} = 1$ and $x^{j + 1} = x^{j} x$ for every real $x$ and natural $j$ ; in particular $x^{2} = x \cdot x$ .

[L3]

Laws of natural exponents (Laws of integer exponents): $(u v)^{n} = u^{n} v^{n}$ and $(u^{m})^{n} = u^{m n}$ for all reals $u, v$ and naturals $m, n$ ; in particular $a_{0}^{2} b_{1}^{2} = (a_{0} b_{1})^{2}$ .

[L4]

Sign rules (Sign rules for products: $(- a) b = - (a b)$ and $(- a) (- b) = a b$ ): $(- u) v = - (u v)$ and $(- u) (- v) = u v$ for all reals $u, v$ , which is what turns the middle term $- 2 (a_{0} b_{1}) (a_{1} b_{0})$ into the two cross terms of a square.

[L5]

Squares (Squares of nonzero elements are positive, Multiplication by zero: $0 \cdot a = 0$ ): $u^{2} > 0$ for every $u \neq 0$ , while $0^{2} = 0 \cdot 0 = 0$ ; hence $u^{2} \geq 0$ for every real $u$ , and $u^{2} = 0$ holds exactly for $u = 0$ .

[L6]

Cauchy-Schwarz, squared form (The Cauchy-Schwarz inequality for finite sums): $(\sum_{k < n} a_{k} b_{k})^{2} \leq (\sum_{k < n} a_{k}^{2}) (\sum_{k < n} b_{k}^{2})$ for all reals and every natural $n$ , with equality if and only if the two lists are proportional, that is, there is a pair $(λ, μ) \neq (0, 0)$ with $λ a_{k} = μ b_{k}$ for all $k < n$ ; the root form of that theorem is a restatement through Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ .

Verification

technique · direct

1.1givenL1

The two-entry evaluations of [L1] give $A = a_{0}^{2} + a_{1}^{2}$ , $B = b_{0}^{2} + b_{1}^{2}$ , $C = a_{0} b_{0} + a_{1} b_{1}$ and $D = a_{0} b_{1} - a_{1} b_{0}$ , all four being real numbers determined by the given data.

1.2L2L3L4algebra

The identity: expanding both products by distributivity and collecting terms by [L2] and [L3], $A B - C^{2} = a_{0}^{2} b_{0}^{2} + a_{0}^{2} b_{1}^{2} + a_{1}^{2} b_{0}^{2} + a_{1}^{2} b_{1}^{2} - (a_{0}^{2} b_{0}^{2} + 2 (a_{0} b_{1}) (a_{1} b_{0}) + a_{1}^{2} b_{1}^{2})$ , and the outer terms cancel, leaving $a_{0}^{2} b_{1}^{2} - 2 (a_{0} b_{1}) (a_{1} b_{0}) + a_{1}^{2} b_{0}^{2}$ , which is $(a_{0} b_{1})^{2} - 2 (a_{0} b_{1}) (a_{1} b_{0}) + (a_{1} b_{0})^{2} = (a_{0} b_{1} - a_{1} b_{0})^{2} = D^{2}$ ; the sign of the cross term is the rule of [L4].

1.3L2L5algebra

The square $D^{2}$ is nonnegative and vanishes only at $D = 0$ : if $D \neq 0$ then $D^{2} > 0$ by [L5], and if $D = 0$ then $D^{2} = 0 \cdot 0 = 0$ by [L5] and [L2].

2.1step 1.2step 1.3algebra

Substituting step 1.2 into step 1.3 gives $A B - C^{2} = D^{2} \geq 0$ , that is $C^{2} \leq A B$ ; and equality $C^{2} = A B$ holds exactly when $D^{2} = 0$ , which by step 1.3 means exactly $D = 0$ , that is $a_{0} b_{1} = a_{1} b_{0}$ .

2.2step 1.2L2algebra

The instance: at $a_{0} = 1$ , $a_{1} = 2$ , $b_{0} = 3$ , $b_{1} = 4$ direct evaluation gives $A = 1 + 4 = 5$ , $B = 9 + 16 = 25$ , $C = 3 + 8 = 11$ and $D = 4 - 6 = - 2$ , so that $5 \cdot 25 - 121 = 4 = (- 2)^{2}$ , in agreement with the identity of step 1.2.

3.1step 2.1L6

The equality criteria agree: by [L6] applied at $n = 2$ , equality $C^{2} = A B$ holds if and only if the lists $(a_{0}, a_{1})$ and $(b_{0}, b_{1})$ are proportional in the symmetric sense; by step 2.1 the same equality holds if and only if $D = 0$ ; hence $a_{0} b_{1} = a_{1} b_{0}$ holds exactly when the two-entry lists are proportional, which is the identification claimed between the local criterion and the clause of [L6].

4.1step 1.2step 2.1step 2.2step 3.1L1L6∎

Collecting the results: the identity of step 1.2 holds for all reals, step 2.1 gives the inequality with its equality criterion, step 3.1 identifies that criterion with the two-entry proportionality clause of [L6], and step 2.2 verifies the numerical instance, completing the example.

Depends on

Used by

Minkowski for two-entry vectors: equality and strict cases Example

Dependency tree · two levels

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