Observer World Covariance

Abstract

Covariant observers on transitive axes have equivalent output worlds.

Theorem 1.1 (Any two observer worlds are equivalent).

$$\begin{array}{r}\forall G,A,X,Y:\mathrm{Type},\\ [\mathrm{Group}\left(G\right)],[\mathrm{MulAction}\left(G,A\right)],[\mathrm{MulAction}\left(G,X\right)],\\ [\mathrm{IsPretransitive}\left(G,A\right)],\\ \forall O:A\to \left(X\to Y\right),U:G\to \mathrm{Equiv}\left(Y,Y\right),\\ (\forall g:G,a:A,x:X,\mathrm{apply}\left(O,\mathrm{smul}\left(g,a\right),\mathrm{smul}\left(g,x\right)\right)=\mathrm{apply}\left(U,g,\mathrm{apply}\left(O,a,x\right)\right))\Rightarrow \\ \forall a:A,b:A,\\ \exists g:G,\exists T:\mathrm{Equiv}\left(\mathrm{range}\left(\mathrm{apply}\left(O,a\right)\right),\mathrm{range}\left(\mathrm{apply}\left(O,b\right)\right)\right),\\ \mathrm{smul}\left(g,a\right)=b\wedge (\forall x:X,\mathrm{apply}\left(T,\mathrm{apply}\left(O,a,x\right)\right)=\mathrm{apply}\left(U,g,\mathrm{apply}\left(O,a,x\right)\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Naturality/ObserverWorldCovariance.observer_world_covariance (✓ std3). ∎

Source. Repository-derived.

Commentary.

An observer world is constructed directly as the range of that axis’s state-to-output map. Transitivity supplies a group element carrying one axis to the other.

Covariance shows that the corresponding output equivalence maps the first range onto the second. Restricting it to these ranges produces the displayed equivalence and transition computation rule.

Repository and pinned-library searches found no complete observer-world result. The generic transitivity witness and subtype restriction construction are applied directly.

References

• Truth anchor: D5/S3/Observer/Naturality/ObserverWorldCovariance.observer_world_covariance