zeroDefectSet
plain-language theorem explainer
zeroDefectSet collects the real defects realized by zeros of a completed-ξ surface. Number theorists establishing invariance of zero defects under functional equations cite this construction. The definition is realized by direct set comprehension over the zero locus of xi and the zeroDefect map.
Claim. Let $Ξ$ be a completed-ξ surface. Then zeroDefectSet$(Ξ) = { d ∈ ℝ | ∃ s ∈ ℂ : Ξ.xi(s) = 0 ∧ zeroDefect(s) = d }$.
background
CompletedXiSurface is the structure carrying xi : ℂ → ℂ together with the reflection axiom xi(1 − s) = xi(s) and the conjugation axiom xi(conj s) = conj(xi s). The module records only the pairing data on zeros that follows from these symmetries; stronger location constraints are added later. zeroDefect is the defect map imported from ZeroLocationCost; the present definition simply collects its values on the zero set of xi.
proof idea
Direct set comprehension: the set of all real d such that there exists s with xi(s) = 0 and zeroDefect(s) = d.
why it matters
This definition supplies the domain for the downstream theorem zeroDefectSet_reflection_invariant, which shows that the functional equation preserves the realized defect set. It forms part of the minimal symmetry surface for Vector C, providing the pairing invariants required before any d'Alembert-style composition law is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.