Logarithmic Radial Defect

Abstract

The logarithmic Cayley radius detects the midline and reverses under the mirror.

Theorem 1.1 (Logarithmic radial defect and mirror reversal).

$$\begin{array}{c}\forall Z:\mathrm{ZeroData},\\ (\forall n,\beta ({\rho }_n)=\frac{1}{2}\log (\frac{\Vert {\rho }_n-1{\Vert }^2}{\Vert {\rho }_n{\Vert }^2}))\wedge \\ (\mathrm{AllZerosOnMidline}(Z)\iff \forall n,\beta ({\rho }_n)=0)\wedge \\ (\forall n,\Vert c(\mathrm{mirror}({\rho }_n))\Vert =\Vert c({\rho }_n){\Vert }^{-1})\wedge \\ (\forall n,\beta (\mathrm{mirror}({\rho }_n))=-\beta ({\rho }_n)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let Z be the canonical exhaustive, duplicate-free source-zero carrier. For a complex point rho, c(rho) is the imported Cayley coefficient (rho - 1)/rho, and beta(rho) is log |c(rho)|.

The first public conjunct rewrites beta on every indexed source zero as one half the logarithm of the squared-norm ratio. The second applies the canonical Cayley unitarity criterion to identify simultaneous vanishing with the global midline predicate.

The remaining public conjuncts state reciprocal Cayley norm and logarithmic sign reversal under the imported conjugate-reflection mirror. The open-strip fields stored in ZeroData exclude both zero and one, so the coefficient norm used in the midline argument is positive.

Pinned Mathlib supplies the logarithm-of-a-square and logarithm-of-an-inverse identities. The mirror norm calculation uses the canonical complex conjugation norm identity rather than introducing a second reflection.

References

• Truth anchor: D5/S3/Midline/Cayley/LogarithmicRadialDefect.logarithmic_radial_defect_and_mirror
• Dependency: D5/S3/Midline/Cayley/CayleyUnitarityDefect
• Dependency: D5/S3/Weil/ReflectionLedger