zeroDeviationSet_neg_closed_not_enough
plain-language theorem explainer
The theorem exhibits an explicit completed-ξ surface whose zero deviations include both 1/2 and -1/2 yet exclude 0. Researchers working on zero-location constraints in Recognition Science would cite it to show that functional-equation symmetry alone fails to force the critical line. The proof constructs the surface from a toy xi function with an off-line zero at 3/4 and applies the negation-closure property.
Claim. There exists a completed-ξ surface Ξ such that 1/2 belongs to its zero-deviation set, -1/2 also belongs to that set, and 0 does not belong to it.
background
The module formalizes the main stage gate for Vector C: functional-equation reflection symmetry plus conjugation symmetry give pairing data on zeros, but do not by themselves force the critical line. A completed-ξ surface is minimal data consisting of a function xi: ℂ → ℂ together with the reflection property xi(1-s) = xi(s) and the conjugation property xi(conj s) = conj(xi s). The zero-deviation set of such a surface collects all real t for which some zero s of xi satisfies zeroDeviation s = t. The negation-closed theorem states that the functional equation forces this set to be symmetric under negation.
proof idea
The proof refines toyCompletedXiSurface as witness. Membership of 1/2 follows by exhibiting the off-critical zero at 3/4 and applying norm_num on the deviation definition. The negative member is obtained directly by applying zeroDeviationSet_neg_closed to the positive member. Absence of 0 is shown by assuming a zero deviation of 0, invoking zeroDeviation_eq_zero_iff_on_critical_line to place the zero on the critical line, then computing that the toy xi is nonzero at that point.
why it matters
This theorem is the main stage gate for Vector C. It shows that the minimal completed-ξ surface equipped only with reflection and conjugation permits off-critical zeros while satisfying negation closure on deviations. The module states that any stronger zero-location constraint must be added on top of this surface. It touches the open question of what extra structure forces all zeros onto the critical line, a prerequisite for the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.