zeroDeviationSet_neg_closed_not_enough
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not prove that every completed-ξ surface has zeros only on the critical line.
- Does not supply the additional input required to force critical-line support.
- Does not contradict the Riemann hypothesis.
- Does not claim that reflection and conjugation symmetries are irrelevant to zero location.
formal statement (Lean)
70theorem zeroDeviationSet_neg_closed_not_enough :
71 ∃ Ξ : CompletedXiSurface,
72 (1 / 2 : ℝ) ∈ zeroDeviationSet Ξ ∧
73 (-1 / 2 : ℝ) ∈ zeroDeviationSet Ξ ∧
74 0 ∉ zeroDeviationSet Ξ := by
proof body
Tactic-mode proof.
75 refine ⟨toyCompletedXiSurface, ?_, ?_, ?_⟩
76 · refine ⟨(3 / 4 : ℂ), ?_, ?_⟩
77 · exact toyCompletedXiSurface_has_off_critical_zero.1
78 · norm_num [zeroDeviation]
79 · have hhalf : (1 / 2 : ℝ) ∈ zeroDeviationSet toyCompletedXiSurface := by
80 refine ⟨(3 / 4 : ℂ), ?_, ?_⟩
81 · exact toyCompletedXiSurface_has_off_critical_zero.1
82 · norm_num [zeroDeviation]
83 have hneg : (-(1 / 2 : ℝ)) ∈ zeroDeviationSet toyCompletedXiSurface :=
84 zeroDeviationSet_neg_closed toyCompletedXiSurface hhalf
85 norm_num at hneg ⊢
86 exact hneg
87 · intro hzero
88 rcases hzero with ⟨s, hs, hdev⟩
89 have hline : OnCriticalLine s :=
90 (zeroDeviation_eq_zero_iff_on_critical_line s).mp hdev
91 have hvalue :
92 toyCompletedXiSurface.xi s =
93 (((1 / 2 - 3 / 4) ^ 2 * (1 / 2 - 1 / 4) ^ 2 : ℝ) : ℂ) := by
94 simp [toyCompletedXiSurface, toyXi, show s.re = 1 / 2 by exact hline]
95 have hnonzero :
96 ((((1 / 2 - 3 / 4) ^ 2 * (1 / 2 - 1 / 4) ^ 2 : ℝ) : ℂ)) ≠ 0 := by
97 norm_num
98 have hxine : toyCompletedXiSurface.xi s ≠ 0 := by
99 simpa [hvalue] using hnonzero
100 exact hxine hs
101
102/-- The strongest concrete Vector C data currently available from pure
103completed-ξ symmetry plus the FE/RCL doubling law. -/