zero_pairing_under_conjugation
plain-language theorem explainer
Zeros of the completed xi surface are closed under complex conjugation by the reality symmetry axiom. Researchers assembling zero-pairing invariants for Vector C in the Recognition framework cite this when building the minimal symmetry surface. The proof is a direct one-line rewrite that applies the conjugation property of the surface and simplifies using conj(0) = 0.
Claim. Let $X$ be a completed-$xi$ surface. If $xi(s) = 0$ then $xi(conj(s)) = 0$.
background
The CompletedXiSurface structure supplies the minimal symmetry data for Vector C. It consists of a function $xi : C to C$ together with the reflection axiom $xi(1-s) = xi(s)$ from the completed functional equation and the conjugation axiom $xi(conj s) = conj(xi s)$ encoding reality symmetry. Any stronger zero-location constraint must be added on top of this surface.
proof idea
The proof is a one-line wrapper that applies the conjugation axiom of CompletedXiSurface to the hypothesis $xi s = 0$. The rewrite replaces $xi(conj s)$ by $conj(xi s)$, after which simplification recognizes that the conjugate of zero is zero.
why it matters
This supplies the conjugation leg of the zero-pairing invariants. It is invoked by functionalEquation_gives_pairing_invariants to collect all available symmetries and by pureVectorCDoublingData_of_zero to equip any completed-$xi$ zero with the pure Vector C doubling package. It closes the conjugation half of the symmetry surface in the CompletedXiSymmetry module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.