Self-Description Distance Classification

Abstract

Self-description differences split into zero, finite-reachable, and horizon distances.

Theorem 1.1 (Self-description differences have three operational distance classes).

$$\begin{array}{r}\forall I,S:Type,tau:\mathrm{Perm}\left(I\right),\\ Delta:S\to I\to \mathbb{R},\mathrm{let}D=\left\{\exists s:S,\mathrm{selfReadout}\left(Delta,s,\mathrm{fst}\left(p\right)\right)\ne \mathrm{selfReadout}\left(Delta,s,\mathrm{snd}\left(p\right)\right)\mid p\in I\times I\right\}\\ \mathrm{in}(\forall p\in D,((\mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)=0\wedge \forall f:I\to \mathbb{R},\mathrm{edgeAdmissible}\left(tau,f\right)\Rightarrow f\left(\mathrm{fst}\left(p\right)\right)=f\left(\mathrm{snd}\left(p\right)\right))\vee (0<\mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)<\infty )\vee (\mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)=\infty \wedge \forall n:\mathbb{Z},\mathrm{snd}\left(p\right)\ne \left(ta{u}^n\right)\left(\mathrm{fst}\left(p\right)\right))))\wedge \\ ((\forall p\in D,(\mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)=0\vee \mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)=\infty ))\Rightarrow \forall p\in D,\neg (\exists f:I\to \mathbb{R},n:\mathbb{Z},\mathrm{edgeAdmissible}\left(tau,f\right)\wedge f\left(\mathrm{fst}\left(p\right)\right)\ne f\left(\mathrm{snd}\left(p\right)\right)\wedge \mathrm{snd}\left(p\right)=\left(ta{u}^n\right)\left(\mathrm{fst}\left(p\right)\right)))\wedge \\ (\forall p\in D,(0<\mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)<\infty )\Rightarrow \exists f:I\to \mathbb{R},n:\mathbb{Z},\mathrm{edgeAdmissible}\left(tau,f\right)\wedge f\left(\mathrm{fst}\left(p\right)\right)\ne f\left(\mathrm{snd}\left(p\right)\right)\wedge \mathrm{snd}\left(p\right)=\left(ta{u}^n\right)\left(\mathrm{fst}\left(p\right)\right)\wedge \mathrm{observerDistance}\left(tau,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)\le \left|n\right|).\end{array}$$

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

Source. Repository-derived.

Commentary.

A self-description difference is an endpoint pair separated by at least one member of the supplied self-readout family. The outside distance is the canonical supremum over bounded unit-edge readouts for the supplied permutation update.

Zero distance forces every admissible readout to agree. Infinite distance excludes every finite signed update path. If all self-description differences are in one of those two hidden classes, no admissible readout can distinguish a pair along such a path.

A finite-positive distance supplies both an admissible separating readout and a signed update path. The imported permutation-horizon theorem bounds the observer distance by that path’s length.

References

• Truth anchor: D5/S3/ContinuousObservables/SelfDescriptionDistanceClassification.self_description_distance_classification
• Dependency: D5/S3/ContinuousObservables/PermutationOrbitHorizon