White to Haar Identity

Abstract

Resolvent-weighted Cayley compactification carries normalized white spectrum to normalized circle Haar spectrum with the exact scale factor.

Definition 1.1 (Normalized Lebesgue spectrum).

$$m_0:\mathrm{Measure}(\mathbb{R})=\mathrm{ofReal}(\frac{1}{2\cdot \pi })\cdot \mathrm{volume}(\mathbb{R}).$$

Formalization. D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.normalizedLebesgueSpectrum (✓ std3).

Source. Repository-derived.

Commentary.

The source white spectrum is constructed as Lebesgue measure on the real line scaled by the reciprocal of two pi.

Definition 1.2 (Cayley map into the unit circle).

$$\begin{gathered} \forall a:\mathbb{R},h:a\ne 0,xi:\mathbb{R}, \\ \mathrm{cayleyCircle}(a,h,xi)=\mathrm{ofConjDivSelf}((xi:\mathrm{Complex}())-i\cdot a):Circle. \end{gathered}$$

Formalization. D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.cayleyCircle (✓ std3).

Source. Repository-derived.

Commentary.

The map is the canonical conjugate-over-self circle point. Its nonzero scale premise ensures that the denominator never vanishes.

Definition 1.3 (Resolvent compactification).

$$\begin{gathered} \forall a:\mathbb{R},h:a\ne 0,\nu :\mathrm{Measure}(\mathbb{R}), \\ \mathrm{resolventCompactification}(a,h,\nu )=\mathrm{map}(\mathrm{cayleyCircle}(a,h),\mathrm{withDensity}(\nu ,\mathrm{lambda}(xi:\mathbb{R},\mathrm{ofReal}(\frac{1}{\mathrm{sq}(xi)+\mathrm{sq}(a)})))). \end{gathered}$$

Formalization. D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.resolventCompactification (✓ std3).

Source. Repository-derived.

Commentary.

Compactification first weights the source measure by the reciprocal quadratic resolvent and then pushes it through the Cayley map.

Theorem 1.4 (White spectrum becomes Haar spectrum).

$$\begin{gathered} \forall a:\mathbb{R},lambda:ENNReal,\nu :\mathrm{Measure}(\mathbb{R}), \\ 0<a\Rightarrow \\ (\mathrm{resolventCompactification}(a,m_0)=\mathrm{ofReal}(\frac{1}{2\cdot a})\cdot m_T)\wedge \\ (\mathrm{resolventCompactification}(a,lambda\cdot m_0)=(lambda\cdot \mathrm{ofReal}(\frac{1}{2\cdot a}))\cdot m_T)\wedge \\ ((lambda\cdot m_0\le \nu )\iff ((lambda\cdot \mathrm{ofReal}(\frac{1}{2\cdot a}))\cdot m_T\le \mathrm{resolventCompactification}(a,\nu )))\wedge \\ (\mathrm{resolventCompactification}(\frac{1}{2},lambda\cdot m_0)=lambda\cdot m_T). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.white_to_haar_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

All binders and the positive-scale premise are displayed. The first two clauses give the base and arbitrary-intensity identities.

The third clause reflects measure domination in both directions, so the real-line white floor and circle Haar floor are equivalent.

At scale one half the coefficient is exactly one, giving the final scale-free correspondence.

References

• Truth anchor: D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.cayleyCircle
• Truth anchor: D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.normalizedLebesgueSpectrum
• Truth anchor: D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.resolventCompactification
• Truth anchor: D5/S3/Weil/TestFunctions/WhiteToHaarIdentity.white_to_haar_identity
• Dependency: D5/S3/Weil/Budget/FullCirclePrimalAttainment
• Dependency: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography