pureVectorCDoublingData_of_zero
plain-language theorem explainer
Any zero of a completed-ξ surface satisfies the pure Vector C doubling data, including pairings under functional reflection, conjugation, and critical reflection together with the quadratic defect recurrence. Researchers examining the Vector C symmetry stage gate cite this to separate what follows from reflection and conjugation alone from stronger location claims. The proof constructs the data structure in one step by supplying the zero hypothesis and invoking three pairing lemmas plus the recurrence definition.
Claim. Let Ξ be a completed-ξ surface and ρ ∈ ℂ with Ξ(ρ) = 0. Then Ξ(1 − ρ) = 0, Ξ(conjugate ρ) = 0, Ξ(critical reflection of ρ) = 0, and the doubled zero defect obeys doubledZeroDefect(ρ) = 2 (zeroDefect(ρ))² + 4 zeroDefect(ρ).
background
A CompletedXiSurface consists of a function xi : ℂ → ℂ equipped with the functional-equation reflection xi(1 − s) = xi(s) and the reality symmetry xi(conjugate s) = conjugate (xi s). PureVectorCDoublingData Ξ ρ is the structure asserting that ρ is a zero of Ξ, that the functional reflection, conjugate, and critical reflection of ρ are also zeros, and that the defect satisfies the quadratic recurrence doubledZeroDefect(ρ) = 2 (zeroDefect(ρ))² + 4 zeroDefect(ρ) derived from the functional equation and recognition composition law.
proof idea
The proof is a term-mode structure construction. It places the hypothesis hρ into the zero field, then applies zero_pairing_under_reflection, zero_pairing_under_conjugation, and zero_pairing_under_critical_reflection to obtain the three pairing fields, and inserts doubledZeroDefect_recurrence ρ for the recurrence field.
why it matters
This result supplies the pure Vector C package to every actual zero and is invoked directly by pureVectorCDoublingData_offline_example to realize the package on an off-critical toy zero. It completes the symmetry-only stage gate in the Vector C development, confirming that reflection and conjugation symmetries produce pairings and the doubling recurrence but do not force the critical line. The module states that these symmetries give pairing data on zeros but do not by themselves force the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.