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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-inner-product-induced-norm/)

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-inner-product-induced-norm-01 · production-20261019-adopted-96



## 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

S01 · impliesBefore

\langle v,v\rangle\ge 0

After

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

Conditions: \langle v,v\rangle\ge0

Rule: sqrt_def · Uses: G1, G3

Leaf basis: sqrt_def + ip_axioms

Positive definiteness gives ⟨v,v⟩≥0, so the principal square root is defined, and by definition it is nonnegative, so N(v)≥0. If ⟨v,v⟩ could be negative (as for a symmetric matrix that is not positive definite), N would not even be defined.



S02 · equivalentBefore

N(v)=0

After

v=0

Conditions: none

Rule: ip_axioms · Uses: S01, G1

Leaf basis: sqrt_def + ip_axioms + logic_chain

N(v)=0 ⇔ ⟨v,v⟩=0, because √s=0 ⇔ s=0 (0 is the only nonnegative square root of 0). Then positive definiteness gives ⟨v,v⟩=0 ⇔ v=0. This is separation: positive definiteness gives separation (MKO).



S03 · equivalentBefore

\langle cv,cv\rangle

After

c^2\langle v,v\rangle

Conditions: none

Rule: ip_axioms · Uses: G1, ip_axioms

Leaf basis: ip_axioms + mul_assoc + power_laws

Linearity in the first argument: ⟨cv,cv⟩=c⟨v,cv⟩; linearity in the second: c⟨v,cv⟩=c·c⟨v,v⟩=c²⟨v,v⟩.



S04 · equivalentBefore

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

After

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

Conditions: \langle v,v\rangle\ge0

Rule: L_sqrt_scale · Uses: S03, S01

Leaf basis: sqrt_def + abs_rules + power_laws

By Lemma L_sqrt_scale (proved in S04.1, with s=⟨v,v⟩), √(c²⟨v,v⟩)=|c|√⟨v,v⟩=|c|N(v). This is absolute homogeneity: the factor is |c|, not c; for example N(−3x)=3N(x).



S05 · equivalentBefore

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

After

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

Conditions: none

Rule: ip_axioms · Uses: G1, ip_axioms

Leaf basis: ip_axioms + add_comm + distributive

Bilinearity expands into four terms, ⟨x,x⟩±⟨x,y⟩±⟨y,x⟩+⟨y,y⟩; symmetry ⟨y,x⟩=⟨x,y⟩ then merges the two cross terms into ±2⟨x,y⟩.



S06 · impliesBefore

x,y\in V

After

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

Conditions: none

Rule: L_cs · Uses: G1

Leaf basis: case_analysis + ip_axioms + order_basics

By Lemma L_cs (Cauchy–Schwarz, fully proved in S06.1 to S06.3), it holds for all x and y. The proof splits into the cases y=0 and y≠0, which cover every possibility. This is a universal proof, not obtained by checking finitely many vectors (MKO assumption a2).



S07 · impliesBefore

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

After

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

Conditions: none

Rule: L_sq_order · Uses: S06, S01

Leaf basis: abs_rules + sqrt_def + power_laws

Let u=|⟨x,y⟩|≥0 and w=N(x)N(y)≥0. Then u²=⟨x,y⟩² (|a|²=a²) and w²=N(x)²N(y)²=⟨x,x⟩⟨y,y⟩ ((√s)²=s). By S06, u²≤w², and Lemma L_sq_order (proved in S07.1) gives u≤w.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: order_basics · Uses: S05, S07, S01

Leaf basis: order_basics + abs_rules + distributive + sqrt_def

By S05, N(x+y)²=N(x)²+2⟨x,y⟩+N(y)². Since ⟨x,y⟩≤|⟨x,y⟩|≤N(x)N(y) (S07), adding the same quantity to both sides keeps the inequality: N(x+y)²≤N(x)²+2N(x)N(y)+N(y)²=(N(x)+N(y))².



S09 · impliesBefore

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

After

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

Conditions: none

Rule: L_sq_order · Uses: S08, S01, S07

Leaf basis: order_basics + sqrt_def

N(x+y)≥0 and N(x)+N(y)≥0 (S01), so Lemma L_sq_order with u=N(x+y) and w=N(x)+N(y) turns S08 into the triangle inequality.



S10 · impliesBefore

\text{S01, S02, S04, S09}

After

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

Conditions: none

Rule: norm_def · Uses: S01, S02, S04, S09

Leaf basis: norm_def + and_intro_elim + forall_intro

Nonnegativity and separation (S01, S02), absolute homogeneity (S04) and the triangle inequality (S09) are proved for arbitrary vectors and scalars, so N is a norm on V. This is a universal proof that depends on no particular vectors.



S11 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: G2, square_nonneg

Leaf basis: distributive + square_nonneg + numeric_evaluation

Audit the premise of G2: expanding the right side gives v₁²+v₂²+v₁²+2v₁v₂+v₂²=2v₁²+2v₁v₂+2v₂² (N1 checks this as a polynomial identity). All three squares are nonnegative, so vᵀAv≥0; if it is 0, then v₁=0 and v₂=0, so v=0. A is symmetric and the matrix form is bilinear, so G2 really defines an inner product.



S12 · equivalentBefore

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

After

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

Conditions: none

Rule: matrix_product_def · Uses: G2, G3, S11

Leaf basis: matrix_product_def + numeric_evaluation + sqrt_def

Standard basis vectors pick out entries of A: ⟨x,x⟩=A₁₁=2, ⟨y,y⟩=A₂₂=2, ⟨x,y⟩=A₁₂=1. The squared norms are exact integers; the norms stay exact symbols N(x)=N(y)=√2 (MKO assumption a2). An instance of homogeneity: N(−3x)=√(9·2)=√18=3√2, equal to |−3|N(x) (N3).



S13 · equivalentBefore

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

After

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

Conditions: none

Rule: eq_replace · Uses: S05, S12

Leaf basis: eq_replace + numeric_evaluation

Substitute into S05: ⟨x−y,x−y⟩=2−2·1+2=2 (N4), so the distance is N(x−y)=√2; ⟨x+y,x+y⟩=2+2·1+2=6 (N5), so N(x+y)=√6. Direct check with x−y=(1,−1): 2·1·1+1·(−1)+(−1)·1+2·(−1)·(−1)=2 (N6), agreeing with the expansion. The cross term −2 cannot be dropped: the Pythagorean 2+2=4 is wrong.



S14 · impliesBefore

\text{values of S12, S13}

After

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

Conditions: none

Rule: numeric_evaluation · Uses: S05, S06, S09, S12, S13

Leaf basis: numeric_evaluation + sqrt_def

Instance checks: Cauchy–Schwarz 1²=1≤2·2=4 (N7); the squared triangle inequality N(x+y)²=6≤(√2+√2)²=2+2·2+2=8 (N8, using √2·√2=2); the parallelogram identity: adding the two formulas of S05 gives the general identity ⟨x+y,x+y⟩+⟨x−y,x−y⟩=2⟨x,x⟩+2⟨y,y⟩, here 6+2=8=2(2+2) (N9). These only check that this instance agrees with S06, S09 and the general identity; they are not proofs of them.



S15 · impliesBefore

\text{S10 to S14}

After

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

Conditions: none

Rule: mko_ip_norm_def · Uses: S10, S11, S12, S13, S14

Leaf basis: and_intro_elim + mko_ip_norm_def

N is a norm on every real inner-product space (S10); in the example of G2 the exact values are N(x)=N(y)=√2, distance N(x−y)=√2 and N(x+y)=√6, and the instance checks agree with the general results (S14). This guide does not infer completeness, or a Hilbert space, from the norm coming from an inner product.







## Substeps and lemmas

S04.1 · equivalentBefore

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

After

|c|\sqrt{s}

Conditions: s\ge0

Rule: sqrt_def · Uses: sqrt_def, abs_rules

Leaf basis: sqrt_def + abs_rules + power_laws + order_basics

b=|c|√s satisfies b≥0 (a product of two nonnegative numbers) and b²=|c|²(√s)²=c²s (since |c|²=c² and (√s)²=s). The principal square root is the unique number with b≥0 and b²=c²s, so √(c²s)=|c|√s. S04.1 proves Lemma L_sqrt_scale.



S06.1 · impliesBefore

y=0

After

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

Conditions: none

Rule: ip_axioms · Uses: G1, ip_axioms

Leaf basis: ip_axioms + mul_zero

Case y=0: linearity in the second argument gives ⟨x,0⟩=⟨x,0·0⟩=0·⟨x,0⟩=0, and likewise ⟨0,0⟩=0. Both sides are 0, so the inequality holds.



S06.2 · impliesBefore

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

After

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

Conditions: y\neq0

Rule: ip_axioms · Uses: G1, S05, ip_axioms

Leaf basis: ip_axioms + distributive + forall_intro

Case y≠0: for every real t, positive definiteness gives ⟨x−ty,x−ty⟩≥0. Expanding as in S05 (with S03 handling the factor t): ⟨x−ty,x−ty⟩=⟨x,x⟩−2t⟨x,y⟩+t²⟨y,y⟩.



S06.3 · impliesBefore

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

After

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

Conditions: \langle y,y\rangle>0

Rule: forall_elim · Uses: S06.2, G1

Leaf basis: forall_elim + frac_rules + order_basics + mul_inverse_nonzero

For y≠0, ⟨y,y⟩>0, so t=⟨x,y⟩/⟨y,y⟩ may be chosen. Write a=⟨x,x⟩, b=⟨x,y⟩, c=⟨y,y⟩ and substitute into S06.2: 0≤a−2b²/c+b²/c=a−b²/c. Multiplying by c>0 (which keeps the direction) gives 0≤ac−b², that is b²≤ac. The algebraic identity c²(a−2(b/c)b+(b/c)²c)=c(ac−b²) is checked by N2. S06.1 to S06.3 together (the two cases cover every y) prove Lemma L_cs.



S07.1 · impliesBefore

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

After

u\le w

Conditions: u\ge0; w\ge0

Rule: contrapositive · Uses: order_basics

Leaf basis: order_basics + contrapositive

Prove the contrapositive: suppose u>w≥0. Then u>0, and multiplying u>w by u>0 gives u²>wu; also u>w with w≥0 gives wu≥w² (both sides are 0 when w=0, and multiply by w when w>0). So u²>w². Hence u²≤w² implies u≤w. S07.1 proves Lemma L_sq_order.







## 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 proofThe 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 spaceThe 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 valueThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-inner-product-induced-norm-01.json)