# Norm-induced metric: proving from the norm axioms that d(x,y)=‖x−y‖ is a metric, with exact l1 and l∞ computations in ℝ³

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

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



## Goal and scope

Let (V,‖·‖) be a real normed vector space. Prove that d(x,y)=‖x−y‖ is nonnegative, separates points, is symmetric and satisfies the triangle inequality; prove that the l1 and l∞ formulas on ℝⁿ are norms, so both induce metrics; then compute d1 and d∞ exactly in ℝ³ for x=(1,−2,3), y=(4,0,−1), z=(2,5,1).

Stays inside the MKO: a certified real normed vector space, and the named l1 and l∞ norms on ℝⁿ; in the general theorem both points need only lie in the same real normed space and use its norm, with no finite-dimensional hypothesis. The finite-coordinate and named-norm requirements apply only to the later ℝⁿ examples (assumption a1). The metric property is proved from the universal formula and the norm axioms; distances between finitely many points are examples only (assumption a2). Completeness and Banach spaces are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- vector_space_axioms
- abs_rules
- order_basics
- metric_def
- finite_sum_rules


- G1 — (V,‖·‖) is a real normed vector space: (N1) ‖v‖≥0 and ‖v‖=0 ⇔ v=0; (N2) ‖tv‖=|t|‖v‖; (N3) ‖u+v‖≤‖u‖+‖v‖, for all u, v∈V and t∈ℝ.
- G2 — For x, y∈V define d(x,y)=‖x−y‖.
- G3 — For a positive integer n, on ℝⁿ: ‖v‖₁=Σ_{i=1}^{n}|v_i| and ‖v‖∞=max_{1≤i≤n}|v_i|. Example in ℝ³: x=(1,−2,3), y=(4,0,−1), z=(2,5,1).


- \|v\| — norm of the vector v
- d(x,y) — induced distance ‖x−y‖
- \|v\|_1 — l1 norm Σ|v_i|
- \|v\|_\infty — l∞ norm max|v_i|
- d_1,\ d_\infty — metrics induced by l1 and l∞
- x,\ y,\ z — three integer-coordinate points of ℝ³





## Rules and sources


- 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.
- 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.
- metric_def · prerequisite — Metric: d:X×X→ℝ with d(x,y)≥0 and d(x,y)=0 ⇔ x=y; d(x,y)=d(y,x); triangle inequality d(x,z)≤d(x,y)+d(y,z).
- 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.
- 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.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- mul_one · prerequisite — Multiplicative identity: 1·u=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.
- 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.
- mko_nim_def · cited — If (V,norm) is a certified real normed vector space, d(x,y)=norm(x−y) is nonnegative, separates points, is symmetric and satisfies the triangle inequality. This slice uses exact coordinate calculations only for the named l1 and linfinity norms on R^n. · mko-norm-induced-metric
- mko_norm_def · cited — A norm sends vectors to nonnegative real numbers, with norm(v)=0 iff v=0, norm(a v)=|a| norm(v), and norm(u+v)≤norm(u)+norm(v). This slice uses only the named l1 and linfinity formulas on R^n. · mko-real-normed-vector-space
- max_rules · prerequisite — Maximum of finitely many reals: max_i w_i equals some w_k, and w_i≤max_i w_i for every i; if every w_i≤M then max_i w_i≤M.
- L_l1_norm · lemma — On ℝⁿ, ‖v‖₁=Σ|v_i| satisfies N1, N2 and N3.
- L_linf_norm · lemma — On ℝⁿ, ‖v‖∞=max|v_i| satisfies N1, N2 and N3.





## Main derivation

S01 · definitionBefore

d(x,y)=\|x-y\|

After

d\ge0,\ d(x,y)=0\Leftrightarrow x=y,\ d(x,y)=d(y,x),\ d(x,z)\le d(x,y)+d(y,z)

Conditions: none

Rule: mko_nim_def · Uses: G1, G2, metric_def

Leaf basis: mko_nim_def + metric_def + def_unfold

By the MKO and the definition of a metric, four properties must be proved, each for all x, y, z∈V: nonnegativity, separation, symmetry and the triangle inequality. The proof uses only the three norm axioms of G1, no particular points.



S02 · impliesBefore

x,y\in V

After

x-y=x+(-1)y\in V,\ d:V\times V\to\mathbb{R}

Conditions: none

Rule: vector_space_axioms · Uses: G1, G2, vector_space_axioms

Leaf basis: vector_space_axioms + function_def

A vector space is closed under addition and scalar multiplication, so x−y=x+(−1)y lies in V and ‖x−y‖ is a real number. d is a function V×V→ℝ. This needs x and y in the same space (assumption a1).



S03 · impliesBefore

d(x,y)=\|x-y\|

After

d(x,y)\ge 0

Conditions: none

Rule: mko_norm_def · Uses: S02, G1

Leaf basis: mko_norm_def

N1 applied to the vector v=x−y gives ‖x−y‖≥0, so d(x,y)≥0.



S04 · equivalentBefore

d(x,y)=0

After

x=y

Conditions: none

Rule: mko_norm_def · Uses: S02, G1

Leaf basis: mko_norm_def + vector_space_axioms

d(x,y)=0 ⇔ ‖x−y‖=0 ⇔ x−y=0 (second half of N1) ⇔ x=y (S04.1). This is separation: the distance is zero exactly when the points coincide.



S05 · equivalentBefore

d(x,y)=\|x-y\|

After

d(x,y)=\|y-x\|=d(y,x)

Conditions: none

Rule: mko_norm_def · Uses: S02, G1

Leaf basis: mko_norm_def + vector_space_axioms + abs_rules

Symmetry comes from two sub-steps: S05.1 writes x−y as (−1)(y−x), and S05.2 uses N2 with t=−1 to get ‖(−1)(y−x)‖=‖y−x‖.



S06 · impliesBefore

d(x,z)=\|x-z\|

After

d(x,z)\le d(x,y)+d(y,z)

Conditions: none

Rule: mko_norm_def · Uses: S02, G1

Leaf basis: mko_norm_def + vector_space_axioms

The triangle inequality comes from two sub-steps: S06.1 splits x−z as (x−y)+(y−z), and S06.2 applies N3 to this sum.



S07 · impliesBefore

\text{nonnegativity, separation, symmetry, triangle}

After

d(x,y)=\|x-y\|\ \text{is a metric on}\ V

Conditions: none

Rule: metric_def · Uses: S03, S04, S05, S06, metric_def

Leaf basis: metric_def + forall_intro + and_intro_elim

All four properties are proved for arbitrary x, y, z with no extra assumption on them, so by generalization and the definition of a metric, d is a metric on V. This is a universal proof using no finite sample.



S08 · theorem_applicationBefore

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

After

\|\cdot\|_1\ \text{satisfies N1, N2, N3}

Conditions: none

Rule: L_l1_norm · Uses: G3

Leaf basis: L_l1_norm

Lemma L_l1_norm (proved in S08.1 to S08.3): the l1 formula applies the properties of absolute value to each coordinate and adds over the finite sum, giving the three norm axioms. This is an algebraic certificate for all vectors (the qualification of the named norm in the MKO).



S09 · theorem_applicationBefore

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

After

\|\cdot\|_\infty\ \text{satisfies N1, N2, N3}

Conditions: none

Rule: L_linf_norm · Uses: G3

Leaf basis: L_linf_norm

Lemma L_linf_norm (proved in S09.1 to S09.3): the l∞ formula satisfies the norm axioms by the properties of a finite maximum.



S10 · theorem_applicationBefore

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

After

d_1(x,y)=\|x-y\|_1,\ d_\infty(x,y)=\|x-y\|_\infty\ \text{are metrics}

Conditions: none

Rule: mko_nim_def · Uses: S07, S08, S09

Leaf basis: mko_nim_def + L_l1_norm + L_linf_norm

S08 and S09 confirm that both are norms on ℝⁿ, so (ℝⁿ,‖·‖₁) and (ℝⁿ,‖·‖∞) are normed spaces, and the general theorem S07 gives the two metrics d1 and d∞.



S11 · impliesBefore

x-y=(1-4,\,-2-0,\,3-(-1))=(-3,-2,4)

After

d_1(x,y)=3+2+4=9,\ d_\infty(x,y)=\max(3,2,4)=4

Conditions: none

Rule: numeric_evaluation · Uses: S10, G3

Leaf basis: numeric_evaluation + abs_rules

Subtract coordinatewise: x−y=(−3,−2,4), with absolute values 3, 2, 4. l1 takes the sum, 9, and l∞ the maximum, 4.



S12 · impliesBefore

y-x=(3,2,-4)

After

d_1(y,x)=9=d_1(x,y)

Conditions: none

Rule: numeric_evaluation · Uses: S05, S11, G3

Leaf basis: numeric_evaluation + abs_rules

y−x=(3,2,−4) also has absolute values 3, 2, 4, so d1(y,x)=9, consistent with the general symmetry of S05. This is one example, not a proof of symmetry.



S13 · impliesBefore

x-z=(-1,-7,2),\ y-z=(2,-5,-2)

After

d_1(x,z)=10,\ d_\infty(x,z)=7,\ d_1(y,z)=9,\ d_\infty(y,z)=5

Conditions: none

Rule: numeric_evaluation · Uses: S10, G3

Leaf basis: numeric_evaluation + abs_rules

x−z=(1−2,−2−5,3−1)=(−1,−7,2): l1 gives 1+7+2=10 and l∞ gives 7. y−z=(4−2,0−5,−1−1)=(2,−5,−2): l1 gives 2+5+2=9 and l∞ gives 5.



S14 · impliesBefore

d_1(x,z)=10,\ d_\infty(x,z)=7

After

10\le 9+9,\ 7\le 4+5

Conditions: none

Rule: order_basics · Uses: S06, S11, S13

Leaf basis: order_basics + numeric_evaluation

At these three points the triangle inequality reads 10≤18 for d1 and 7≤9 for d∞, both consistent with S06. This checks an example and cannot replace the universal proof of S06.



S15 · impliesBefore

d_1(x,y)=9,\ d_\infty(x,y)=4

After

d_1(x,y)\neq d_\infty(x,y)

Conditions: none

Rule: numeric_evaluation · Uses: S11

Leaf basis: numeric_evaluation

The same pair of points has different distances under the two named norms (9≠4), so each computation must identify its norm and keep both points in the same dimension (assumption a1). A mixed-norm bound needs an additional comparison estimate, not just the triangle inequality for one metric. Here ‖v‖∞≤‖v‖₁ gives d∞(x,z)≤d1(x,y)+d∞(y,z).







## Substeps and lemmas

S04.1 · equivalentBefore

x-y=0

After

x=y

Conditions: none

Rule: vector_space_axioms · Uses: vector_space_axioms

Leaf basis: vector_space_axioms + eq_congruence

Add y to both sides: (x−y)+y=x+((−y)+y)=x+0=x, and on the right 0+y=y, so x=y. Backward: if x=y then x−y=y−y=0.



S05.1 · equivalentBefore

x-y

After

(-1)(y-x)

Conditions: none

Rule: vector_space_axioms · Uses: vector_space_axioms

Leaf basis: vector_space_axioms + neg_mul

(−1)(y−x)=(−1)y+(−1)(−1)x=−y+x=x−y, using distributivity of a scalar over vector addition, (ab)u=a(bu) and commutativity of addition.



S05.2 · equivalentBefore

\|(-1)(y-x)\|

After

|-1|\,\|y-x\|=\|y-x\|

Conditions: t=-1

Rule: mko_norm_def · Uses: S05.1, G1

Leaf basis: mko_norm_def + abs_rules + mul_one

N2 with t=−1: ‖(−1)(y−x)‖=|−1|·‖y−x‖=‖y−x‖. This step really needs N2; a function satisfying only N1 and N3 need not give a symmetric distance (see the error controls).



S06.1 · equivalentBefore

x-z

After

(x-y)+(y-z)

Conditions: none

Rule: vector_space_axioms · Uses: vector_space_axioms

Leaf basis: vector_space_axioms

(x−y)+(y−z)=x+((−y)+y)+(−z)=x+0−z=x−z, using associativity, inverses and the zero vector.



S06.2 · impliesBefore

\|(x-y)+(y-z)\|

After

\le\|x-y\|+\|y-z\|

Conditions: none

Rule: mko_norm_def · Uses: S06.1, G1

Leaf basis: mko_norm_def

N3 with u=x−y and v=y−z: ‖u+v‖≤‖u‖+‖v‖. Combined with S06.1, d(x,z)≤d(x,y)+d(y,z).



S08.1 · impliesBefore

\sum_{i}|v_i|

After

\sum_i|v_i|\ge0,\ \sum_i|v_i|=0\Leftrightarrow v=0

Conditions: none

Rule: abs_rules · Uses: G3, abs_rules, order_basics

Leaf basis: abs_rules + order_basics + finite_sum_rules

Each |v_i|≥0, and a sum of nonnegative numbers is nonnegative. If the sum is 0, each term lies between 0 and the whole sum, so every |v_i|=0, that is every v_i=0 and v=0; conversely v=0 gives the sum 0. This is N1.



S08.2 · equivalentBefore

\sum_i|t\,v_i|

After

|t|\sum_i|v_i|

Conditions: none

Rule: abs_rules · Uses: G3, abs_rules, finite_sum_rules

Leaf basis: abs_rules + finite_sum_rules

|t v_i|=|t||v_i|, then the constant |t| comes out of the finite sum. This is N2.



S08.3 · impliesBefore

\sum_i|u_i+v_i|

After

\le\sum_i(|u_i|+|v_i|)=\sum_i|u_i|+\sum_i|v_i|

Conditions: none

Rule: abs_rules · Uses: G3, abs_rules, order_basics

Leaf basis: abs_rules + order_basics + finite_sum_rules

Each coordinate satisfies |u_i+v_i|≤|u_i|+|v_i| (the real triangle inequality). Adding the n inequalities (u<v gives u+w<v+w, used repeatedly, allowing equality) gives the inequality of sums, and the sum then splits. This is N3. S08.1 to S08.3 together prove Lemma L_l1_norm.



S09.1 · impliesBefore

\max_i|v_i|

After

\max_i|v_i|\ge0,\ \max_i|v_i|=0\Leftrightarrow v=0

Conditions: none

Rule: max_rules · Uses: G3, abs_rules, max_rules

Leaf basis: max_rules + abs_rules + order_basics

The maximum equals some |v_k|≥0. If the maximum is 0, every |v_i|≤0, and also |v_i|≥0, so every v_i=0; conversely v=0 gives maximum 0. This is N1.



S09.2 · equivalentBefore

\max_i|t\,v_i|

After

|t|\max_i|v_i|

Conditions: |t|\ge 0

Rule: max_rules · Uses: G3, abs_rules, max_rules

Leaf basis: max_rules + abs_rules + order_basics

|t v_i|=|t||v_i|. Let the maximum be attained at k: for every i, |v_i|≤|v_k|, and multiplying by the nonnegative |t| keeps the inequality, so |t||v_i|≤|t||v_k|; the maximum is |t||v_k|=|t|max|v_i|. This is N2.



S09.3 · impliesBefore

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

After

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

Conditions: none

Rule: max_rules · Uses: G3, abs_rules, max_rules

Leaf basis: abs_rules + max_rules + order_basics

For every i: |u_i+v_i|≤|u_i|+|v_i| (the real triangle inequality), with |u_i|≤‖u‖∞ and |v_i|≤‖v‖∞. So ‖u‖∞+‖v‖∞ is an upper bound of every |u_i+v_i|, and the maximum does not exceed it. This is N3. S09.1 to S09.3 together prove Lemma L_linf_norm.







## Reverse audits


- S15 · premise_audit · S11, numeric_evaluation — It only compares two exact numbers, showing that the metric depends on the chosen norm.
- S14 · premise_audit · S06, order_basics — A check at finitely many points supports only those points; the general conclusion comes from S06.
- S13 · premise_audit · G3, numeric_evaluation — Exact integer computation, recomputable (N4 to N7).
- S12 · premise_audit · S05, numeric_evaluation — The general conclusion comes from S05; this step is only an example.
- S11 · premise_audit · G3, numeric_evaluation — Exact integer computation, recomputable (N1, N2).
- S10 · premise_audit · S07, S08, S09 — S07 needs the norm axioms, which S08 and S09 supply; each metric is paired only with the norm that induces it.
- S09.3 · premise_audit · abs_rules, max_rules, order_basics — The upper-bound argument gives a one-way inequality; this sub-step does not use L_linf_norm.
- S09.2 · inverse_equivalence · max_rules, abs_rules, order_basics — Both sides are the same number; the condition is |t|≥0 (multiplying by a negative number would reverse inequalities). This sub-step does not use L_linf_norm.
- S09.1 · premise_audit · max_rules, abs_rules — It uses that the maximum is an upper bound and is attained; this sub-step does not use L_linf_norm.
- S09 · premise_audit · G3, L_linf_norm — It needs only the l∞ formula and the lemma; it holds for every vector.
- S08.3 · premise_audit · abs_rules, order_basics — Adding inequalities term by term preserves their direction, and no converse is claimed; this sub-step does not use L_l1_norm.
- S08.2 · inverse_equivalence · abs_rules, finite_sum_rules — Both equalities can be reversed; this sub-step does not use L_l1_norm.
- S08.1 · premise_audit · abs_rules, order_basics — The key is that a zero sum of nonnegative terms forces every term to be zero; this sub-step does not use L_l1_norm.
- S08 · premise_audit · G3, L_l1_norm — It needs only the l1 formula and the lemma; it holds for every n and every vector.
- S07 · sufficient_goal_reduction · S03, S04, S05, S06, metric_def, forall_intro — Goal G: d is a metric. Sufficient condition H: the four properties hold for all points; H⇒G by the definition of a metric. H is proved forwards in S03 to S06.
- S06.2 · premise_audit · mko_norm_def, S06.1 — N3 is a one-way inequality; equality does not hold in general and is not claimed.
- S06.1 · inverse_equivalence · vector_space_axioms — Two expressions for the same vector, so the step is two-way.
- S06 · premise_audit · mko_norm_def, vector_space_axioms — It needs the vector identity (sub-step S06.1) and N3 (sub-step S06.2); this is an inequality, and no converse is claimed.
- S05.2 · inverse_equivalence · mko_norm_def, abs_rules — N2 is an equation and |−1|=1, so both sides are the same number.
- S05.1 · inverse_equivalence · vector_space_axioms — Two expressions for the same vector, so the step is two-way.
- S05 · inverse_equivalence · mko_norm_def, vector_space_axioms, abs_rules — Both sides are the same real number (sub-steps S05.1 and S05.2 give this from the vector space axioms and N2); swapping x and y and repeating the argument goes back.
- S04.1 · inverse_equivalence · vector_space_axioms — Adding y and subtracting y undo each other; both directions come from the additive group axioms.
- S04 · inverse_equivalence · mko_norm_def, vector_space_axioms — The second half of N1 is itself an iff, and so is x−y=0⇔x=y, proved in sub-step S04.1, so the whole chain holds both ways.
- S03 · premise_audit · G1, mko_norm_def — It uses only the first half of N1 and holds for every x, y.
- S02 · premise_audit · vector_space_axioms, G2 — It only confirms that d is defined; if the two points were in different spaces, x−y would be meaningless.
- S01 · premise_audit · mko_nim_def, metric_def — This step only lists the obligations and derives no new fact.





## Error controls and negative controls

A finite sample does not establish the metric or its originThe common mistake named by the MKO is to claim, after checking finitely many distances, that a metric is induced by a norm. The 10≤18 and 7≤9 of S14 are only examples. Counterexample: the discrete metric on ℝ³ (distance 1 between distinct points) satisfies the metric axioms, but a norm-induced metric always has d(2v,0)=‖2v‖=2d(v,0), while the discrete metric gives 1≠2 for v≠0, so no norm induces it.

N1 and N3 alone do not ensure symmetryN1 and N3 alone are not enough. On ℝ, f(v)=max(v,−2v) is nonnegative, zero only at 0, and subadditive (a maximum of linear functions), but f(1)=1 and f(−1)=2, so f(x−y) is not symmetric: from 1 to 0 it is 1, from 0 to 1 it is 2. S05.2 obtains symmetry exactly through N2 with t=−1.

One named norm, one dimensiond1(x,y)=9 while d∞(x,y)=4 (S15). Mixing norms requires a comparison estimate in addition to the triangle inequality for one metric. In this example d∞(x,y)≤d1(x,y), so d∞(x,z)≤d∞(x,y)+d∞(y,z)≤d1(x,y)+d∞(y,z) does hold. When the two points have different dimensions, x−y is undefined in this model (S02).


- d(x,y)=‖x‖₁−‖y‖₁ is a metric on ℝ³ → reject — x=0 and y=(1,0,0) give 0−1=−1<0, violating nonnegativity.
- The discrete metric on ℝ³ is induced by some norm → reject — An induced metric satisfies d(2v,0)=2d(v,0), but the discrete metric gives 1≠2 for v≠0.
- The triangle inequality was checked at x, y, z (10≤18, 7≤9), so d1 and d∞ are metrics → reject — A finite sample supports only those points; the metric property comes from the universal proof in S06 to S10.
- The l1 distance between (1,−2,3)∈ℝ³ and (1,2)∈ℝ² is 4 → reject — The points are not in the same space, so x−y is undefined (assumption a1).





## Result and limitations

For every real normed vector space, d(x,y)=‖x−y‖ is nonnegative (N1), separates points (N1 with x−y=0⇔x=y), is symmetric (N2 with t=−1) and satisfies the triangle inequality (x−z=(x−y)+(y−z) and N3), so it is a metric. The l1 and l∞ formulas on ℝⁿ are norms, so d1 and d∞ are metrics. Example: d1(x,y)=9, d∞(x,y)=4, d1(x,z)=10, d∞(x,z)=7, d1(y,z)=9, d∞(y,z)=5.


- max_rules is a premise of this guide and is not derived here from the order axioms of the reals.
- The subadditivity of f(v)=max(v,−2v) in the error controls is explanatory (a standard property of a maximum of linear functions) and is not a numbered step.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 49854f1c5f3eec27f6de9fba35448a82d0db140a86fbabd4f87f370e0e39ac1a
- original source SHA-256: 6d24d167b92a2af8ec2a7ab0a267082c9664a86cde10e8728624bf97a61aff02
- 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-norm-induced-metric-01.json)