xi_reflection_invariant
plain-language theorem explainer
The theorem establishes invariance of the completed xi function under the functional reflection map on any CompletedXiSurface. Researchers deriving zero-pairing invariants for Vector C in Recognition Science would cite this when building reflection-closed sets of zeros. The proof is a one-line wrapper that unfolds functionalReflection and applies the reflection axiom of the surface.
Claim. Let $X$ be a completed-$xi$ surface equipped with a function $xi:mathbb{C}to mathbb{C}$ satisfying $xi(1-s)=xi(s)$ for all complex $s$. Then $xi(1-s)=xi(s)$ holds identically.
background
The CompletedXiSurface is defined as a structure carrying a map $xi:mathbb{C}to mathbb{C}$ together with two axioms: reflection $xi(1-s)=xi(s)$ and conjugation $xi(conj s)=conj(xi s)$. The module records the minimal functional-equation symmetry surface needed for Vector C; it supplies pairing data on zeros but deliberately omits any d'Alembert-style composition law. The upstream CompletedXiSurface doc-comment states that any stronger zero-location constraint must be added on top of this surface.
proof idea
This is a one-line wrapper that applies the reflection axiom of CompletedXiSurface after the simpa tactic unfolds the definition of functionalReflection (the map $s mapsto 1-s$).
why it matters
The result supplies the reflection invariance of the completed xi value, a prerequisite for the sibling declarations zeroDeviationSet_reflection_invariant and zeroDefectSet_reflection_invariant. It encodes the completed functional-equation symmetry required for Vector C and thereby supports the pairing data on zeros that the module extracts from the classical zeta functional equation. In the Recognition framework this step closes the minimal symmetry surface before any phi-ladder or J-cost structure is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.