zeroDefectSet
plain-language theorem explainer
The definition zeroDefectSet extracts the set of realized zero defects from the zeros of a given completed-ξ surface. Analysts of functional-equation symmetries and zero-location constraints would cite this construction when tracking defect values under reflection. It proceeds by direct set comprehension that pairs the zero locus of the xi map with the zeroDefect assignment.
Claim. Let $Ξ$ be a completed-ξ surface. The zero defect set is the collection of all real numbers $d$ for which there exists a complex number $s$ such that $Ξ.xi(s)=0$ and zeroDefect$(s)=d$.
background
The module CompletedXiSymmetry supplies the minimal data structure CompletedXiSurface consisting of a map xi from complex numbers to complex numbers together with the reflection symmetry xi(1-s)=xi(s) and the conjugation symmetry xi(conj s)=conj(xi s). This encodes the functional equation and reality condition needed for Vector C, yielding pairing invariants on the zeros without imposing stronger location constraints. The zeroDefect function, drawn from the imported ZeroLocationCost module, assigns a real defect value to each zero location.
proof idea
The definition is a direct set comprehension that collects every real d for which there exists s with xi(s)=0 and zeroDefect(s)=d.
why it matters
This definition supplies the domain for the reflection invariance theorem zeroDefectSet_reflection_invariant, which establishes that the realized defect set is closed under the functional equation. It forms part of the symmetry surface for tracking zero defects in the completed xi function, supporting the extraction of pairing data required by the Recognition Science framework for Vector C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.