functionalEquation_gives_pairing_invariants
plain-language theorem explainer
If a completed xi surface vanishes at s then it vanishes at the functional reflection 1-s, the complex conjugate, and the critical reflection 1-conjugate s, while zero deviation flips sign under functional reflection and stays invariant under conjugation, and zero defect remains invariant under all three maps. Number theorists tracking zeta-zero distributions cite the result for its explicit pairing constraints. The proof is a term-mode refinement that applies the three zero-pairing lemmas followed by the five deviation and defect invariance le
Claim. Let $s$ be a complex number and let $xi$ be a completed xi-surface obeying $xi(1-s)=xi(s)$ and $xi(conj s)=conj(xi(s))$. If $xi(s)=0$ then $xi(1-s)=0$, $xi(conj s)=0$, and $xi(1-conj s)=0$; moreover zeroDeviation$(1-s)$ equals the negative of zeroDeviation$(s)$, zeroDeviation is unchanged under conjugation, and zeroDefect is unchanged under functional reflection, conjugation, and critical reflection.
background
CompletedXiSurface is the structure carrying a map xi from complex numbers to complex numbers together with the two axioms that xi(1-s) equals xi(s) for every s and that xi of the conjugate of s equals the conjugate of xi(s). The module records only the minimal functional-equation symmetry surface required for Vector C; its explicit purpose is to encode pairing data on zeros and thereby produce reflection and conjugation invariants for zeroDeviation and zeroDefect, without yet supplying a d'Alembert-style composition law. The upstream definition states that any stronger zero-location constraint must be added on top of this surface and is not present by default.
proof idea
The term proof refines the eight conjuncts by direct application of the three pairing lemmas zero_pairing_under_reflection, zero_pairing_under_conjugation and zero_pairing_under_critical_reflection together with the five invariance statements zeroDeviation_functionalReflection, zeroDeviation_conj, zeroDefect_invariant_under_functional_reflection, zeroDefect_invariant_under_conjugation and zeroDefect_invariant_under_reflection.
why it matters
The declaration supplies the strongest zero-location consequence currently available from the minimal completed-xi surface, as stated in the module comment. It closes the symmetry data needed for Vector C by converting the functional equation into concrete invariants on zeroDeviation and zeroDefect. No downstream uses are recorded yet, but the result sits inside the NumberTheory layer that prepares pairing data for later composition-law extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.