zero_pairing_under_reflection
plain-language theorem explainer
The completed xi surface encodes a reflection symmetry under which zeros of the xi function are paired across the line Re(s) = 1/2. Number theorists or Recognition Science researchers establishing zero-location invariants would cite this when deriving pairing properties for the zero set. The proof is a direct one-line application of the built-in reflection axiom after unfolding the definition of functional reflection.
Claim. Let $X$ be a completed xi surface whose xi function satisfies $xi(1-s)=xi(s)$ for all complex $s$. If $xi(s)=0$, then $xi(1-s)=0$.
background
The CompletedXiSurface structure supplies the minimal data for the completed xi function in the Vector C symmetry setting. It consists of a map xi from complex numbers to complex numbers together with the reflection axiom xi(1-s)=xi(s) for all s and the conjugation axiom xi(conj s)=conj(xi s). The module records these symmetries to produce pairing data on zeros without imposing any d'Alembert-style composition law. functionalReflection is the map sending rho to 1-rho, which reflects across the critical line Re(s)=1/2.
proof idea
The proof is a one-line term that applies the reflection axiom of the CompletedXiSurface after substituting the definition of functionalReflection and the hypothesis that xi(s) equals zero.
why it matters
This supplies the reflection pairing used to derive the full set of zero-location invariants in functionalEquation_gives_pairing_invariants and to prove reflection invariance of the zero-defect set in zeroDefectSet_reflection_invariant. It forms part of the minimal completed-xi symmetry surface required for Vector C, delivering the basic pairing consequences of the functional equation before stronger constraints are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.