# Metric space: auditing a finite distance table cell by cell and triple by triple [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-metric-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-metric-space-01 · production-20261019-adopted-96 ## Goal and scope Three complete integer distance tables are given. (A) On X={0,1,2,3}, table d (step distance on a 4-cycle): check nonnegativity, zero diagonal, nonzero off-diagonal entries and symmetry cell by cell, and the triangle inequality by a case argument covering all 4³=64 triples, concluding that (X,d) is a metric space. (B) Table e on Y={0,1,2} passes the first four checks but violates the triangle inequality at (0,1,2). (C) Table f on Z={0,1,2} is nonnegative, symmetric and zero on the diagonal, yet has an off-diagonal zero and violates separation. Treats only finite carriers labeled 0 to n−1 with complete integer distance tables (MKO assumption a1); the conclusions concern only these three specified models and are not extended to arbitrary or infinite metric spaces (MKO assumption a2). Open balls, convergence and completeness are not treated; the canonical MKO and its English edition are not changed. ## Givens and symbols - order_basics - case_analysis - contrapositive - numeric_evaluation - G1 — Candidate A: X={0,1,2,3}; row i of table d lists d(i,0), d(i,1), d(i,2), d(i,3) in order: row 0 is 0,1,2,1; row 1 is 1,0,1,2; row 2 is 2,1,0,1; row 3 is 1,2,1,0. - G2 — Candidate B: Y={0,1,2}; the three rows of table e are 0,1,3; 1,0,1; 3,1,0. - G3 — Candidate C: Z={0,1,2}; the three rows of table f are 0,0,2; 0,0,2; 2,2,0. - X=\{0,1,2,3\} — the carrier of candidate A - d(i,j) — the distance in row i, column j of table d - e,\ f — the distance tables of candidates B and C - (i,j,k) — an ordered triple checked in the triangle inequality ## Rules and sources - order_basics · prerequisite — Order of the reals: exactly one of uv holds; u0 give uwvw. - 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. - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - 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). - iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold. - add_zero · prerequisite — Additive identity: u+0=u. - 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. - finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - mko_metric_def · cited — A metric d:X×X→R on a set X satisfies nonnegativity and separation, symmetry and the triangle inequality. A complete finite distance table permits cell-by-cell and triple-by-triple auditing of a specified candidate. · mko-metric-space - finite_exhaustion · prerequisite — On a finite set, a statement about all elements (or all ordered pairs or triples) holds exactly when it holds in each of the finitely many listed cases; checking every case is a complete proof for that finite model, but says nothing about other sets. ## Main derivation S01 · definitionBefore d:X\times X\to\mathbb{R} After d\ge 0;\ 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: metric_def · Uses: mko_metric_def Leaf basis: metric_def + mko_metric_def By the MKO a metric must satisfy four conditions, each for all points (or pairs, or triples): nonnegativity; separation (distance zero exactly when the points coincide); symmetry; the triangle inequality. Separation has two directions: a zero diagonal and nonzero off-diagonal entries. S02 · impliesBefore d(i,j),\ i,j\in X After d(i,j)\in\{0,1,2\},\ d(i,j)\ge 0 Conditions: none Rule: finite_exhaustion · Uses: G1 Leaf basis: finite_exhaustion + order_basics Inspect all 16 values: each is 0, 1 or 2, so all are nonnegative. Also note a bound used later: every value is at most 2. S03 · impliesBefore d(i,i),\ i\in X After x=y\Rightarrow d(x,y)=0 Conditions: none Rule: finite_exhaustion · Uses: G1 Leaf basis: finite_exhaustion The diagonal entries d(0,0), d(1,1), d(2,2), d(3,3) are all 0, so a point has distance zero from itself. This is one direction of separation. S04 · impliesBefore d(i,j),\ i\neq j After d(x,y)=0\Rightarrow x=y Conditions: none Rule: contrapositive · Uses: G1, S02 Leaf basis: finite_exhaustion + contrapositive The 12 off-diagonal cells are all 1 or 2, so for x≠y we have d(x,y)≥1, in particular d(x,y)≠0. By contraposition this is equivalent to 'd(x,y)=0 implies x=y'. S05 · impliesBefore x=y\Rightarrow d(x,y)=0,\ d(x,y)=0\Rightarrow x=y After d(x,y)=0\Leftrightarrow x=y Conditions: none Rule: iff_intro · Uses: S03, S04 Leaf basis: iff_intro S03 and S04 together give both directions, which is separation. This is the MKO's first paragraph: the diagonal must be zero and off-diagonal entries must not be zero, and together they make up separation. S06 · impliesBefore d(i,j)\ \text{vs}\ d(j,i) After \forall i,j\in X:\ d(i,j)=d(j,i) Conditions: none Rule: finite_exhaustion · Uses: G1 Leaf basis: finite_exhaustion Compare the 6 mirror pairs: d(0,1)=d(1,0)=1, d(0,2)=d(2,0)=2, d(0,3)=d(3,0)=1, d(1,2)=d(2,1)=1, d(1,3)=d(3,1)=2, d(2,3)=d(3,2)=1; the diagonal is trivially symmetric. The table equals its transpose. S07 · case_splitBefore (i,j,k)\in X^3 After i=k\ \lor\ (i\neq k\land(j=i\lor j=k))\ \lor\ i,j,k\ \text{pairwise distinct} Conditions: none Rule: case_analysis · Uses: S02, S03, S04 Leaf basis: case_analysis The triangle inequality d(i,k)≤d(i,j)+d(j,k) must hold for all 64 ordered triples. Split the triples into three cases: A: i=k; B: i≠k and j equals i or k; C: i, j, k pairwise distinct. Sub-steps S07.1 to S07.3 treat each case, and S07.4 confirms that the three cases cover exactly the 64 triples. S08 · impliesBefore \text{cases A, B, C} After \forall i,j,k\in X:\ d(i,k)\le d(i,j)+d(j,k) Conditions: none Rule: case_analysis · Uses: S07, S07.1, S07.2, S07.3, S07.4 Leaf basis: case_analysis + finite_exhaustion The inequality is proved in all three cases, which cover all 64 triples, so by proof by cases the triangle inequality holds for every ordered triple of X. N1 additionally enumerates all 64 triples with the formula d(i,j)=min(|i−j|, 4−|i−j|) as a cross-check. S09 · impliesBefore \text{nonnegativity, separation, symmetry, triangle inequality} After (X,d)\ \text{is a metric space} Conditions: none Rule: mko_metric_def · Uses: S02, S05, S06, S08 Leaf basis: mko_metric_def + and_intro_elim The four conditions come from S02, S05, S06 and S08, so (X,d) is a metric space. The conclusion concerns this specified finite model only. S10 · impliesBefore e\ \text{on } Y=\{0,1,2\} After e\ge 0,\ e(x,y)=0\Leftrightarrow x=y,\ e(x,y)=e(y,x) Conditions: none Rule: finite_exhaustion · Uses: G2 Leaf basis: finite_exhaustion Inspect candidate B cell by cell: all 9 values are nonnegative; the three diagonal cells are 0; the six off-diagonal cells are 1, 3, 1, 1, 3, 1, none of them 0; e(0,1)=e(1,0)=1, e(0,2)=e(2,0)=3, e(1,2)=e(2,1)=1, so the table is symmetric. The first three conditions all pass. S11 · impliesBefore e(0,2)\ \text{vs}\ e(0,1)+e(1,2) After 3>1+1=2 Conditions: none Rule: order_basics · Uses: G2 Leaf basis: order_basics + numeric_evaluation Take the triple (0,1,2): e(0,2)=3 while e(0,1)+e(1,2)=1+1=2. Since 3>2, the triangle inequality fails at this triple: going through point 1 is shorter than the direct distance. S12 · impliesBefore \exists(i,j,k):\ e(i,k)>e(i,j)+e(j,k) After (Y,e)\ \text{is not a metric space} Conditions: none Rule: quantifier_negation · Uses: S10, S11 Leaf basis: quantifier_negation + mko_metric_def The triangle inequality is a universal statement; S11 gives a counterexample, so by quantifier negation it is false and (Y,e) is not a metric space, although nonnegativity, separation and symmetry in S10 all pass. S13 · impliesBefore f(0,1)=0,\ 0\neq 1 After (Z,f)\ \text{is not a metric space} Conditions: none Rule: mko_metric_def · Uses: G3 Leaf basis: mko_metric_def + metric_def + quantifier_negation Candidate C has all 9 values nonnegative, a symmetric table and a zero diagonal; but f(0,1)=0 although 0≠1, violating 'd(x,y)=0 implies x=y'. Separation fails, so f is not a metric (such a table is usually called a pseudometric). Checking only nonnegativity, symmetry and the diagonal would miss this. ## Substeps and lemmas S07.1 · impliesBefore i=k After d(i,k)=0\le d(i,j)+d(j,i) Conditions: i=k Rule: order_basics · Uses: S07, S02, S03 Leaf basis: order_basics + add_zero Case A: i=k, so the left side is d(i,i)=0 (S03); the right side is a sum of two nonnegative numbers (S02), hence ≥0. Since 0≤right side, the inequality holds. S07.2 · impliesBefore i\neq k,\ j\in\{i,k\} After d(i,j)+d(j,k)=d(i,k) Conditions: i\neq k Rule: eq_replace · Uses: S07, S03 Leaf basis: eq_replace + add_zero + order_basics Case B: if j=i the right side is d(i,i)+d(i,k)=0+d(i,k)=d(i,k); if j=k it is d(i,k)+d(k,k)=d(i,k)+0=d(i,k). In both sub-cases the right side equals the left, so d(i,k)≤right side holds with equality. S07.3 · impliesBefore i,j,k\ \text{pairwise distinct} After d(i,k)\le 2\le d(i,j)+d(j,k) Conditions: i\neq j,\ j\neq k,\ i\neq k Rule: order_basics · Uses: S07, S02, S04 Leaf basis: order_basics + numeric_evaluation Case C: since i≠j and j≠k, S04 gives d(i,j)≥1 and d(j,k)≥1, so the right side is at least 1+1=2; by S02 every distance is at most 2, so d(i,k)≤2. By transitivity of order, d(i,k)≤right side. S07.4 · impliesBefore |A|+|B|+|C| After 16+24+24=64=4^3 Conditions: none Rule: finite_counting_basics · Uses: S07 Leaf basis: finite_counting_basics + numeric_evaluation The three cases are exclusive and exhaustive: if i=k the triple is in A; otherwise i≠k, and it is in B if j equals i or k, and in C if j differs from both. Counting: A has 4·4=16 triples (choose i and j); B has 2·(4·3)=24 (choose distinct i, k, then let j equal one of them); C has 4·3·2=24. The total 64=4³ is exactly the number of ordered triples. ## Reverse audits - S13 · sufficient_goal_reduction · G3, mko_metric_def, metric_def — Goal G: f is not a metric. Sufficient condition H: one off-diagonal zero (H⇒G by the definition of separation). H is read directly from the table in G3; G is never used as a premise. - S12 · sufficient_goal_reduction · S11, quantifier_negation, mko_metric_def — Goal G: e is not a metric. Sufficient condition H: some triple violates the triangle inequality; H⇒G by the definition. H is computed directly in S11; G is never used as a premise. - S11 · premise_audit · G2, order_basics, numeric_evaluation — One counterexample suffices to refute the universal statement over all triples. - S10 · premise_audit · G2, finite_exhaustion — These are cell-by-cell checks involving no triples, so they guarantee nothing about the triangle inequality. - S09 · sufficient_goal_reduction · S02, S05, S06, S08, mko_metric_def — Goal G: (X,d) is a metric space. Sufficient condition H: the four conditions hold together; H⇒G by the definition. H is proved forwards from table d; G is never used as a premise. - S08 · premise_audit · S07.1, S07.2, S07.3, S07.4, case_analysis — Proof by cases needs a proof in every case and exhaustive cases; S07.1 to S07.3 and S07.4 supply these. - S07.4 · premise_audit · finite_counting_basics, numeric_evaluation — Exclusivity follows from the definitions of the cases, and the matching total confirms that no triple is missed (N6, N7). - S07.3 · premise_audit · S02, S04, order_basics — The argument depends on a feature of table d: twice the smallest off-diagonal value, 1, is at least the largest value, 2. This fails for candidate B (largest value 3 exceeds 1+1), so it cannot be transferred. - S07.2 · premise_audit · S03, eq_replace, add_zero — Only the zero diagonal and the additive identity are used; since i≠k, j cannot equal both i and k, so the two sub-cases are exclusive. - S07.1 · premise_audit · S02, S03, order_basics — It needs the zero diagonal and nonnegativity; no particular j has to be inspected. - S07 · premise_audit · case_analysis, S02, S03, S04 — Proof by cases needs the cases to cover every possibility, which S07.4 checks by counting. Each case uses only table properties already established in S02 to S04. - S06 · premise_audit · G1, finite_exhaustion — All 6 off-diagonal pairs are compared, and with the 4 diagonal cells all 16 ordered pairs are covered. - S05 · premise_audit · S03, S04, iff_intro — A biconditional needs both directions, supplied by S03 and S04 respectively. - S04 · premise_audit · G1, finite_exhaustion, contrapositive — All 12 off-diagonal cells must be inspected; a single zero there would break separation (see candidate C). The step also records d(x,y)≥1 for x≠y, used in S07.3. - S03 · premise_audit · G1, finite_exhaustion — Only the four diagonal cells are inspected; the converse (zero distance forces the same point) does not follow and is left to S04. - S02 · premise_audit · G1, finite_exhaustion — Nonnegativity is established only after all 16 cells are inspected; this step says nothing about separation or the triangle inequality. - S01 · premise_audit · mko_metric_def, metric_def — This step only lists the conditions to check and derives no new fact; none of the four may be skipped. ## Error controls and negative controls Nonnegativity and symmetry are not enoughThe MKO names the mistake of calling a table a metric after checking only nonnegativity and symmetry. Candidate B passes nonnegativity and symmetry (even separation) yet violates the triangle inequality; candidate C passes nonnegativity and symmetry yet violates separation. All four conditions must be checked. Separation includes nonzero off-diagonal entriesA zero diagonal is only half of separation (S03). The MKO warns against overlooking off-diagonal zeros: in candidate C, f(0,1)=0 gives two distinct points distance zero. S04 must inspect every off-diagonal cell. The triangle inequality must cover every ordered tripleIn candidate B every triple with a repeated point passes (for the reasons in S07.1 and S07.2); failure appears only at the distinct triples (0,1,2) and (2,1,0). Sampling, or checking only triples with i1+1. - f has nonnegative values, a symmetric table and a zero diagonal, so f is a metric → reject — f(0,1)=0 although 0≠1, so separation fails. - Since all 64 triples of (X,d) pass, every distance table of this kind on any set satisfies the triangle inequality → reject — A finite enumeration proves only the specified model (MKO assumption a2); candidate B is a failing example. - On a three-point carrier, checking the triple with ih(1,0)+h(0,2)=2. ## Result and limitations (X,d) is a metric space: all 16 cells are nonnegative, the diagonal is zero and off-diagonal entries are 1 or 2 (separation), the table is symmetric, and the triangle inequality holds for all 64 triples (proved in three cases). (Y,e) passes nonnegativity, separation and symmetry, but e(0,2)=3>e(0,1)+e(1,2)=2, so it is not a metric. (Z,f) is nonnegative, symmetric and zero on the diagonal, but f(0,1)=0 with 0≠1, so separation fails and it is not a metric. All three conclusions concern only the specified finite models. - N1 uses the formula d(i,j)=min(|i−j|, 4−|i−j|), which reproduces table d (N2 to N4 spot-check three cells; the others can be compared one by one in the same way), and enumerates all 64 triples; it is a complete cross-check for this finite model, and the argument of S07 does not depend on it. - Open balls, metric convergence, Cauchy sequences and completeness (the MKO's formal next) are not treated, and nothing is extended to infinite metric spaces. ## Verification and source binding 10 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 3927e5b8483787d913f92ff4449074b352dd7013da2ee9eaafcf52ea099490b7 - original source SHA-256: 3927e5b8483787d913f92ff4449074b352dd7013da2ee9eaafcf52ea099490b7 - 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-metric-space-01.json)