LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01

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 reverse triangle inequality in a normed space

Statement

Let $V$ be a normed space. For all $x, y \in V$ , $∣ ∥ x ∥ - ∥ y ∥ ∣ \leq ∥ x - y ∥ .$ In particular, the norm map is $1$ -Lipschitz for the norm metric.

Facts & Assumptions

Given: A normed space $V$ and vectors $x, y \in V$ .

[L1]

A norm satisfies the triangle inequality and absolute homogeneity (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

Proof

technique · direct

1.1L1

Since $x = (x - y) + y$ , the triangle inequality in [L1] gives $∥ x ∥ \leq ∥ x - y ∥ + ∥ y ∥$ .

1.2L1algebra

Since $y = (y - x) + x$ and $∥ y - x ∥ = ∥ x - y ∥$ by absolute homogeneity at the scalar $- 1$ , [L1] also gives $∥ y ∥ \leq ∥ x - y ∥ + ∥ x ∥$ .

2.1step 1.1step 1.2algebra

Step 1.1 yields $∥ x ∥ - ∥ y ∥ \leq ∥ x - y ∥$ , and step 1.2 yields $∥ y ∥ - ∥ x ∥ \leq ∥ x - y ∥$ ; together these are exactly $∣ ∥ x ∥ - ∥ y ∥ ∣ \leq ∥ x - y ∥$ .

3.1step 2.1∎

The displayed inequality says precisely that the map $x \mapsto ∥ x ∥$ is $1$ -Lipschitz for the metric $d (u, v) = ∥ u - v ∥$ .

Depends on

A norm on a real vector space, the induced metric, and the dictionary with the metric axioms

The reverse triangle inequality in a normed space

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources