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

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

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

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

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

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

\|v\|_1=0

v=0

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

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

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

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

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

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

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

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

\|v\|_\infty=0

v=0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Substeps and lemmas

t\in\mathbb{R}

|t|=0\iff t=0

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

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

M=|v_k|

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

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 proof

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