CompletedXiSurface
plain-language theorem explainer
The completed xi surface structure packages a complex-valued function with its reflection and conjugation symmetries as the minimal data package for Vector C. Number theorists deriving zero-pairing invariants in Recognition Science cite this surface when building sets such as XiZeroSet and zeroDefectSet. The declaration is a direct structure definition that introduces the three fields with no proof obligations.
Claim. A completed-$xi$ surface is a function $xi:mathbb{C}to mathbb{C}$ satisfying $xi(1-s)=xi(s)$ for all $sinmathbb{C}$ and $xi(bar s)=overline{xi(s)}$ for all $sinmathbb{C}$.
background
The Completed Xi Symmetry module records the minimal functional-equation symmetry surface needed for Vector C. It encodes only the completed zeta symmetries that give pairing data on zeros, yielding reflection and conjugation invariants for zeroDeviation and zeroDefect, but without any d'Alembert-style composition law.
proof idea
The declaration is a direct structure definition. It specifies the xi map together with the two forall axioms for reflection (completed functional equation) and conjugation (reality symmetry). No lemmas or tactics are invoked.
why it matters
This structure feeds the downstream theorems functionalEquation_gives_pairing_invariants, xi_reflection_invariant, xi_conjugation_invariant, and the derived sets XiZeroSet, zeroDefectSet, and zeroDeviationSet. It supplies the base symmetry surface for zero-location analysis in the Recognition Science framework, consistent with the forcing chain steps T5 J-uniqueness and T7 eight-tick octave, while leaving stronger zero constraints for later addition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.