PureVectorCDoublingData
plain-language theorem explainer
PureVectorCDoublingData packages the four symmetry-induced zero conditions on a completed-ξ surface together with the explicit FE/RCL doubling recurrence for the defect. Researchers examining symmetry-only constraints on zeta zeros cite this structure to demarcate the data extractable from reflection and conjugation alone. The definition assembles the zero equalities at ρ, 1-ρ, conj ρ and 1-conj ρ plus the recurrence doubledZeroDefect ρ = 2(zeroDefect ρ)^2 + 4 zeroDefect ρ without further lemmas.
Claim. Let $Ξ$ be a completed-ξ surface and $ρ ∈ ℂ$. The pair satisfies pure Vector C doubling data when $Ξ.xi(ρ)=0$, $Ξ.xi(1-ρ)=0$, $Ξ.xi(¯ρ)=0$, $Ξ.xi(1-¯ρ)=0$, and the doubled zero defect equals $2·(zeroDefect ρ)^2 + 4·(zeroDefect ρ)$.
background
The module formalizes the Vector C symmetry-only no-go: functional-equation reflection plus conjugation symmetry produce pairing data on zeros but do not force the critical line. A CompletedXiSurface is a function xi:ℂ→ℂ obeying xi(1-s)=xi(s) for all s and xi(conj s)=conj(xi s) for all s. functionalReflection ρ is defined as 1-ρ; criticalReflection ρ is 1-conj ρ. zeroDefect ρ applies the RS defect functional to the deviation of ρ; doubledZeroDefect ρ applies J_log to twice that deviation.
proof idea
This is a structure definition that directly encodes the conjunction of the four zero conditions and the recurrence equality. No proof tactics or lemmas are applied; the fields are the literal properties drawn from CompletedXiSurface and the doubledZeroDefect definition.
why it matters
The structure supplies the data package used to establish that pure FE symmetry plus the current doubling law cannot force the critical line, as shown by pureVectorCDoublingData_not_enough_for_critical_line and the offline example at Re=3/4. It marks the boundary before extra analytic input (Euler/Hadamard factors or phase bounds) is required to reach a ZeroCompositionWitness. In the Recognition framework this corresponds to the symmetry stage prior to T5 J-uniqueness or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.