Dual Observer Distance Readings

Abstract

Two bounded-function observers assign a typed extended-distance reading to the same endpoints.

Theorem 1.1 (One endpoint pair has two typed observer readings).

$$\begin{array}{r}\forall X:Type,A,APrime:\mathrm{Submodule}(\mathbb{R},\mathrm{ellInfty}(X,\mathbb{R})),\\ L:A\to [0,\infty ],LPrime:APrime\to [0,\infty ],x,y:X,\\ (\forall c:\mathbb{R},f:A,L(cf)=\left|c\right|L(f))\wedge (\forall c:\mathbb{R},f:APrime,LPrime(cf)=\left|c\right|LPrime(f))\Rightarrow \\ \mathrm{let}{d}_O=\mathrm{observerDistance}(A,L,x,y);\\ \mathrm{let}{d}_{OPrime}=\mathrm{observerDistance}(APrime,LPrime,x,y);\\ \mathrm{let}{Z}_O=\mathrm{span}(\mathbb{R},\mathrm{unitBall}(A,L))=A\Rightarrow (d_O=0⟺\forall f\in A,f(x)=f(y));\\ \mathrm{let}{Z}_{OPrime}=\mathrm{span}(\mathbb{R},\mathrm{unitBall}(APrime,LPrime))=APrime\Rightarrow (d_{OPrime}=0⟺\forall f\in APrime,f(x)=f(y));\\ \mathrm{let}{H}_O=(\exists f\in A,L(f)=0\wedge f(x)\ne f(y))\Rightarrow d_O=\infty ;\\ \mathrm{let}{H}_{OPrime}=(\exists f\in APrime,LPrime(f)=0\wedge f(x)\ne f(y))\Rightarrow d_{OPrime}=\infty \\ \mathrm{in}((d_O=0\wedge Z_O\wedge H_O)\vee (0<d_O<\infty \wedge Z_O\wedge H_O)\vee (d_O=\infty \wedge Z_O\wedge H_O))\wedge ((d_{OPrime}=0\wedge Z_{OPrime}\wedge H_{OPrime})\vee (0<d_{OPrime}<\infty \wedge Z_{OPrime}\wedge H_{OPrime})\vee (d_{OPrime}=\infty \wedge Z_{OPrime}\wedge H_{OPrime})).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ContinuousObservables/DualObserverDistanceReadings.dual_observer_distance_readings (✓ std3). ∎

Source. Repository-derived.

Commentary.

The observable carriers are real subspaces of the bounded functions on the state set. Each cost is homogeneous under real scaling, and each distance is the supremum of endpoint gaps over its unit-cost ball.

When that unit ball spans its observable space, zero distance is exactly equality of all accessible readouts. A zero-cost observable that separates the endpoints can be scaled without cost and therefore forces infinite distance.

References

• Truth anchor: D5/S3/ContinuousObservables/DualObserverDistanceReadings.dual_observer_distance_readings
• Dependency: D5/S3/Observer/Separation/RefinementDistanceMonotonicity