Asymmetric Permutation Observer Distances

Abstract

Invariant-label separation for one update and orbit reachability for another produce asymmetric observer distances.

Theorem 1.1 (Two permutation observers can assign infinite and finite distance).

$$\forall I,Leaf,tau,tauPrime\in \mathrm{EquivPerm}(I),leaf\in \mathrm{Map}(I,Leaf),x,y\in I,n\in \mathbb{Z},\mathrm{InvariantLabel}(tau,leaf)\wedge leaf(x)\ne leaf(y)\wedge x=\mathrm{act}(tauPrim{e}^n,y)\Rightarrow \mathrm{observerDistance}(tau,x,y)=\infty \wedge \mathrm{observerDistance}(tauPrime,x,y)\le \left|n\right|\wedge \mathrm{observerDistance}(tauPrime,x,y)<\infty .$$

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

Source. Repository-derived.

Commentary.

A bounded indicator of the first update’s invariant label separates the endpoints, so its scalable zero-defect readout forces infinite distance.

For the second update, the signed orbit witness gives a telescoping unit-edge bound. The natural absolute displacement is explicitly finite in the extended nonnegative reals.

References

• Truth anchor: D5/S3/ContinuousObservables/AsymmetricPermutationDistances.asymmetric_permutation_observer_distances
• Dependency: D5/S3/ContinuousObservables/PermutationOrbitHorizon