Linear Cayley Scale Flow

Abstract

The canonical logarithmic Cayley flow has a transport-decay generator and invariant characteristics.

Definition 1.1 (Cayley characteristic).

$$\forall u:\mathbb{C},tau:\mathbb{R},\mathrm{chi}\left(u,tau\right)=\mathrm{Phi}\left(\tanh \left(-\frac{tau}{2}\right),u\right).$$

Formalization. D5/S3/Weil/Budget/LinearCayleyScaleFlow.cayleyCharacteristic (✓ std3).

Source. Repository-derived.

Commentary.

The characteristic is the imported real disk automorphism with the negative half-time hyperbolic parameter.

Definition 1.2 (Disk artanh branch).

$$\forall w:\mathbb{C},\mathrm{diskArtanh}\left(w\right)=\frac{\log \left(1+w\right)-\log \left(1-w\right)}{2}.$$

Formalization. D5/S3/Weil/Budget/LinearCayleyScaleFlow.diskArtanh (✓ std3).

Source. Repository-derived.

Commentary.

This half-log expression fixes the analytic branch on the complex unit disk.

Theorem 1.3 (Linear Cayley scale PDE).

$$\begin{gathered} \forall nu:\mathrm{Measure}\left(\mathbb{R}\right),tau:\mathbb{R},w,u:\mathbb{C}, \\ \mathrm{map}\left(x\mapsto -x,nu\right)=nu\wedge \\ \forall a:\mathbb{R},0<a\Rightarrow \mathrm{FiniteMeasure}\left(W_a(nu)\right)\wedge \\ \Vert w\Vert <1\wedge \Vert u\Vert <1\Rightarrow \\ \mathrm{HasDerivAt}\left(t\mapsto F\left(\exp \left(t\right),nu,w\right),\frac{1-w^2}{2}\cdot \mathrm{deriv}\left(w\mapsto F\left(\exp \left(tau\right),nu,w\right),w\right)-F\left(\exp \left(tau\right),nu,w\right),tau\right)\wedge \\ \mathrm{HasDerivAt}\left(t\mapsto \mathrm{chi}\left(u,t\right),-\frac{1-\mathrm{chi}{\left(u,tau\right)}^2}{2},tau\right)\wedge \\ \mathrm{HasDerivAt}\left(t\mapsto \mathrm{diskArtanh}\left(\mathrm{chi}\left(u,t\right)\right)+\frac{\mathrm{ofReal}\left(t\right)}{2},0,tau\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Differentiation under the finite resolvent integral supplies the spatial derivative. The imported finite scale-covariance law then gives the time generator, while the explicit characteristic makes the disk-artanh coordinate invariant.

References

• Truth anchor: D5/S3/Weil/Budget/LinearCayleyScaleFlow.cayleyCharacteristic
• Truth anchor: D5/S3/Weil/Budget/LinearCayleyScaleFlow.diskArtanh
• Truth anchor: D5/S3/Weil/Budget/LinearCayleyScaleFlow.linear_cayley_scale_pde
• Dependency: D5/S3/Weil/Budget/CaratheodoryScaleCovariance