xi_conjugation_invariant
plain-language theorem explainer
The theorem asserts that the completed xi function attached to a symmetry surface satisfies xi(conj s) equals the complex conjugate of xi(s). Researchers tracking zero pairings under the functional equation in analytic number theory would cite it when confirming reality properties of the xi surface. The proof is a direct one-line extraction of the conjugation field from the CompletedXiSurface structure.
Claim. Let $X$ be a completed-$xi$ surface. For every complex number $s$, $X(s^*) = {X(s)}^*$, where $^*$ denotes complex conjugation.
background
The CompletedXiSurface structure packages a map $xi:mathbb{C}to mathbb{C}$ together with two axioms: the reflection identity $xi(1-s)=xi(s)$ that encodes the completed functional equation, and the conjugation identity $xi(conj s)=conj(xi s)$ that encodes reality. This module supplies only the minimal symmetry data required for Vector C, which yields pairing invariants on zero sets but stops short of any d'Alembert-style composition law.
proof idea
The proof is a term-mode one-liner that applies the conjugation field of the supplied CompletedXiSurface instance directly to the argument $s$. No auxiliary lemmas or tactics are used; the result is immediate from the structure definition.
why it matters
The result isolates the conjugation symmetry that, together with the reflection symmetry, produces the zero-pairing invariants recorded elsewhere in the module. It supplies the reality condition needed for zeroDeviationSet and zeroDefectSet constructions, which in turn feed the functional-equation symmetries required by Recognition Science. The module leaves stronger zero-location constraints and composition laws for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.