Anchored Observer Distance Invariance

Abstract

Compatible group actions preserve observer distance and anchored radius.

Theorem 1.1 (Compatible actions preserve the observer geometry).

$$\forall G\in Type,A\in Type,X\in Type,O\in \mathrm{Set}\left(A\right),L\in A\to [0,\infty ],e\in X\to \left(A\to \mathbb{R}\right),o\in X,\left(\left(\mathrm{Group}\left(G\right)\wedge \left(\mathrm{MulAction}\left(G,A\right)\wedge \mathrm{MulAction}\left(G,X\right)\right)\right)\wedge \left(\left(\forall g\in G,f\in A,f\in O\Rightarrow \mathrm{act}\left(g,f\right)\in O\right)\wedge \left(\left(\forall g\in G,f\in A,f\in O\Rightarrow L\left(\mathrm{act}\left(g,f\right)\right)=L\left(f\right)\right)\wedge \left(\forall g\in G,f\in A,x\in X,e\left(\mathrm{act}\left(g,x\right),\mathrm{act}\left(g,f\right)\right)=e\left(x,f\right)\right)\right)\right)\right)\Rightarrow \left(\mathrm{observerDistance}\left(O,L,e,o,o\right)=0\wedge \left(\left(\forall g\in G,x\in X,y\in X,\mathrm{observerDistance}\left(O,L,e,\mathrm{act}\left(g,x\right),\mathrm{act}\left(g,y\right)\right)=\mathrm{observerDistance}\left(O,L,e,x,y\right)\right)\wedge \left(\forall g\in G,x\in X,\mathrm{act}\left(g,o\right)=o\Rightarrow \mathrm{observerDistance}\left(O,L,e,o,\mathrm{act}\left(g,x\right)\right)=\mathrm{observerDistance}\left(O,L,e,o,x\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The action transports every admissible observable, preserves its cost, and commutes with evaluation. Reindexing the unit-cost supremum by the inverse action proves distance invariance in both directions.

References

• Truth anchor: D5/S3/ContinuousObservables/AnchoredObserverDistanceInvariance.anchored_observer_distance_invariance
• Dependency: D5/S3/Observer/Separation/RefinementDistanceMonotonicity