Inner-product-induced norm: proving √⟨x,x⟩ is a norm and computing exactly for a positive-definite matrix on ℝ²

Goal and scope

In any real inner-product space, prove that N(v)=√⟨v,v⟩ is a norm: nonnegativity and separation, absolute homogeneity, and the triangle inequality (via a fully proved Cauchy–Schwarz inequality). Then, on ℝ² with the inner product given by A=[[2,1],[1,2]], compute exactly the squared norms and the squared distance for x=(1,0) and y=(0,1), and check Cauchy–Schwarz, the triangle inequality and the parallelogram identity on this instance.

Works inside the MKO's scope: one real inner-product space; the concrete example uses a matrix inner product on ℝ² that already qualifies as bilinear, symmetric and positive definite (assumption a1), with square roots kept as exact symbols (assumption a2). The norm axioms are proved in full for a general real inner-product space; checks on particular vectors are instances only and do not replace the universal proofs. Completeness and Hilbert spaces are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• sqrt_def
• square_nonneg
• abs_rules
• order_basics
• vector_space_axioms
• case_analysis

• G1 — V is a real inner-product space: ⟨·,·⟩:V×V→ℝ is linear in each argument (bilinear), symmetric ⟨u,v⟩=⟨v,u⟩, and positive definite: ⟨v,v⟩≥0, with ⟨v,v⟩=0 ⇔ v=0.
• G2 — Concrete example: V=ℝ², ⟨u,v⟩=uᵀAv=2u₁v₁+u₁v₂+u₂v₁+2u₂v₂, where A=[[2,1],[1,2]] already qualifies as bilinear, symmetric and positive definite (MKO assumption a1); x=(1,0) and y=(0,1) lie in the same ℝ².
• G3 — Define N(v)=√⟨v,v⟩ (MKO statement).

• \langle u,v\rangle — the inner product
• N(v)=\sqrt{\langle v,v\rangle} — the inner-product-induced norm
• A=\begin{pmatrix}2&1\\1&2\end{pmatrix} — the matrix defining the inner product on ℝ²
• x=(1,0),\ y=(0,1) — the two example vectors
• |c| — the absolute value of the real c

Rules and sources

• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• 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.
• 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.
• 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.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• 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.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• 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.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• 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.
• matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• mko_ip_norm_def · cited — In one real inner-product space define norm(x)=sqrt(<x,x>). Positive definiteness gives separation, homogeneity gives absolute homogeneity, and Cauchy–Schwarz gives the triangle inequality. This slice calculates exact squared norms and identities for positive-definite matrices on R² without replacing universal certificates with vector samples. · mko-inner-product-induced-norm
• ip_axioms · prerequisite — Inner-product axioms: ⟨au+bw,v⟩=a⟨u,v⟩+b⟨w,v⟩ (likewise in the second argument); ⟨u,v⟩=⟨v,u⟩; ⟨v,v⟩≥0 and ⟨v,v⟩=0 ⇔ v=0.
• norm_def · prerequisite — A norm N on a real vector space: N(v)≥0 with N(v)=0 ⇔ v=0; N(cv)=|c|N(v); N(u+v)≤N(u)+N(v).
• L_sqrt_scale · lemma — For a real c and s≥0: √(c²s)=|c|√s.
• L_cs · lemma — Cauchy–Schwarz: in a real inner-product space, ⟨x,y⟩²≤⟨x,x⟩⟨y,y⟩ for all x, y.
• L_sq_order · lemma — For reals u≥0 and w≥0: if u²≤w², then u≤w.

Main derivation

\langle v,v\rangle\ge 0

N(v)=\sqrt{\langle v,v\rangle}\ \text{defined},\ N(v)\ge 0

N(v)=0

v=0

\langle cv,cv\rangle

c^2\langle v,v\rangle

N(cv)=\sqrt{c^2\langle v,v\rangle}

N(cv)=|c|\,N(v)

\langle x\pm y,x\pm y\rangle

\langle x,x\rangle\pm2\langle x,y\rangle+\langle y,y\rangle

x,y\in V

\langle x,y\rangle^2\le\langle x,x\rangle\langle y,y\rangle

\langle x,y\rangle^2\le N(x)^2N(y)^2

|\langle x,y\rangle|\le N(x)N(y)

N(x+y)^2=\langle x,x\rangle+2\langle x,y\rangle+\langle y,y\rangle

N(x+y)^2\le\big(N(x)+N(y)\big)^2

N(x+y)^2\le\big(N(x)+N(y)\big)^2

N(x+y)\le N(x)+N(y)

\text{S01, S02, S04, S09}

N\ \text{is a norm on}\ V

v^{\mathsf T}Av=2v_1^2+2v_1v_2+2v_2^2

v_1^2+v_2^2+(v_1+v_2)^2

x=(1,0),\ y=(0,1)

\langle x,x\rangle=2,\ \langle y,y\rangle=2,\ \langle x,y\rangle=1,\ N(x)=N(y)=\sqrt2

\langle x\mp y,x\mp y\rangle

\langle x-y,x-y\rangle=2,\ \langle x+y,x+y\rangle=6

\text{values of S12, S13}

1\le4,\ \ 6\le8,\ \ 6+2=2(2+2)

\text{S10 to S14}

N\ \text{norm};\ N(x)=N(y)=N(x-y)=\sqrt2,\ N(x+y)=\sqrt6

Substeps and lemmas

\sqrt{c^2s},\ s\ge0

|c|\sqrt{s}

y=0

\langle x,0\rangle^2=0=\langle x,x\rangle\langle 0,0\rangle

y\neq0,\ t\in\mathbb{R}

0\le\langle x,x\rangle-2t\langle x,y\rangle+t^2\langle y,y\rangle

t=\frac{\langle x,y\rangle}{\langle y,y\rangle}

\langle x,y\rangle^2\le\langle x,x\rangle\langle y,y\rangle

u,w\ge0,\ u^2\le w^2

u\le w

Reverse audits

• S15 · sufficient_goal_reduction · S10, S12, S13, S14 — Goal G: the norm theorem and the exact values of the instance. Sufficient condition H: S10 and S12 to S14; H⇒G by conjunction. H is proved forwards from G1 to G3, and no finite sample replaces a universal proof.
• S14 · premise_audit · S12, S13, numeric_evaluation — The numbers can be recomputed independently; but finitely many vectors passing a check cannot establish a universal statement, and the universal part is proved in S06 to S10.
• S13 · inverse_equivalence · S05, S12, eq_replace — Replacement of equals in an identity, so both sides have the same value; two methods (expansion and direct) give the same result.
• S12 · inverse_equivalence · matrix_product_def, sqrt_def — Each value can be recomputed directly from the formula in G2; both sides are the same number.
• S11 · inverse_equivalence · distributive, square_nonneg — Both sides are the same polynomial, so the step is two-way; N1 checks the identity of degree at most 2 on a 3×3 grid, which decides it.
• S10 · sufficient_goal_reduction · S01, S02, S04, S09, norm_def — Goal G: N is a norm. Sufficient condition H: the three clauses of the definition; H⇒G by definition. H is proved forwards from G1.
• S09 · premise_audit · S08, S01, L_sq_order — Both sides must be nonnegative, which S01 provides.
• S08 · premise_audit · S05, S07, order_basics, abs_rules — This is exactly where Cauchy–Schwarz yields the triangle inequality (MKO); no converse is claimed.
• S07.1 · premise_audit · order_basics, contrapositive — The lemma keeps u≥0 and w≥0 as sufficient hypotheses, but this one-way proof does not separately need u≥0: its contrapositive assumption u>w≥0 already yields u>0. If u<0≤w the conclusion holds immediately. The condition w≥0 supplies the upper-bound sign needed for the implication. The converse holds when both are nonnegative, but is not needed here.
• S07 · premise_audit · S06, S01, L_sq_order, abs_rules — Here u=|⟨x,y⟩| and w=N(x)N(y) are both nonnegative, so the stated lemma applies. This does not make u≥0 necessary for the one-way implication. Removing w≥0 can fail: 1²≤(−2)² yet 1>−2.
• S06.3 · premise_audit · S06.2, forall_elim, order_basics, mul_inverse_nonzero — It needs c>0: dividing by c needs c≠0, and multiplying by c without reversing the inequality needs c>0; both come from y≠0 and positive definiteness.
• S06.2 · premise_audit · ip_axioms, S05 — The inequality holds for every t, which is what lets the next step choose a particular t.
• S06.1 · premise_audit · ip_axioms, mul_zero — Only linearity is used; this case must be handled separately because S06.3 divides by ⟨y,y⟩.
• S06 · premise_audit · G1, L_cs — It needs bilinearity, symmetry and positive definiteness; it does not claim when equality holds.
• S05 · inverse_equivalence · ip_axioms, distributive — An identity for all x and y, so two-way. The cross term must be kept: the Pythagorean form appears only when ⟨x,y⟩=0.
• S04.1 · inverse_equivalence · sqrt_def, abs_rules — By uniqueness the two expressions name the same number. Replacing |c| by c fails for c<0 and s>0, since c√s<0 cannot be a principal square root. For s=0 both expressions are zero, so no strict-negative argument applies.
• S04 · inverse_equivalence · L_sqrt_scale — Both sides are two expressions for the same real number, so it holds both ways.
• S03 · inverse_equivalence · ip_axioms, mul_assoc — This is an identity, equal for all c and v, so it holds both ways.
• S02 · inverse_equivalence · sqrt_def, ip_axioms — Both equivalences are two-way: uniqueness of the square root and the 'if and only if' of positive definiteness.
• S01 · premise_audit · G1, sqrt_def — It uses only ⟨v,v⟩≥0 and the definition of the principal square root.

Error controls and negative controls

Passing samples is not a universal proof

The MKO's misconception: declaring a general norm after seeing the triangle inequality hold for some vectors. In S14, 6≤8 only says that the pair x, y does not violate it; that the triangle inequality holds for all vectors comes from the proof in S06 to S09, which uses no particular vectors.

An induced norm is not yet a Hilbert space

The MKO's second misconception is to call a space Hilbert directly because its norm comes from an inner product. A Hilbert space also requires completeness with respect to this norm, a separate property that neither Cauchy–Schwarz nor the parallelogram identity implies. This guide neither proves nor uses completeness.

The cross term and the absolute value

The two easiest slips: the cross term 2⟨x,y⟩ in S05 cannot be dropped (here ⟨x−y,x−y⟩=2, not 4), and the factor in S04 is |c|, not c (N(−3x)=3√2, not −3√2). Also √ does not distribute over addition: N(x+y)=√6≠√2+√2.

• x, y and x+y all satisfy the triangle inequality, so N is a norm on every inner-product space → reject — Finitely many instances cannot prove a universal statement; the universal proof is S06 to S09.
• N(x+y)=N(x)+N(y)=2√2 → reject — N(x+y)²=6 while (2√2)²=8, and 6≠8; the triangle inequality need not hold with equality.
• By Pythagoras, N(x−y)²=N(x)²+N(y)²=4 → reject — Under this inner product ⟨x,y⟩=1≠0, and the cross term −2 makes N(x−y)²=2 (S13).
• Every symmetric matrix defines an inner product, for example B=[[1,2],[2,1]] → reject — For v=(1,−1), vᵀBv=1−2−2+1=−2<0 (N10), so B is not positive definite and √ is undefined.
• The norm comes from an inner product, so (V,N) must be a Hilbert space → reject — A Hilbert space additionally needs completeness, which neither this guide nor the MKO derives from the induced norm.

Result and limitations

In every real inner-product space, N(v)=√⟨v,v⟩ is a norm: positive definiteness gives nonnegativity and separation, bilinearity gives N(cv)=|c|N(v), and the fully proved Cauchy–Schwarz inequality ⟨x,y⟩²≤⟨x,x⟩⟨y,y⟩ gives the triangle inequality. On ℝ² with the inner product given by A=[[2,1],[1,2]], ⟨x,x⟩=⟨y,y⟩=2 and ⟨x,y⟩=1, so N(x)=N(y)=√2, the squared distance is ⟨x−y,x−y⟩=2 and ⟨x+y,x+y⟩=6; the instance satisfies 1≤4, 6≤8 and 6+2=2(2+2).

• Completeness (and hence Hilbert spaces, the MKO's next step) is outside this guide: it neither proves that ℝ² is complete under this norm nor gives an incomplete example.
• N1 and N2 are polynomial-identity checks on a grid; N3 to N9 are valid for this example's numbers only.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: c4ddbc627d1b1a07ab027fee5efedc07a1bcf302d187aa0e3c6b47ad21ca3b2f
• original source SHA-256: 5c985ba54e11c7600e0ba5b543ac1e169154c8abd3f78b01cd3b3d654e479277
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)