zero_pairing_under_critical_reflection
plain-language theorem explainer
Zeros of the completed xi surface remain zeros after critical reflection, the composition of functional reflection across the line Re(s)=1/2 with complex conjugation. Researchers assembling zero-pairing invariants for the Vector C construction cite this result when closing the symmetry surface. The proof is a one-line composition that first invokes conjugation invariance to reach the conjugate zero then applies reflection invariance.
Claim. Let $X$ be a completed-$xi$ surface, i.e., a function $xi:mathbb{C}to mathbb{C}$ obeying $xi(1-s)=xi(s)$ and $xi(overline{s})=overline{xi(s)}$ for all $s$. If $xi(s)=0$ then $xi(1-overline{s})=0$.
background
CompletedXiSurface supplies the minimal data for Vector C: a function $xi:mathbb{C}to mathbb{C}$ together with the two axioms $xi(1-s)=xi(s)$ (functional reflection) and $xi(overline{s})=overline{xi(s)}$ (reality conjugation). criticalReflection is defined as $1-overline{rho}$, the map that first reflects across the critical line and then conjugates. The module records only the pairing consequences of these symmetries; no d'Alembert composition law or explicit zero locations are present. Upstream, zero_pairing_under_reflection states that zeros are stable under functional reflection while zero_pairing_under_conjugation states stability under conjugation.
proof idea
Apply zero_pairing_under_conjugation to the hypothesis $xi(s)=0$ to obtain a zero at the conjugate point. Then invoke zero_pairing_under_reflection on that conjugate zero; the simpa tactic rewrites the definition of criticalReflection to finish the chain.
why it matters
The declaration supplies the missing critical-reflection leg of the zero-location invariants. It is used directly by functionalEquation_gives_pairing_invariants to assemble the triple of pairing statements and by pureVectorCDoublingData_of_zero to equip each zero with the full Vector C package. Within the Recognition framework it closes the symmetry surface needed before any RCL-based recurrence or phi-ladder mass formula can be applied to the zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.