Reciprocal Orbit Geometry Under Reflection and Conjugation Symmetry

This paper gives a scoped Lean 4 formalization of centered and reciprocal coordinates for a complex-valued function with reflection symmetry about a real centre and conjugation symmetry. It proves that reflection reverses both coordinates, that the centered real part detects the symmetry line, and that a zero generates the reflection and conjugation orbit. The package verifies seven theorems with lake build and trust-zero checks. Its formal scope is the algebra of centered and reciprocal coordinates, critical-line detection, and four-point zero orbits under the two stated symmetry assumptions.