PureVectorCDoublingData
plain-language theorem explainer
PureVectorCDoublingData packages the four zero-pairing conditions and the quadratic recurrence for the doubled defect that follow from completed-xi symmetry plus the FE/RCL doubling law. Researchers testing whether functional-equation data alone can force the critical line cite this as the maximal pure Vector C package. The definition directly records the zero equalities together with the explicit relation supplied by doubledZeroDefect and zeroDefect.
Claim. Let $Xi$ be a completed $xi$-surface and $rho in mathbb{C}$. The predicate holds when $Xi(rho)=0$, $Xi(1-rho)=0$, $Xi(overline{rho})=0$, $Xi(1-overline{rho})=0$, and the doubled zero defect equals $2,(text{zero defect of }rho)^2 + 4,text{zero defect of }rho$, where the zero defect is the Recognition Science defect of the deviation of $rho$ from the critical line and the doubled defect is obtained by applying the $J$-log to twice that deviation.
background
The Vector C Symmetry-Only No-Go module shows that reflection and conjugation symmetries on a completed $xi$-surface yield zero pairings but do not force the critical line; an explicit toy surface with zeros at Re$(s)=1/4,3/4$ realizes the package. A CompletedXiSurface consists of a function $xi:mathbb{C}to mathbb{C}$ obeying $xi(1-s)=xi(s)$ and $xi(overline{s})=overline{xi(s)}$ for all $s$. Functional reflection of $rho$ is $1-rho$, critical reflection is $1-overline{rho}$, zeroDefect$(rho)$ is the RS defect attached to the zero-location deviation, and doubledZeroDefect$(rho)$ is the $J$-log of twice the deviation. The upstream CompletedXiSurface doc states: Minimal completed-$xi$ symmetry data for Vector C. reflection is the completed functional equation, and conjugation is the standard reality symmetry. Any stronger zero-location constraint must be added on top of this surface; it is not present here by default.
proof idea
This is a structure definition that directly assembles the four zero conditions implied by the reflection and conjugation axioms of CompletedXiSurface together with the recurrence relation for the doubled defect supplied by the ZeroDoublingLaw.
why it matters
PureVectorCDoublingData supplies the hypothesis for the no-go results pureVectorCDoublingData_not_enough_for_critical_line and pureVectorCDoublingData_requires_extra_input, which exhibit an off-critical toy zero satisfying the package and conclude that extra analytic input from the Euler or Hadamard side is required to reach a ZeroCompositionWitness. It marks the boundary of what T5 J-uniqueness and the Recognition Composition Law can extract without additional structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.