One-Scale Informational Completeness

Abstract

All integer moments of one weighted Cayley pushforward determine the real spectrum.

Theorem 1.1 (One complete Cayley scale determines the spectrum).

$$\begin{array}{c}\forall a:\mathbb{R},\\ nu1,nu2:\mathrm{Measure}(\mathbb{R}),\\ 0<a\wedge \\ \mathrm{HasFiniteIntegral}(xi\mapsto \frac{1}{x{i}^2+a^2},nu1)\wedge \\ \mathrm{HasFiniteIntegral}(xi\mapsto \frac{1}{x{i}^2+a^2},nu2)\Rightarrow \\ \mathrm{let}density:\mathbb{R}\to \mathrm{ENNReal}():=xi\mapsto \mathrm{ofReal}(\frac{1}{x{i}^2+a^2}),\\ \mathrm{let}cayleyPoint:\mathbb{R}\to Circle:=xi\mapsto \mathrm{circlePoint}(\frac{xi+i\cdot a}{xi-i\cdot a}),\\ \mathrm{let}cayleyCoordinate:\mathbb{R}\to \mathrm{AddCircle}(2\cdot \pi ):=xi\mapsto \mathrm{symm}({\mathrm{homeomorphCircle}}^{\prime },cayleyPoint\left(xi\right)),\\ \mathrm{let}circleMeasure:\mathrm{Measure}(\mathbb{R})\to \mathrm{Measure}(\mathrm{AddCircle}(2\cdot \pi )):=nu\mapsto \mathrm{map}(cayleyCoordinate,\mathrm{withDensity}(nu,density)),\\ (\forall n:\mathbb{Z},\mathrm{integral}(circleMeasure\left(nu1\right),theta\mapsto fourier\left(n,theta\right))=\mathrm{integral}(circleMeasure\left(nu2\right),theta\mapsto fourier\left(n,theta\right)))\Rightarrow nu1=nu2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MeasureSeparation/OneScaleInformationalCompleteness.one_scale_informational_completeness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proposition constructs the source resolvent density, the scaled Cayley point, its additive-circle coordinate, and the resulting pushforward measure from each real spectrum.

Finite resolvent budgets make both circle measures finite. Equality of every integer Fourier moment identifies them through the separating Fourier star algebra.

The Cayley coordinate is a measurable embedding. Pulling the measure equality back and cancelling the everywhere positive finite density recovers equality of the original real measures.

References

• Truth anchor: D5/S3/Observer/MeasureSeparation/OneScaleInformationalCompleteness.one_scale_informational_completeness