# A complete contraction certificate on a finite metric

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-contraction-mapping-theorem/)

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-contraction-mapping-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit completeness, a unique fixed point and the error bound for a constant self-map on a three-point discrete metric.

Only the complete finite model, not a replacement for the general Banach theorem.





## Givens and symbols


- algebra
- sets
- epsilon


- G1 — X={a,b,c}; d(x,x)=0 and d=1 on distinct points; T(a)=T(b)=T(c)=a, q=1/2, x_0=c.


- D — complete metric matrix
- T — total self-map
- q — strict contraction factor





## Rules and sources


- mko_definition · cited — The exact finite families qualify every metric axiom and a complete total self-map, then check d(Tx,Ty)≤q*d(x,y) for every ordered pair with fixed0≤q<1. From a declared start generate the entire requested Picard orbit and enumerate fixed points to check uniqueness. Compare d(x_n,x*) with q^n/(1−q)*d(x_1,x_0) exactly. A finite metric space is complete, but its certificate proves only that specified model. q=1, failure of the self-map premise, a noncomplete space or sampled-pair checks do not license the theorem. · mko-contraction-mapping-theorem
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- sets · prerequisite — Compute unions, intersections, complements, inclusion and preimages element by element.
- epsilon · prerequisite — Convergence requires for every positive epsilon an integer N controlling every n≥N by a strict error bound; use the Archimedean property of the reals.





## Main derivation

S01 · impliesBefore

D=\begin{pmatrix}0&1&1\\1&0&1\\1&1&0\end{pmatrix}

After

d\ge0,\quad d(x,y)=0\iff x=y,\quad d(x,y)=d(y,x)

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

The full nine-entry matrix directly verifies nonnegativity, separation and symmetry.



S02 · impliesBefore

x=z\text{ or }x\ne z

After

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

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

If x=z the left side is zero; otherwise the two right terms cannot both vanish, so their sum is at least one. This covers all 27 triples.



S03 · impliesBefore

(z_n)\text{ is }d\text{-Cauchy},\quad\varepsilon=1/2

After

\exists N\ \forall m,n\ge N:\ d(z_m,z_n)<1/2\Longrightarrow z_m=z_n

Conditions: none

Rule: epsilon · Uses: S01, S02

Leaf basis: epsilon

A Cauchy tail must be constant, hence eventually equals a point of X and converges; the space is complete.



S04 · impliesBefore

T(a)=T(b)=T(c)=a\in X

After

T:X\to X\text{ is a total self-map}

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

Every input is assigned and its image remains in the carrier.



S05 · impliesBefore

x,y\in X

After

d(Tx,Ty)=0\le\tfrac12d(x,y),\quad0\le q<1

Conditions: none

Rule: algebra · Uses: G1, S04

Leaf basis: algebra

Images agree for all nine ordered pairs, establishing the full contraction inequality.



S06 · impliesBefore

Tx=x

After

x=a\text{ is the only fixed point}

Conditions: none

Rule: sets · Uses: G1, S04

Leaf basis: sets

a maps to itself, while b,c map to the different point a; the exhaustive fixed-point list contains only a.



S07 · impliesBefore

x_{n+1}=Tx_n,\quad x_0=c

After

x_1=a,\quad x_n=a\ (n\ge1),\quad x_n\to a

Conditions: none

Rule: sets · Uses: G1, S04, S06

Leaf basis: sets

The first step reaches a, and T(a)=a inductively fixes the entire remaining orbit.



S08 · impliesBefore

\frac{q^n}{1-q}d(x_1,x_0)=2^{1-n}

After

d(x_0,a)=1\le2;\quad d(x_n,a)=0\le2^{1-n}\ (n\ge1)

Conditions: none

Rule: algebra · Uses: S06, S07

Leaf basis: algebra

Check the standard geometric error bound for all n, including zero, by explicit branches.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S06, S07 — The bound certifies this instance without claiming a general complete-space proof.
- S07 · premise_audit · G1, S04, S06 — Convergence is not claimed merely from a finite Picard trace.
- S06 · premise_audit · G1, S04 — Uniqueness follows from all-point auditing and also from d≤q*d with q<1.
- S05 · premise_audit · G1, S04 — q=1/2 is strictly below one, not merely nonexpansive q=1.
- S04 · premise_audit · G1 — A self-map, not a map into another space, is required.
- S03 · premise_audit · S01, S02 — The minimum positive distance controls every Cauchy sequence, not selected samples.
- S02 · premise_audit · G1, S01 — The triangle argument covers every triple, not numerical samples.
- S01 · premise_audit · G1 — Distances are supplied for every pair, not sampled pairs.





## Error controls and negative controls

Complete metricQualify every metric axiom and the total map before contraction.

Whole orbitInductively prove it stays fixed forever, separately from a finite trace.


- The identity with q=1 also has a unique fixed point. → reject — All three points are fixed; strict contraction fails.
- Checking only (a,b) proves contraction on every pair. → reject — One success cannot replace the all-pair quantifier.
- A map leaving X still qualifies for the self-map theorem. → reject — Iteration and the fixed-point obligation require the same X.





## Result and limitations

This finite metric is complete, T has unique fixed point a, and the orbit from c reaches it in one step with every error bound satisfied.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 9495e80b14cbe0e32e555d76b8ebed0ff8eb48f593477974ab06adb8325a82a6
- original source SHA-256: 9495e80b14cbe0e32e555d76b8ebed0ff8eb48f593477974ab06adb8325a82a6
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-contraction-mapping-theorem-01.json)