Radial Boundary Phase Derivative

Abstract

The normal logarithmic Cayley radius and its smooth boundary phase have the same Poisson-kernel derivative.

Theorem 1.1 (Radial and boundary phase derivatives coincide).

$$\begin{array}{c}\forall a,gamma:\mathrm{Real}\left(\right),\\ 0<a\Rightarrow \\ \mathrm{let}cayleyCoordinate:\mathrm{Real}\left(\right)\to \left(\mathrm{Real}\left(\right)\to \mathrm{Complex}\left(\right)\right):=(gamma:\mathrm{Real}\left(\right),delta:\mathrm{Real}\left(\right)\mapsto \frac{\mathrm{complex}\left(gamma\right)-Complex.I\cdot \mathrm{complex}\left(delta\right)+Complex.I\cdot \mathrm{complex}\left(a\right)}{\mathrm{complex}\left(gamma\right)-Complex.I\cdot \mathrm{complex}\left(delta\right)-Complex.I\cdot \mathrm{complex}\left(a\right)}),\\ \mathrm{let}radialCoordinate:\mathrm{Real}\left(\right)\to \left(\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right)\right):=(gamma:\mathrm{Real}\left(\right),delta:\mathrm{Real}\left(\right)\mapsto \log \left(\Vert cayleyCoordinate\left(gamma,delta\right)\Vert \right)),\\ \mathrm{let}boundaryPhase:\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right):=(gamma:\mathrm{Real}\left(\right)\mapsto Real.pi-2\cdot \arctan \left(\frac{gamma}{a}\right)),\\ \mathrm{let}poissonKernel:\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right):=(gamma:\mathrm{Real}\left(\right)\mapsto \mathrm{RiemannPoissonDensityPoissonKernel}\left(a,gamma\right)),\\ \mathrm{complex}\left(Circle.exp\left(boundaryPhase\left(gamma\right)\right)\right)=cayleyCoordinate\left(gamma,0\right)\wedge \left(\Vert cayleyCoordinate\left(gamma,0\right)\Vert =1\wedge \left(\left(\forall delta\in \mathrm{Real}\left(\right),delta\ne 0\Rightarrow \Vert cayleyCoordinate\left(gamma,delta\right)\Vert \ne 1\right)\wedge \left(\mathrm{HasDerivAt}\left((delta:\mathrm{Real}\left(\right)\mapsto radialCoordinate\left(gamma,delta\right)),-2\cdot Real.pi\cdot poissonKernel\left(gamma\right),0\right)\wedge \mathrm{HasDerivAt}\left(boundaryPhase,-2\cdot Real.pi\cdot poissonKernel\left(gamma\right),gamma\right)\right)\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Midline/Cayley/RadialBoundaryPhaseDerivative.radial_boundary_phase_derivative (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a positive scale, the off-axis Cayley coordinate is constructed from the real tangential and normal coordinates. Its logarithmic norm is the radial coordinate, while pi minus twice the arctangent is a smooth real phase lift of the boundary value.

The exponential clause ties that lift to the canonical boundary Cayley point, including the branch-cut point. The norm clauses state that the coordinate is unitary exactly when the normal displacement vanishes.

Both derivative clauses use the same explicitly constructed Poisson kernel value. Thus the normal derivative of the logarithmic radius is the tangential derivative of the boundary phase.

References

• Truth anchor: D5/S3/Midline/Cayley/RadialBoundaryPhaseDerivative.radial_boundary_phase_derivative
• Dependency: D5/S3/Weil/TestFunctions/CayleyMomentTransport
• Dependency: D5/S3/Weil/ZetaAnalytic/RiemannPoissonDensity