Metric space: auditing a finite distance table cell by cell and triple by triple

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 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.
• 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

d:X\times X\to\mathbb{R}

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)

d(i,j),\ i,j\in X

d(i,j)\in\{0,1,2\},\ d(i,j)\ge 0

d(i,i),\ i\in X

x=y\Rightarrow d(x,y)=0

d(i,j),\ i\neq j

d(x,y)=0\Rightarrow x=y

x=y\Rightarrow d(x,y)=0,\ d(x,y)=0\Rightarrow x=y

d(x,y)=0\Leftrightarrow x=y

d(i,j)\ \text{vs}\ d(j,i)

\forall i,j\in X:\ d(i,j)=d(j,i)

(i,j,k)\in X^3

i=k\ \lor\ (i\neq k\land(j=i\lor j=k))\ \lor\ i,j,k\ \text{pairwise distinct}

\text{cases A, B, C}

\forall i,j,k\in X:\ d(i,k)\le d(i,j)+d(j,k)

\text{nonnegativity, separation, symmetry, triangle inequality}

(X,d)\ \text{is a metric space}

e\ \text{on } Y=\{0,1,2\}

e\ge 0,\ e(x,y)=0\Leftrightarrow x=y,\ e(x,y)=e(y,x)

e(0,2)\ \text{vs}\ e(0,1)+e(1,2)

3>1+1=2

\exists(i,j,k):\ e(i,k)>e(i,j)+e(j,k)

(Y,e)\ \text{is not a metric space}

f(0,1)=0,\ 0\neq 1

(Z,f)\ \text{is not a metric space}

Substeps and lemmas

i=k

d(i,k)=0\le d(i,j)+d(j,i)

i\neq k,\ j\in\{i,k\}

d(i,j)+d(j,k)=d(i,k)

i,j,k\ \text{pairwise distinct}

d(i,k)\le 2\le d(i,j)+d(j,k)

|A|+|B|+|C|

16+24+24=64=4^3

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 enough

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

A 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 triple

In 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 i<j<k, can miss a counterexample (see negative control 4). This guide covers all 64 triples with the case argument of S07 and cross-checks by enumeration in N1; both are valid for the finite model X only.

• e is nonnegative, symmetric, zero on the diagonal and nonzero off it, so e is a metric → reject — The triangle inequality fails at (0,1,2): 3>1+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 i<j<k, namely (0,1,2), suffices for the triangle inequality → reject — Let h(0,1)=1, h(0,2)=1, h(1,2)=3 (symmetric, zero diagonal): (0,1,2) gives 1≤1+3 and passes, but (1,0,2) gives h(1,2)=3>h(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)