Visible-Phase Infinity of the Observer Distance

Abstract

The ENNReal observable-supremum distance is infinite across distinct visible phases.

Theorem 1.1 (Distinct visible phases have top observer distance).

$$\forall tauxy,hphase\in H,projection(x)\ne projection(y)\Rightarrow observerDistance(tau,x,y)=\infty .$$

Proof. Machine-checked in Lean as D5/S3/Observer/MetricGeometry/VisiblePhaseInfinity.visible_phase_separation_distance_eq_top (✓ std3). ∎

Source. Repository-derived.

Commentary.

The distance is the supremum in ENNReal of the endpoint gaps of continuous complex observables whose read-update defect is at most one. If the update preserves the visible projection, the phase character obtained from AddCircle.toCircle has exactly zero defect. Scaling that character by every natural number gives admissible gaps with no finite upper bound. This is the finite observable-supremum shadow only; it does not claim a spectral triple, a bundle identification, or a type-II classification.

Theorem 1.2 (A nonidentity hidden translation supplies the witness).

$$\exists tau,tau\ne refl\wedge (\forall z,\mathrm{proj}(ta{u}^{-1}z)=\mathrm{proj}(z))\wedge \mathrm{proj}(\mathrm{flow}(0))\ne \mathrm{proj}(\mathrm{flow}(\frac{1}{2}))\wedge observerDistance(tau,\mathrm{flow}(0),\mathrm{flow}(\frac{1}{2}))=\infty .$$

Proof. Machine-checked in Lean as D5/S3/Observer/MetricGeometry/VisiblePhaseInfinity.hiddenTranslation_visible_phase_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The translation by the frozen nonzero hidden-unit offset is a genuine permutation of the solenoid. Its offset lies in the kernel of the visible projection, so the phase-preservation hypothesis holds. The real-flow points at zero and one half have distinct visible phases, and the main theorem therefore gives top distance for this concrete nonidentity update.

References

• Truth anchor: D5/S3/Observer/MetricGeometry/VisiblePhaseInfinity.hiddenTranslation_visible_phase_witness
• Truth anchor: D5/S3/Observer/MetricGeometry/VisiblePhaseInfinity.visible_phase_separation_distance_eq_top
• Dependency: D5/S1/Dynamics/UniversalSolenoid
• Dependency: D5/S1/Solenoid/StreamlineDecomposition
• Dependency: D5/S3/Observer/ObserverMetric