zeroDeviationSet_neg_closed
plain-language theorem explainer
The completed-ξ surface forces its realized zero-deviation set to be closed under negation via the functional equation. Researchers deriving minimal pairing constraints on zeta zeros cite this when bounding zero locations from symmetry alone. The term proof unpacks the membership witness, applies the reflection pairing lemma to the complex zero, and simplifies to confirm the negated deviation.
Claim. Let $Ξ$ be a completed-ξ surface. If $t$ lies in the zero-deviation set realized by $Ξ$, then $-t$ also lies in that set.
background
The module supplies the minimal completed-ξ symmetry surface required for Vector C. It encodes only the pairing data that follow from the functional equation and reality symmetry; stronger zero-location rules are deliberately omitted. CompletedXiSurface consists of a function xi : ℂ → ℂ together with the axioms xi(1 - s) = xi(s) and xi(conj s) = conj(xi s). zeroDeviationSet(Ξ) collects the real numbers t such that some zero s of xi satisfies zeroDeviation s = t. The upstream lemma zero_pairing_under_reflection states that if xi s = 0 then xi(1 - s) = 0, which directly supplies the reflected zero needed for sign flip of the deviation.
proof idea
The term proof begins with rcases on the membership hypothesis to extract the witnessing complex zero s. It then constructs the new witness by applying functionalReflection to s and invoking zero_pairing_under_reflection to obtain the reflected zero. The final simp step confirms that the deviation extracted from the reflected zero equals -t.
why it matters
This supplies the negation symmetry on the deviation set, described in the module doc-comment as the strongest zero-location consequence available from the minimal surface. It feeds the downstream counterexample zeroDeviationSet_neg_closed_not_enough, which exhibits a surface whose deviation set is negation-closed yet contains nonzero elements. Within the Recognition framework the result records the pairing invariants forced by the functional equation before any composition law or d'Alembert-style rule is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.