Caratheodory Scale Covariance

Abstract

Even resolvent spectra give covariant Caratheodory functions and budgets.

Definition 1.1 (Caratheodory kernel).

$$\forall z,w:\mathbb{C},K\left(z,w\right)=\frac{z+w}{z-w}.$$

Formalization. D5/S3/Weil/Budget/CaratheodoryScaleCovariance.caratheodoryKernel (✓ std3).

Source. Repository-derived.

Commentary.

The kernel is constructed directly from the two complex variables.

Definition 1.2 (Caratheodory function).

$$\forall nu:\mathrm{Measure}\left(\mathbb{R}\right),a:\mathbb{R},w:\mathbb{C},F_a(nu,w)=\mathrm{integral}\left(m{u}_a(nu),z\mapsto K\left(z,w\right)\right).$$

Formalization. D5/S3/Weil/Budget/CaratheodoryScaleCovariance.caratheodoryFunction (✓ std3).

Source. Repository-derived.

Commentary.

The function integrates the kernel against the imported Cayley spectral measure.

Definition 1.3 (Observer scale parameter).

$$\forall a,b:\mathbb{R},s_{a,b}=\frac{b-a}{a+b}.$$

Formalization. D5/S3/Weil/Budget/CaratheodoryScaleCovariance.observerScaleParameter (✓ std3).

Source. Repository-derived.

Commentary.

This parameter is the observer-side sign convention for the real disk automorphism.

Definition 1.4 (Resolvent budget).

$$\forall nu:\mathrm{Measure}\left(\mathbb{R}\right),a:\mathbb{R},R_a(nu)=\mathrm{toReal}\left(\mathrm{mass}\left(W_a(nu)\right)\right).$$

Formalization. D5/S3/Weil/Budget/CaratheodoryScaleCovariance.resolventBudget (✓ std3).

Source. Repository-derived.

Commentary.

The budget is the real total mass of the resolvent-weighted source measure.

Theorem 1.5 (Caratheodory scale covariance).

$$\begin{gathered} \forall nu:\mathrm{Measure}\left(\mathbb{R}\right),a,b:\mathbb{R},w:\mathbb{C}, \\ 0<a\wedge 0<b\wedge \mathrm{map}\left(x\mapsto -x,nu\right)=nu\wedge \\ \mathrm{FiniteMeasure}\left(W_a(nu)\right)\wedge \mathrm{FiniteMeasure}\left(W_b(nu)\right)\wedge \Vert w\Vert <1\Rightarrow \\ {F}_b(nu,w)=\mathrm{ofReal}\left(\frac{a}{b}\right)\cdot F_a(nu,Ph{i}_{s_{a,b}}(w))\wedge \\ \mathrm{ofReal}\left(R_b(nu)\right)=\mathrm{ofReal}\left(\frac{a}{b}\right)\cdot F_a(nu,\mathrm{ofReal}\left(s_{a,b}\right)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Budget/CaratheodoryScaleCovariance.caratheodory_scale_covariance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Evenness cancels the imaginary normalization term after pairing the positive and negative spectral points. Evaluating the same law at zero gives the budget specialization.

References

• Truth anchor: D5/S3/Weil/Budget/CaratheodoryScaleCovariance.caratheodoryFunction
• Truth anchor: D5/S3/Weil/Budget/CaratheodoryScaleCovariance.caratheodoryKernel
• Truth anchor: D5/S3/Weil/Budget/CaratheodoryScaleCovariance.caratheodory_scale_covariance
• Truth anchor: D5/S3/Weil/Budget/CaratheodoryScaleCovariance.observerScaleParameter
• Truth anchor: D5/S3/Weil/Budget/CaratheodoryScaleCovariance.resolventBudget
• Dependency: D5/S3/Weil/Budget/PositiveCayleyScaleTransport