Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

The metrics d1d_1, d2d_2 and dd_\infty on Rn\mathbb{R}^n are metrics and are Lipschitz equivalent, with explicit constants

Example

Let n1n \ge 1 be a natural number and let Rn\mathbb{R}^n carry the three metrics

d1(x,y)=k<nxkyk,d2(x,y)=k<n(xkyk)2,d(x,y)=max{xkyk:k<n}d_1(x,y) = \sum_{k<n}|x_k-y_k|, \qquad d_2(x,y) = \sqrt{\textstyle\sum_{k<n}(x_k-y_k)^2}, \qquad d_\infty(x,y) = \max\{|x_k-y_k| : k<n\}

of Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{R}, and d1d_1, d2d_2, dd_\infty are metrics on it, where Rn\mathbb{R}^n is the set of functions from the von Neumann natural nn to R\mathbb{R}. All three are metrics (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric); that is Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{R}, and d1d_1, d2d_2, dd_\infty are metrics on it and is quoted here rather than reproved. What this example adds is that the three are Lipschitz equivalent with explicit constants (Topologically, uniformly and Lipschitz equivalent metrics on a set): for all x,yRnx, y \in \mathbb{R}^n,

d(x,y)    d2(x,y)    n  d(x,y),d(x,y)    d1(x,y)    n  d(x,y),d2(x,y)    d1(x,y)    n  d2(x,y).d_\infty(x,y) \;\le\; d_2(x,y) \;\le\; \sqrt{n}\; d_\infty(x,y), \qquad d_\infty(x,y) \;\le\; d_1(x,y) \;\le\; n\; d_\infty(x,y), \qquad d_2(x,y) \;\le\; d_1(x,y) \;\le\; \sqrt{n}\; d_2(x,y).

Consequently the three are uniformly equivalent and topologically equivalent (Lipschitz equivalence implies uniform equivalence implies topological equivalence), so they determine the same open sets, the same convergent sequences and the same continuous maps on Rn\mathbb{R}^n.

The constants are best possible: taking xyx - y with a single nonzero coordinate gives equality in d=d2=d1d_\infty = d_2 = d_1, and taking all nn coordinates equal in absolute value gives d1=ndd_1 = n\, d_\infty and d2=ndd_2 = \sqrt{n}\, d_\infty. Those two remarks are not needed for the equivalence and are not proved below.

Facts & Assumptions

Given: A natural n1n \ge 1, elements x,yRnx, y \in \mathbb{R}^n, the list uk:=xkyku_k := x_k - y_k for k<nk < n, and the abbreviations M:=d(x,y)M := d_\infty(x,y), S:=d1(x,y)=k<nukS := d_1(x,y) = \sum_{k<n}|u_k| and Q:=k<nuk2Q := \sum_{k<n} u_k^2, so that d2(x,y)=Qd_2(x,y) = \sqrt{Q}; the canonical natural nn is here read inside R\mathbb{R} as n1Rn \cdot 1_{\mathbb{R}}.

[L2]

Laws of finite sums (Laws of finite sums and finite products, Finite sums and finite products, by recursion): monotonicity, scaling, k<nλ=nλ\sum_{k<n}\lambda = n\lambda, a sum of nonnegative terms is nonnegative, and each single term is at most such a sum.

[L3]

The maximum of a nonempty finite set of reals exists, is one of its elements and bounds the set above (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L4]

Square roots (Square roots exist: a unique a0\sqrt{a} \ge 0 with (a)2=a(\sqrt{a})^2 = a; the positives are {x2:x0}\{x^2 : x \neq 0\}): every c0c \ge 0 has a unique c0\sqrt{c} \ge 0 with (c)2=c(\sqrt{c})^2 = c; hence t2=t\sqrt{t^2} = t for t0t \ge 0 and ab=ab\sqrt{ab} = \sqrt{a}\sqrt{b} for a,b0a,b \ge 0, both by uniqueness. Squaring is monotone on the nonnegatives, st    s2t2s \le t \iff s^2 \le t^2 (Squaring is monotone on the nonnegatives), so the same holds for square roots.

[L5]

Cauchy-Schwarz in root form (The Cauchy-Schwarz inequality for finite sums): k<nakbkk<nak2k<nbk2\big|\sum_{k<n} a_kb_k\big| \le \sqrt{\sum_{k<n}a_k^2}\,\sqrt{\sum_{k<n}b_k^2}.

[L6]

Absolute value (Basic properties of the absolute value, Absolute value in an ordered field, Integer powers ama^m): t0|t| \ge 0, t2=t2|t|^2 = t^2, and t=t|t| = t for t0t \ge 0.

[L7]

Order arithmetic: multiplying an inequality by a nonnegative element preserves it and inequalities may be added, in the strict forms of Sign rules for products and monotonicity of multiplication and Order is preserved by adding a constant and by adding inequalities together with the case of equality settled by totality (Ordered field, Complete ordered field (least-upper-bound property)); and n1R>0n \cdot 1_{\mathbb{R}} > 0 for n1n \ge 1 (Canonical naturals are positive and strictly increasing).

Verification

technique · direct
1.1

Since n1n \ge 1 the set {uk:k<n}\{|u_k| : k<n\} is nonempty and finite, so MM exists, equals uj|u_j| for some j<nj < n, satisfies M0M \ge 0, and bounds every uk|u_k| above.

L3L6
1.2

The reals n1Rn \cdot 1_{\mathbb{R}}, n\sqrt{n}, QQ and SS are all nonnegative, and n1R>0n \cdot 1_{\mathbb{R}} > 0, so n>0\sqrt{n} > 0; also M2=uj2M^2 = u_j^2 and uk2=uk2u_k^2 = |u_k|^2 for every kk.

L2L4L6L7
2.1

First chain: M2=uj2QM^2 = u_j^2 \le Q because a single nonnegative term is at most the sum, so M=M2Q=d2(x,y)M = \sqrt{M^2} \le \sqrt{Q} = d_2(x,y); and Q=k<nuk2k<nM2=nM2Q = \sum_{k<n}u_k^2 \le \sum_{k<n}M^2 = n M^2 by monotonicity and scaling, so d2(x,y)=QnM2=nMd_2(x,y) = \sqrt{Q} \le \sqrt{nM^2} = \sqrt{n}\,M.

step 1.1step 1.2L2L4L7
2.2

Second chain: M=ujSM = |u_j| \le S because a single nonnegative term is at most the sum; and S=k<nukk<nM=nMS = \sum_{k<n}|u_k| \le \sum_{k<n}M = nM by monotonicity and scaling.

step 1.1step 1.2L2L7
2.3

Third chain: for every k<nk < n, multiplying ukS|u_k| \le S by the nonnegative uk|u_k| gives uk2=uk2ukSu_k^2 = |u_k|^2 \le |u_k| S, so summing and scaling gives QSk<nuk=S2Q \le S \sum_{k<n}|u_k| = S^2 and hence d2(x,y)=QS2=S=d1(x,y)d_2(x,y) = \sqrt{Q} \le \sqrt{S^2} = S = d_1(x,y); and Cauchy-Schwarz applied to the lists ak:=uka_k := |u_k| and bk:=1b_k := 1 gives S=k<nuk1k<nuk2 k<n1=Qn=nd2(x,y)S = \big|\sum_{k<n}|u_k|\cdot 1\big| \le \sqrt{\sum_{k<n}u_k^2}\ \sqrt{\sum_{k<n}1} = \sqrt{Q}\,\sqrt{n} = \sqrt{n}\, d_2(x,y).

step 1.1step 1.2L2L4L5L6L7
3.1

The three chains are exactly Lipschitz equivalences with positive constants: 1dd2nd1 \cdot d_\infty \le d_2 \le \sqrt{n}\, d_\infty, 1dd1nd1 \cdot d_\infty \le d_1 \le n\, d_\infty and 1d2d1nd21 \cdot d_2 \le d_1 \le \sqrt{n}\, d_2, the constants 11, n\sqrt{n} and nn all being positive.

step 2.1step 2.2step 2.3L7L8
4.1

Hence any two of d1d_1, d2d_2, dd_\infty are Lipschitz equivalent, and therefore uniformly equivalent and topologically equivalent; all three induce the same topology on Rn\mathbb{R}^n.

step 3.1L1L8

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 87 results over 30 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources