Barycenter Defect Decomposition

Abstract

The completion barycenter and anti-coordinate separate center from mirror displacement.

Theorem 1.1 (Barycenter and anti-coordinate separate mirror pairs).

$$\begin{array}{c}\forall \rho \in \mathbb{C},\mathrm{completionBarycenter}(\rho ):=\frac{\rho +\mathrm{mirror}(\rho )}{2},\mathrm{antiCoordinate}(\rho ):=\frac{\rho -\mathrm{mirror}(\rho )}{2},\\ ((\forall \rho \in \mathbb{C},\mathrm{IsNontrivialZero}(\rho )\Rightarrow \Re (\rho )=\mathrm{criticalAbscissa})\iff (\forall \rho \in \mathbb{C},\mathrm{IsNontrivialZero}(\rho )\Rightarrow \mathrm{antiCoordinate}(\rho )=0))\wedge \\ \forall \Delta ,\Gamma \in \mathbb{R},\Delta \ne 0\Rightarrow \mathrm{let}r:\mathbb{C}:=(\mathrm{criticalAbscissa}+\Delta )+i\Gamma ;\mathrm{let}\ell :\mathbb{C}:=(\mathrm{criticalAbscissa}-\Delta )+i\Gamma ;\\ \mathrm{let}c:\mathbb{C}:=\mathrm{criticalAbscissa}+i\Gamma ;\mathrm{completionBarycenter}(r)=c\wedge \mathrm{completionBarycenter}(\ell )=c\wedge \\ \mathrm{antiCoordinate}(r)=\Delta \wedge \mathrm{antiCoordinate}(\ell )=-\Delta \wedge \mathrm{mirror}(r)=\ell \wedge \mathrm{mirror}(\ell )=r\wedge \\ \mathrm{card}\{r,\mathrm{mirror}(r)\}=2\wedge \Vert r-c\Vert =\left|\Delta \right|\wedge \Vert \ell -c\Vert =\left|\Delta \right|.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/Symmetry/BarycenterDefectDecomposition.barycenter_defect_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

The barycenter and anti-coordinate are constructed from the frozen conjugate-reflection map. Vanishing anti-coordinate on every nontrivial zero is exactly the critical-line condition.

For every real nonzero displacement and real height, the explicitly constructed symmetric pair has a common completion center, opposite anti-coordinates, and is exchanged by the mirror map. Its canonical two-point mirror orbit has radius equal to the absolute displacement.

References

• Truth anchor: D5/S3/Zeros/Symmetry/BarycenterDefectDecomposition.barycenter_defect_decomposition
• Dependency: D5/S3/Zeros/Symmetry/ZeroSymmetryAction