pureVectorCDoublingData_offline_example
plain-language theorem explainer
This theorem supplies an explicit toy completed-ξ surface whose zero satisfies the pure Vector C doubling data yet lies off the critical line. Researchers examining whether functional-equation symmetries alone can locate zeta zeros would cite the result to mark the boundary of the symmetry-only package. The proof is a direct term construction that instantiates the existential with the toy surface and the point 3/4, then applies the sibling lemmas pureVectorCDoublingData_of_zero and toyCompletedXiSurface_has_off_critical_zero.
Claim. There exists a completed-ξ surface Ξ and a complex number ρ such that Ξ has a zero at ρ, the surface obeys reflection and conjugation symmetries at ρ, the doubling recurrence holds, and ρ does not lie on the critical line.
background
The module formalizes the Vector C symmetry-only stage gate: functional-equation reflection together with conjugation symmetry yield pairing data on zeros but do not force the critical line. A CompletedXiSurface is a function xi : ℂ → ℂ equipped with the axioms xi(1-s) = xi(s) and xi(conj s) = conj(xi s). PureVectorCDoublingData Ξ ρ packages the four zero conditions (at ρ, its functional reflection, its conjugate, and its critical reflection) plus the recurrence doubledZeroDefect ρ = 2·(zeroDefect ρ)² + 4·zeroDefect ρ.
proof idea
The proof is a term-mode construction. It refines the two existentials with toyCompletedXiSurface and the concrete point 3/4, then applies pureVectorCDoublingData_of_zero to the toy surface and the first component of toyCompletedXiSurface_has_off_critical_zero to obtain the PureVectorCDoublingData witness, and finally uses the second component of the same lemma to witness that the zero is off the critical line.
why it matters
The declaration supplies the concrete witness required by the two immediate downstream theorems pureVectorCDoublingData_not_enough_for_critical_line and pureVectorCDoublingData_requires_extra_input. Those results establish that pure FE/RCL symmetry plus the current doubling law cannot force the critical line or a ZeroCompositionWitness. In the Recognition framework this closes the symmetry-only gate for Vector C and points to the need for extra analytic input such as QuantitativeLocalFactorization and phaseIncrementEpsilonBound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.