pureVectorCDoublingData_not_enough_for_critical_line
plain-language theorem explainer
Pure functional-equation symmetry together with the doubling recurrence on zeros fails to force every zero onto the critical line. Researchers working on symmetry-based zero-location constraints in the Recognition framework cite this no-go to justify adding further structure beyond the pure Vector C package. The argument is a one-line wrapper that instantiates an explicit off-critical toy surface satisfying the data and derives a contradiction from the universal assumption.
Claim. It is not the case that for every completed-ξ surface Ξ and complex number ρ, if ρ is a zero of Ξ satisfying the reflection, conjugation, and doubling conditions of the pure Vector C package then ρ has real part equal to 1/2.
background
A CompletedXiSurface consists of a function xi: ℂ → ℂ equipped with functional reflection xi(1-s) = xi(s) and conjugation xi(conj s) = conj(xi s). These supply the minimal symmetry data for Vector C; any stronger zero-location rule must be imposed separately. PureVectorCDoublingData strengthens this by requiring that ρ is a zero, its functional and critical reflections are zeros, its conjugate is a zero, and the defect satisfies the doubling recurrence doubledZeroDefect ρ = 2 (zeroDefect ρ)^2 + 4 zeroDefect ρ. OnCriticalLine is the predicate ρ.re = 1/2.
proof idea
Assume for contradiction that every zero obeying PureVectorCDoublingData lies on the critical line. The offline-example theorem supplies a concrete CompletedXiSurface and a zero ρ with real part 3/4 that satisfies the pure data yet violates OnCriticalLine. Substituting this pair into the assumption immediately yields the contradiction.
why it matters
This theorem certifies the main stage gate for Vector C: functional-equation reflection plus conjugation symmetry and the current doubling law produce pairing data on zeros but do not force the critical line. It aligns with the Recognition framework's stepwise derivation of constraints from the functional equation and composition laws without presupposing the critical line. No downstream theorems are recorded, leaving open the question of what additional input would close the gap to a full location theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.