Permutation-Orbit Horizon

Abstract

Full permutation readouts place the horizon exactly outside the cyclic update orbit.

Theorem 1.1 (The full-readout horizon is the cyclic-orbit complement).

$$\forall I,tau\in \mathrm{EquivPerm}(I),x,y,o\in I,(\mathrm{observerDistance}(tau,x,y)=\infty ⟺\mathrm{Orb}(tau,x)\ne \mathrm{Orb}(tau,y))\wedge (\forall n\in \mathbb{Z},y=\mathrm{act}(ta{u}^n,x)\Rightarrow \mathrm{observerDistance}(tau,x,y)\le \left|n\right|)\wedge \mathrm{horizonSet}(tau,o)=I\setminus \mathrm{Orb}(tau,o)\wedge \mathrm{finiteDistanceBall}(tau,o)=\mathrm{Orb}(tau,o).$$

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

Source. Repository-derived.

Commentary.

The update orbit is Mathlib’s canonical orbit of the subgroup generated by all integer powers of the permutation. A bounded indicator of one such orbit is update-invariant, so distinct orbits have infinite observer distance by the frozen invariant-leaf theorem.

On a common orbit, the unit edge bound telescopes along positive powers. For a negative power, the proof telescopes forward from that iterate back to the origin and swaps the distance endpoints. This gives the absolute integer bound without assuming the carrier is finite.

The horizon and finite-distance ball are defined directly as the top and non-top fibers of the existing observer distance. Their displayed set equalities are public conjuncts of the same theorem.

References

• Truth anchor: D5/S3/ContinuousObservables/PermutationOrbitHorizon.permutation_observer_horizon_eq_orbit_complement
• Dependency: D5/S3/ContinuousObservables/ObserverDistanceClassification