Observer Ultrametric Threshold Closure

Abstract

Supremum distance over a bounded ultrametric readout family is an ultrapseudometric whose nonnegative threshold kernels are equivalence relations.

Theorem 1.1 (Observer suprema preserve ultrametric threshold closure).

$$\begin{array}{c}\forall P,X,Lambda:\mathrm{Type},\\ [\mathrm{PseudoMetricSpace}\left(Lambda\right)],\\ Q:\mathrm{Set}\left(P\right),q:P\to \left(X\to Lambda\right),\\ \forall a,b:Lambda,\mathrm{dist}\left(a,b\right)\le 1,\\ \forall a,b,c:Lambda,\mathrm{dist}\left(a,c\right)\le \max (\mathrm{dist}\left(a,b\right),\mathrm{dist}\left(b,c\right))\Rightarrow \\ \mathrm{let}(d_Q:X\to \left(X\to \mathbb{R}\right),\forall x,y:X,d_Q(x,y)=\mathrm{sSup}\left(\left\{\mathrm{dist}\left(q\left(p\right)\left(x\right),q\left(p\right)\left(y\right)\right)\mid p\in Q\right\}\right),\\ K_Q:\mathrm{NNReal}\to \left(X\to \left(X\to \mathrm{Prop}\right)\right),\forall epsilon:\mathrm{NNReal},x,y:X,K_Q(epsilon,x,y)⟺d_Q(x,y)\le epsilon)\\ (\forall x,y:X,0\le d_Q(x,y))\wedge \\ (\forall x:X,d_Q(x,x)=0)\wedge \\ (\forall x,y:X,d_Q(x,y)=d_Q(y,x))\wedge \\ (\forall x,y,z:X,d_Q(x,z)\le \max (d_Q(x,y),d_Q(y,z)))\wedge \\ \forall epsilon:\mathrm{NNReal},\mathrm{Equivalence}\left(K_Q(epsilon)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

The public statement constructs d_Q as the real supremum of the coordinate distances over the selected observer set Q. The boundedness premise makes every such supremum well defined.

A coordinate strong triangle inequality passes through the supremum. Self-distance, symmetry, and nonnegativity pass through as well, including the empty observer set where the real supremum is zero.

The threshold carrier is NNReal, so every admitted threshold is nonnegative without an additional premise. Reflexivity, symmetry, and transitivity then follow from the three corresponding distance laws.

References

• Truth anchor: D5/S3/Observer/MetricGeometryLaws/ObserverUltrametricThresholdClosure.observer_ultrametric_threshold_closure