Phase Observer Translation

Abstract

The winding-phase observer carries the admissible crossing sandwich to the explicit translation by minus two on every rational additive circle.

Theorem 1.1 (The phase observer descends to translation).

$$\begin{array}{r}\forall m\in \mathbb{Q},q_m(A)=[Psi(A){]}_m\\ T_m:\mathrm{AddCircle}\left(m\right)\to \mathrm{AddCircle}\left(m\right),T_m(z)=z-2\\ q_m\circ sigma=T_m\circ q_m.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/CrossingPeriodicity/PhaseObserverTranslation.phase_observer_descends_to_translation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source state space consists of positive matrices satisfying the existing admissibility predicate. Its update is the existing crossing sandwich, which preserves that predicate.

For an arbitrary rational modulus m, the observer sends a matrix to its winding phase in the additive quotient by m. The target map is constructed explicitly as subtraction by two.

The exact single-step phase law proves that observing after the source update is the same as translating after observation. Thus the phase dynamics descends to the displayed translation.

References

• Truth anchor: D5/S3/PrimeForms/CrossingPeriodicity/PhaseObserverTranslation.phase_observer_descends_to_translation
• Dependency: D5/S3/PrimeForms/CrossingPeriodicity/SandwichPhasePeriod