Evaluation Supremum Minimality

Abstract

Evaluation suprema are the least pseudometrics dominating every readout distance.

Theorem 1.1 (State and protocol evaluation suprema are least dominating).

$$\begin{array}{c}\forall X,P,\Lambda :\mathrm{Type},\\ \mathrm{PseudoMetricSpace}(\Lambda ),e:X\to \left(P\to \Lambda \right),\\ {\delta }_X:\mathrm{PseudoMetricSpace}(X),{\delta }_P:\mathrm{PseudoMetricSpace}(P),\\ ((\forall x,y\in X,\forall p\in P,\mathrm{dist}(d_{\Lambda },\mathrm{eval}(e,x,p),\mathrm{eval}(e,y,p))\le \mathrm{dist}({\delta }_X,x,y))\Rightarrow \forall x,y\in X,{\sup }_{p\in P}\mathrm{dist}(d_{\Lambda },\mathrm{eval}(e,x,p),\mathrm{eval}(e,y,p))\le \mathrm{dist}({\delta }_X,x,y))\\ \wedge \\ ((\forall p,q\in P,\forall x\in X,\mathrm{dist}(d_{\Lambda },\mathrm{eval}(e,x,p),\mathrm{eval}(e,x,q))\le \mathrm{dist}({\delta }_P,p,q))\Rightarrow \forall p,q\in P,{\sup }_{x\in X}\mathrm{dist}(d_{\Lambda },\mathrm{eval}(e,x,p),\mathrm{eval}(e,x,q))\le \mathrm{dist}({\delta }_P,p,q)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MetricGeometryLaws/EvaluationSupremumMinimality.evaluation_suprema_are_least_dominating (✓ std3). ∎

Source. Repository-derived.

Commentary.

Lambda is a pseudometric law carrier, e evaluates a state-protocol pair, and delta_X and delta_P are arbitrary competitor pseudometrics on the exact source carriers.

The two displayed suprema are the canonical source constructions. Any pointwise upper bound for every state readout bounds the state supremum, and the same least-upper-bound argument applies to protocol responses.

The surrounding bounded-law assumption is not needed for this stronger minimality statement: each competitor hypothesis already supplies the required upper bound.

References

• Truth anchor: D5/S3/Observer/MetricGeometryLaws/EvaluationSupremumMinimality.evaluation_suprema_are_least_dominating