Six Birds Verified IV: Tolerance and Surrogates

Abstract

A coarse description often reads its data only approximately: the states merged into one class give outputs that are close but not equal. It is tempting to declare them equal and take one canonical quotient. This paper replaces that step by exact finite mathematics. Part I asks when a readout descends approximately through a fixed quotient. It does exactly when every class has an allowed common center, a finite form of the 1-center problem. The best uniform radius is a finite minimax. For a pseudometric loss it is at least half the largest fiber diameter, and at most that diameter when each class may use one of its own outputs as center; both bounds are sharp. Pairwise and equivalence repairs of the tolerance have least elements, but center repairs need not: on three points there are two incomparable minimal ones. A proposed bound of idempotence defect by lumpability is false, and a sharp weight-floor inequality replaces it. Part II starts from one finite graded tolerance and builds its clique, component, matrix and path-metric surrogates. They are separate functors with different universal properties, the center of the matrix algebra pulls back rather than pushes forward, and two tolerances on four points share every component profile while differing in first homology. All results are exact, with Lean 4 formalizations.