zeroDeviationSet
plain-language theorem explainer
zeroDeviationSet collects the real deviation values realized at the zeros of a supplied completed-ξ surface. Researchers working on zero-pairing invariants for Vector C cite this definition when deriving negation symmetry from the functional equation. The definition is a direct set comprehension that extracts zeroDeviation values from the zeros of the xi map.
Claim. Let $Ξ$ be a completed-ξ surface. Then zeroDeviationSet$(Ξ)$ is the set of all real $t$ such that there exists complex $s$ with $Ξ.xi(s)=0$ and zeroDeviation$(s)=t$.
background
CompletedXiSurface is the minimal structure that supplies a map xi : ℂ → ℂ together with the reflection axiom xi(1-s)=xi(s) and the conjugation axiom xi(conj s)=conj(xi s). zeroDeviation is the real-valued function on ℂ that records the deviation cost of each point, imported from the zero-location cost module. The present module deliberately restricts itself to these pairing data and does not yet encode any d'Alembert-style composition law.
proof idea
One-line definition that builds the set by existential quantification over the zeros of Ξ.xi and the matching zeroDeviation values.
why it matters
The definition supplies the deviation set that is proved negation-closed in the downstream theorem zeroDeviationSet_neg_closed, which follows immediately from the reflection property of the completed-ξ surface. It therefore records the strongest zero-location consequence currently available from the minimal functional-equation symmetry surface for Vector C. The module leaves open whether this negation-closed property forces the only realized deviation to be zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.