# Real normed vector space: universal norm certificates for the ℓ¹ and ℓ^∞ formulas, and two formulas that are not norms

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-real-normed-vector-space/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-real-normed-vector-space-01 · production-20261019-adopted-96



## Goal and scope

On ℝⁿ (n≥1 fixed), for all vectors u, v and all reals a, prove that ‖v‖₁=Σ|v_i| and ‖v‖_∞=max|v_i| both satisfy the three norm axioms: nonnegativity with ‖v‖=0 ⇔ v=0, ‖av‖=|a|‖v‖, and ‖u+v‖≤‖u‖+‖v‖. Then, in ℝ³, compute both norms and instances of the triangle inequality and homogeneity for the integer-coordinate vectors u=(3,−4,1) and v=(−1,2,5); finally show that φ(v)=|v₁| and ψ(v)=(‖v‖₁)² are not norms.

Stays inside the MKO's slice: only the named ℓ¹ and ℓ^∞ formulas on ℝⁿ, with qualification coming from algebraic certificates valid for all vectors and scalars; concrete examples use integer-coordinate vectors. Induced metrics, completeness (Banach spaces), equivalence of norms and bounded operators are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- abs_rules
- finite_sum_rules
- order_basics
- vector_space_axioms
- forall_intro
- quantifier_negation


- G1 — n≥1 is fixed; ℝⁿ is a real vector space with coordinatewise addition and scalar multiplication; v=0 exactly when every v_i=0.
- G2 — Named formulas: ‖v‖₁=Σ_{i=1}^{n}|v_i| and ‖v‖_∞=max_{1≤i≤n}|v_i|.
- G3 — Norm axioms (MKO): (N1) ‖v‖≥0, and ‖v‖=0 ⇔ v=0; (N2) ‖av‖=|a|‖v‖; (N3) ‖u+v‖≤‖u‖+‖v‖; all three must hold for all u,v∈ℝⁿ and a∈ℝ.
- G4 — Concrete data in ℝ³: u=(3,−4,1) and v=(−1,2,5); candidate formulas φ(v)=|v₁| and ψ(v)=(‖v‖₁)².


- v=(v_i)_{i=1}^{n} — a vector of ℝⁿ and its coordinates
- \|v\|_1=\sum_{i=1}^{n}|v_i| — the ℓ¹ norm: sum of absolute values of coordinates
- \|v\|_\infty=\max_{1\le i\le n}|v_i| — the ℓ^∞ norm: largest absolute value of a coordinate
- (N1),(N2),(N3) — the three norm axioms: definiteness, homogeneity, triangle inequality
- e_1,\ e_2 — the standard basis vectors (1,0,0) and (0,1,0) of ℝ³
- \varphi,\ \psi — two candidate formulas under review





## Rules and sources


- abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
- finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- vector_space_axioms · prerequisite — Vector space axioms (over ℝ or another field F): vectors form a commutative group under addition; scalar multiplication satisfies a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu) and 1u=u.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- mko_norm · cited — A norm sends vectors to nonnegative real numbers, with norm(v)=0 iff v=0, norm(av)=|a| norm(v), and norm(u+v)≤norm(u)+norm(v). This slice uses only the named l1 and linfinity formulas on ℝⁿ; qualification comes from universal algebraic certificates for the formulas, and finite samples do not stand in for general norm proofs. · mko-real-normed-vector-space
- coord_ops · prerequisite — Coordinatewise operations: (u+v)_i=u_i+v_i and (av)_i=a v_i; v=0 ⇔ every v_i=0.
- sum_order · prerequisite — Finite sums and order: if s_i≤t_i for every i, then Σs_i≤Σt_i; if every s_i≥0, then Σs_i≥0 and Σs_i≥s_j for every j.
- max_finite · prerequisite — Maximum of finitely many reals: for t_i (1≤i≤n, n≥1), M=max_i t_i exists and equals some t_k; t_i≤M for every i; if t_i≤K for every i, then M≤K.
- mono_nonneg · prerequisite — Multiplying by a nonnegative number keeps the inequality: if u≤v and w≥0, then wu≤wv.
- ineq_add · prerequisite — Adding inequalities: if u₁≤v₁ and u₂≤v₂, then u₁+u₂≤v₁+v₂.
- L_abs_zero · lemma — For a real t: |t|=0 ⇔ t=0.





## Main derivation

S01 · definitionBefore

\|\cdot\|_1,\ \|\cdot\|_\infty\ \text{are norms on}\ \mathbb{R}^n

After

(N1)\land(N2)\land(N3)\ \text{for all } u,v\in\mathbb{R}^n,\ a\in\mathbb{R},\ \text{for each formula}

Conditions: none

Rule: mko_norm · Uses: G2, G3, mko_norm

Leaf basis: mko_norm + def_unfold

By the MKO, a formula is a norm exactly when the three axioms hold for all vectors and all scalars. What is needed is therefore a universal certificate: every step argues for arbitrary u, v, a, rather than substituting a few vectors.



S02 · impliesBefore

|v_i|\ge 0\ \text{for every } i

After

\|v\|_1=\sum_{i=1}^{n}|v_i|\ge 0

Conditions: none

Rule: sum_order · Uses: G2, abs_rules, sum_order

Leaf basis: abs_rules + sum_order

Absolute values are nonnegative: every |v_i|≥0. A finite sum of nonnegative numbers is nonnegative, so ‖v‖₁≥0 (the first half of N1).



S03 · equivalentBefore

\|v\|_1=0

After

v=0

Conditions: none

Rule: sum_order · Uses: S02, G1, sum_order, L_abs_zero

Leaf basis: sum_order + L_abs_zero + coord_ops

Forward: if ‖v‖₁=0, then for every j, 0≤|v_j|≤Σ|v_i|=0 (a sum of nonnegative terms is at least each term), so |v_j|=0; by Lemma L_abs_zero (S03.1), v_j=0; every coordinate is 0, that is v=0. Backward: if v=0 then every |v_i|=|0|=0 and the sum is 0. This is the second half of N1.



S04 · equivalentBefore

\|av\|_1=\sum_{i=1}^{n}|a v_i|

After

\|av\|_1=\sum_{i=1}^{n}|a||v_i|=|a|\,\|v\|_1

Conditions: none

Rule: finite_sum_rules · Uses: G1, G2, abs_rules, finite_sum_rules

Leaf basis: coord_ops + abs_rules + finite_sum_rules

(av)_i=a v_i and |a v_i|=|a||v_i|; the constant |a| factors out of the finite sum: Σ|a||v_i|=|a|Σ|v_i|. This holds for arbitrary a and v, which is N2.



S05 · impliesBefore

\|u+v\|_1=\sum_{i=1}^{n}|u_i+v_i|

After

\|u+v\|_1\le\sum_{i=1}^{n}(|u_i|+|v_i|)=\|u\|_1+\|v\|_1

Conditions: none

Rule: sum_order · Uses: G1, G2, abs_rules, sum_order, finite_sum_rules

Leaf basis: abs_rules + sum_order + finite_sum_rules + coord_ops

In each coordinate use the real triangle inequality |u_i+v_i|≤|u_i|+|v_i|; adding the termwise inequalities gives the inequality for the sums; then split Σ(|u_i|+|v_i|) into Σ|u_i|+Σ|v_i|. This holds for arbitrary u and v, which is N3.



S06 · impliesBefore

(N1),(N2),(N3)\ \text{for}\ \|\cdot\|_1\ \text{with arbitrary } u,v,a

After

\|\cdot\|_1\ \text{is a norm on}\ \mathbb{R}^n

Conditions: none

Rule: forall_intro · Uses: S02, S03, S04, S05, forall_intro

Leaf basis: forall_intro + and_intro_elim

S02 to S05 prove the three axioms for arbitrary u, v, a, without using particular values; by ∀-introduction and conjunction, the ℓ¹ formula is a norm on ℝⁿ.



S07 · impliesBefore

\|v\|_\infty=\max_i|v_i|

After

\|v\|_\infty=|v_k|\ge 0\ \text{for some } k

Conditions: n\ge 1

Rule: max_finite · Uses: G2, max_finite, abs_rules

Leaf basis: max_finite + abs_rules

Since n≥1, the maximum of finitely many numbers exists and equals some |v_k|, and absolute values are nonnegative, so ‖v‖_∞≥0 (the first half of N1).



S08 · equivalentBefore

\|v\|_\infty=0

After

v=0

Conditions: none

Rule: max_finite · Uses: S07, G1, max_finite, L_abs_zero

Leaf basis: max_finite + L_abs_zero + coord_ops

Forward: if max|v_i|=0, then 0≤|v_i|≤0 for every i, so |v_i|=0 and by L_abs_zero v_i=0, that is v=0. Backward: if v=0, every |v_i|=0 and the maximum is 0.



S09 · equivalentBefore

\|av\|_\infty=\max_i|a||v_i|

After

\|av\|_\infty=|a|\max_i|v_i|=|a|\,\|v\|_\infty

Conditions: |a|\ge 0

Rule: max_finite · Uses: G1, G2, abs_rules, max_finite, mono_nonneg

Leaf basis: abs_rules + max_finite + mono_nonneg + order_basics

|(av)_i|=|a||v_i|. Let M=max|v_i|=|v_k|. Upper bound (S09.1): every |a||v_i|≤|a|M, so the maximum is ≤|a|M; lower bound (S09.2): |a||v_k|=|a|M is itself one of the values, so the maximum is ≥|a|M. Together they are equal, which is N2. What is factored out is |a|≥0, not a.



S10 · impliesBefore

|u_i+v_i|\ \text{for each } i

After

\|u+v\|_\infty\le\|u\|_\infty+\|v\|_\infty

Conditions: none

Rule: max_finite · Uses: G1, G2, abs_rules, max_finite, ineq_add

Leaf basis: abs_rules + max_finite + ineq_add + coord_ops

For each i: |u_i+v_i|≤|u_i|+|v_i| (triangle inequality), while |u_i|≤‖u‖_∞ and |v_i|≤‖v‖_∞; adding gives |u_i+v_i|≤‖u‖_∞+‖v‖_∞. Every value is at most the same bound K=‖u‖_∞+‖v‖_∞, so the maximum is at most K. This is N3.



S11 · impliesBefore

(N1),(N2),(N3)\ \text{for}\ \|\cdot\|_\infty\ \text{with arbitrary } u,v,a

After

\|\cdot\|_\infty\ \text{is a norm on}\ \mathbb{R}^n

Conditions: none

Rule: forall_intro · Uses: S07, S08, S09, S10, forall_intro

Leaf basis: forall_intro + and_intro_elim

S07 to S10 prove the three axioms for arbitrary u, v, a; by ∀-introduction and conjunction, the ℓ^∞ formula is a norm on ℝⁿ.



S12 · impliesBefore

u=(3,-4,1),\ v=(-1,2,5)

After

\|u\|_1=8,\ \|u\|_\infty=4,\ \|v\|_1=8,\ \|v\|_\infty=5

Conditions: none

Rule: numeric_evaluation · Uses: G4, G2

Leaf basis: numeric_evaluation + abs_rules

Apply the formulas: ‖u‖₁=3+4+1=8 and ‖u‖_∞=max(3,4,1)=4; ‖v‖₁=1+2+5=8 and ‖v‖_∞=max(1,2,5)=5. The two vectors have the same ℓ¹ norm but different ℓ^∞ norms: different norms measure size differently.



S13 · impliesBefore

u+v=(2,-2,6)

After

\|u+v\|_1=10\le 16,\ \|u+v\|_\infty=6\le 9

Conditions: none

Rule: numeric_evaluation · Uses: S12, S05, S10

Leaf basis: numeric_evaluation + coord_ops

u+v=(2,−2,6). ‖u+v‖₁=2+2+6=10≤8+8=16; ‖u+v‖_∞=6≤4+5=9. These values agree with the general results of S05 and S10, but they are instances only, not proofs.



S14 · impliesBefore

-2u=(-6,8,-2)

After

\|-2u\|_1=16=|-2|\cdot 8,\ \|-2u\|_\infty=8=|-2|\cdot 4

Conditions: none

Rule: numeric_evaluation · Uses: S12, S04, S09

Leaf basis: numeric_evaluation + coord_ops

−2u=(−6,8,−2). ‖−2u‖₁=6+8+2=16=2·8 and ‖−2u‖_∞=8=2·4. The factor is |−2|=2, not −2; a norm is never negative.



S15 · impliesBefore

\varphi(v)=|v_1|\ \text{on}\ \mathbb{R}^3

After

\varphi(0,1,0)=0,\ (0,1,0)\neq 0;\ \varphi\ \text{is not a norm}

Conditions: none

Rule: quantifier_negation · Uses: G4, quantifier_negation, G3

Leaf basis: quantifier_negation + abs_rules + numeric_evaluation

φ satisfies nonnegativity, homogeneity (|a v₁|=|a||v₁|) and the triangle inequality (|u₁+v₁|≤|u₁|+|v₁|), all for every vector. But N1 requires φ(v)=0 only when v=0; v=(0,1,0)≠0 has φ(v)=|0|=0. One counterexample refutes this universal axiom, so φ is not a norm (it is only a seminorm).



S16 · impliesBefore

\psi(v)=(\|v\|_1)^2,\ e_1=(1,0,0),\ e_2=(0,1,0)

After

\psi(e_1+e_2)=4>2=\psi(e_1)+\psi(e_2);\ \psi(2e_1)=4\neq 2=|2|\psi(e_1)

Conditions: none

Rule: quantifier_negation · Uses: G4, S06, quantifier_negation

Leaf basis: quantifier_negation + numeric_evaluation + power_laws

ψ≥0, and by S03 ψ(v)=0 ⇔ ‖v‖₁=0 ⇔ v=0, so N1 holds. But ψ(e₁+e₂)=(1+1)²=4 while ψ(e₁)+ψ(e₂)=1+1=2, so the triangle inequality fails; ψ(2e₁)=2²=4 while |2|ψ(e₁)=2, so homogeneity fails too. Hence ψ is not a norm.







## Substeps and lemmas

S03.1 · equivalentBefore

t\in\mathbb{R}

After

|t|=0\iff t=0

Conditions: none

Rule: case_analysis · Uses: abs_rules, case_analysis

Leaf basis: abs_rules + case_analysis + order_basics

If t=0, |0|=0. If t≠0 there are two cases: for t>0, |t|=t>0; for t<0, |t|=−t>0. In both cases |t|≠0. So |t|=0 holds exactly when t=0. This proves Lemma L_abs_zero.



S09.1 · impliesBefore

|v_i|\le M\ \text{for every } i,\ |a|\ge 0

After

\max_i|a||v_i|\le|a|M

Conditions: |a|\ge 0

Rule: mono_nonneg · Uses: max_finite, mono_nonneg, abs_rules

Leaf basis: mono_nonneg + max_finite

Every |v_i|≤M; multiplying by |a|≥0 keeps the direction: |a||v_i|≤|a|M. All values are at most |a|M, so their maximum is too.



S09.2 · impliesBefore

M=|v_k|

After

|a|M=|a||v_k|\le\max_i|a||v_i|

Conditions: none

Rule: max_finite · Uses: S09.1, max_finite

Leaf basis: max_finite

The maximum M is attained by some |v_k|, so |a|M=|a||v_k| is one of the numbers whose maximum is taken and is at most that maximum. Together with S09.1 this gives equality.







## Reverse audits


- S16 · premise_audit · S03, quantifier_negation, numeric_evaluation — Each failing axiom needs only one exact counterexample; ψ passing N1 cannot repair it.
- S15 · premise_audit · G3, quantifier_negation, abs_rules — A refutation needs one vector; the other two axioms holding cannot repair it.
- S14 · premise_audit · S12, numeric_evaluation — An instance consistent with S04 and S09; not used as a proof.
- S13 · premise_audit · S12, numeric_evaluation — Exact computation; it implies no universal conclusion.
- S12 · premise_audit · G4, numeric_evaluation — Exact integer arithmetic; it concerns these two vectors only.
- S11 · premise_audit · S07, S08, S09, S10, forall_intro, and_intro_elim — None of the three axioms may be missing.
- S10 · premise_audit · abs_rules, max_finite, ineq_add — It needs a common bound independent of i; equality is not claimed.
- S09.2 · premise_audit · max_finite — It needs the maximum to be attained (finitely many numbers).
- S09.1 · premise_audit · max_finite, mono_nonneg — It needs a nonnegative multiplier; multiplying by a negative number would reverse the direction (see the error controls).
- S09 · inverse_equivalence · abs_rules, max_finite, mono_nonneg — Both sides are the same number (the upper and lower bounds agree), so the equality holds both ways; the key condition is |a|≥0.
- S08 · inverse_equivalence · max_finite, L_abs_zero, G1 — Forward uses 'each term is at most the maximum' and L_abs_zero, backward uses |0|=0; both directions have reasons.
- S07 · premise_audit · max_finite, abs_rules — It needs n≥1 so that the maximum exists; no converse is claimed.
- S06 · premise_audit · S02, S03, S04, S05, forall_intro, and_intro_elim — None of the three axioms may be missing.
- S05 · premise_audit · abs_rules, sum_order, finite_sum_rules — It needs the coordinatewise triangle inequality; equality is not claimed.
- S04 · inverse_equivalence · abs_rules, finite_sum_rules, coord_ops — Every equality is a rewrite into an equal expression and can be read backwards.
- S03.1 · inverse_equivalence · abs_rules, case_analysis, order_basics — The cases t=0, t>0, t<0 cover every real (trichotomy) and both directions are argued; L_abs_zero itself is not used.
- S03 · inverse_equivalence · sum_order, L_abs_zero, G1 — Each direction has its own reason: forward uses 'the sum is at least each term' and L_abs_zero; backward uses |0|=0.
- S02 · premise_audit · abs_rules, sum_order — Only the nonnegativity of absolute values is needed; no converse is claimed.
- S01 · premise_audit · G3, mko_norm — This step only lists the obligations and derives no new fact.





## Error controls and negative controls

Passing tests at finitely many points is not a norm proofThe mistake named by the MKO is to declare an arbitrary formula a norm because it passes nonnegativity and triangle tests at finitely many points. ψ is nonnegative everywhere and passes the triangle test on e₁ and −e₁ (ψ(0)=0≤1+1), yet fails on e₁ and e₂ (S16). The values in S13 and S14 for ℓ¹ and ℓ^∞ are likewise only instances; qualification comes from the universal certificates of S02 to S11.

Check all three axioms: a seminorm need not be a normφ(v)=|v₁| satisfies nonnegativity, homogeneity and the triangle inequality for all vectors, which makes it easy to mistake for a norm; what fails is 'zero only at v=0' (S15). Definiteness must be proved just like the other two axioms.

Homogeneity of the maximum factors out |a|max_i(c t_i)=c·max_i t_i holds only for c≥0: with t=(1,3) and c=−1, max(−1,−3)=−1 while −1·max(1,3)=−3. S09 first writes |a v_i| as |a||v_i| and then factors out the nonnegative |a|, which is what allows the monotonicity of S09.1.


- ψ(v)=(‖v‖₁)² is nonnegative everywhere and passes the triangle inequality on e₁ and −e₁, so ψ is a norm → reject — ψ(e₁+e₂)=4>2=ψ(e₁)+ψ(e₂).
- φ(v)=|v₁| is a norm on ℝ³ → reject — φ(0,1,0)=0 although (0,1,0)≠0.
- The example ‖u+v‖₁=10≤16 proves the triangle inequality for ℓ¹ → reject — One instance is not a universal proof; the proof is the coordinatewise argument of S05.
- For every real c, max_i(c t_i)=c·max_i t_i → reject — c=−1, t=(1,3): the left side is −1 and the right side is −3.





## Result and limitations

For every n≥1, all u,v∈ℝⁿ and a∈ℝ, ‖v‖₁=Σ|v_i| and ‖v‖_∞=max|v_i| satisfy (N1) nonnegativity with value 0 only at v=0, (N2) ‖av‖=|a|‖v‖, and (N3) the triangle inequality, so both are norms on ℝⁿ. Example: u=(3,−4,1) and v=(−1,2,5) have ‖u‖₁=‖v‖₁=8, ‖u‖_∞=4, ‖v‖_∞=5, ‖u+v‖₁=10≤16 and ‖u+v‖_∞=6≤9. φ(v)=|v₁| is not a norm since φ(0,1,0)=0; ψ(v)=(‖v‖₁)² is not a norm since ψ(e₁+e₂)=4>2.


- sum_order, max_finite, mono_nonneg, ineq_add and coord_ops are premises of this guide and are not derived here from the axioms of the reals.
- N1 to N10 are only the values for the concrete vectors of S12 to S14; the norm qualification does not depend on them. Induced metrics and Banach spaces belong to the MKO's formal next.





## Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 69969d495840bc7b4387481a8711aa588a4d19c47ffa88dc52585857ed099067
- original source SHA-256: 69969d495840bc7b4387481a8711aa588a4d19c47ffa88dc52585857ed099067
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-real-normed-vector-space-01.json)