Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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.

Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it

Statement

Let n∈N with n≥1. A von Neumann natural is the set of its predecessors, n={0,1,…,n−1} (The natural numbers N (von Neumann)), so it can be used directly as an index set. Define

Rn:={ x:x is a function n→R },

and write xk for x(k), k<n. Two elements of Rn are equal exactly when they agree at every k<n, functions being equal when they have the same values. For x,y∈Rn put

d1(x,y):=∑k<n∣xk−yk∣,d2(x,y):= ∑k<n(xk−yk)2 ,d∞(x,y):=max⁡{ ∣xk−yk∣:k<n }.

All three are well defined: the finite sums are those of Finite sums and finite products, by recursion; the sum of squares is nonnegative (Laws of finite sums and finite products, Squares of nonzero elements are positive) so it has a unique nonnegative square root (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}); and {∣xk−yk∣:k<n} is a nonempty finite subset of R, because n≥1, so it has a maximum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

Then d1, d2 and d∞ are metrics on Rn (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

Why n≥1. For n=0 the set R0 has exactly one element, the empty function, and d1 and d2 are the empty sum 0 and its root; but d∞ would be the maximum of the empty set, which does not exist. The hypothesis n≥1 is therefore not decoration, and it is carried by every statement about d∞ in this library.

Facts & Assumptions

Given: A natural n≥1; elements x,y,z∈Rn; and the lists ak:=xk−yk, bk:=yk−zk for k<n, so that ak+bk=xk−zk. Write A:=∑k<nak2, C:=∑k<nbk2 and B:=∑k<nakbk.

[L1]

Laws of finite sums (Laws of finite sums and finite products, Finite sums and finite products, by recursion): additivity, scaling, monotonicity; a sum of nonnegative terms is nonnegative, every single term is at most the sum, and a sum of nonnegative terms that vanishes has every term 0.

[L2]

Absolute value (Basic properties of the absolute value, Absolute value in an ordered field): ∣u∣≥0; ∣u∣=0 if and only if u=0; ∣−u∣=∣u∣; and u≤∣u∣.

[L3]

Two-term triangle inequality: ∣u+v∣≤∣u∣+∣v∣ (The triangle inequality).

[L4]

Minkowski's inequality at the rational exponent p=1 (Minkowski's inequality for finite sums (rational exponent)): ∑k<n∣ak+bk∣≤∑k<n∣ak∣+∑k<n∣bk∣.

[L5]

Cauchy-Schwarz in root form (The Cauchy-Schwarz inequality for finite sums): ∣∑k<nakbk∣≤∑k<nak2 ∑k<nbk2.

[L6]

Square roots (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}): every c≥0 has a unique c≥0 with (c)2=c; in particular c=0 if and only if c=0.

[L7]

Squares (Squares of nonzero elements are positive, Integer powers am): u2≥0 always, and u2=0 only for u=0; and monotonicity of squaring on the nonnegatives, s≤t  ⟺  s2≤t2 for s,t≥0 (Squaring is monotone on the nonnegatives).

[L8]

Maximum of a nonempty finite set of reals: it exists, it belongs to the set, and it is an upper bound of the set (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L9]

Order arithmetic in R: inequalities may be added and a constant added to both sides, in the strict form of Order is preserved by adding a constant and by adding inequalities and, together with the case of equality settled by totality (Ordered field, Complete ordered field (least-upper-bound property)), in the nonstrict form used below.

Proof

technique · direct
1.1

Separation for d1: d1(x,y)=∑k<n∣ak∣ is a sum of nonnegative terms, so it vanishes exactly when every ∣ak∣ vanishes, that is exactly when xk=yk for all k<n, that is exactly when x=y.

L1L2
1.2

Separation for d2: d2(x,y)=A vanishes exactly when A=0; A is a sum of nonnegative terms, so A=0 exactly when ak2=0 for every k<n, which happens exactly when every ak=0, that is exactly when x=y.

L1L6L7
1.3

Separation for d∞: the maximum d∞(x,y) belongs to {∣ak∣:k<n} and bounds it above, so it is 0 exactly when every ∣ak∣=0, that is exactly when x=y.

L2L8
1.4

Symmetry for all three: ∣yk−xk∣=∣−(xk−yk)∣=∣xk−yk∣ and (yk−xk)2=(xk−yk)2 for every k<n, so the three defining expressions are unchanged when x and y are exchanged.

L2L7
1.5

Triangle inequality for d1: applying [L4] to the lists (ak) and (bk) gives d1(x,z)=∑k<n∣ak+bk∣≤∑k<n∣ak∣+∑k<n∣bk∣=d1(x,y)+d1(y,z).

L4
1.6

Expanding with additivity and scaling: ∑k<n(ak+bk)2=∑k<n(ak2+2akbk+bk2)=A+2B+C.

L1algebra
1.7

By [L5] and B≤∣B∣: B≤A C, and A=(A)2, C=(C)2 with A,C≥0.

L2L5L6
1.8

Triangle inequality for d∞: for each k<n, ∣ak+bk∣≤∣ak∣+∣bk∣≤d∞(x,y)+d∞(y,z) because the two maxima bound their sets; so d∞(x,y)+d∞(y,z) is an upper bound of {∣ak+bk∣:k<n}, and the maximum d∞(x,z) of that set is one of its elements, whence d∞(x,z)≤d∞(x,y)+d∞(y,z).

L3L8L9
2.1

Combining steps 1.6 and 1.7: ∑k<n(ak+bk)2=A+2B+C≤(A)2+2AC+(C)2=(A+C)2.

step 1.6step 1.7L9algebra
3.1

Both d2(x,z)=∑k<n(ak+bk)2 and A+C are nonnegative, and by step 2.1 the square of the first is at most the square of the second, so monotonicity of squaring on the nonnegatives gives d2(x,z)≤A+C=d2(x,y)+d2(y,z).

step 2.1L6L7
4.1

Each of d1, d2, d∞ satisfies (M1) by steps 1.1, 1.2 and 1.3, satisfies (M2) by step 1.4, and satisfies (M3) by steps 1.5, 3.1 and 1.8 respectively; hence all three are metrics on Rn.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.8step 3.1∎

Remarks

  • Rn is defined ZFC-natively here, as the set of functions from the von Neumann natural n to R, precisely so that its coordinates are indexed by k<n and the finite-sum machinery of Finite sums and finite products, by recursion, Minkowski's inequality for finite sums (rational exponent) and The Cauchy-Schwarz inequality for finite sums, all of which sum over k<n, applies without any reindexing.
  • No rational power appears anywhere above. The triangle inequality for d2 is obtained from Cauchy-Schwarz and the existence of square roots, not from Minkowski at p=2, so this lemma does not depend on the theory of rational exponents. Minkowski is used only at p=1, where its statement is the termwise sum of the two-term triangle inequality.
  • The three metrics are Lipschitz equivalent, with explicit constants, and in particular have the same topology; that computation is on the companion page and is not needed here.

Depends on

Used by

…and 35 more results.

Dependency tree · two levels

52 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