pureVectorCDoublingData_of_zero
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.
claimLet Ξ 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 in Recognition Science
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.
scope and limits
- Does not prove that zeros lie on the critical line.
- Does not assume the Riemann hypothesis or any stronger zero-location axiom.
- Does not derive dimension or forcing-chain steps beyond T5 symmetry.
- Does not address the full eight-tick octave or D = 3 construction.
Lean usage
exact pureVectorCDoublingData_of_zero toyCompletedXiSurface toyCompletedXiSurface_has_off_critical_zero.1formal statement (Lean)
114theorem pureVectorCDoublingData_of_zero (Ξ : CompletedXiSurface) {ρ : ℂ}
115 (hρ : Ξ.xi ρ = 0) :
116 PureVectorCDoublingData Ξ ρ := by
proof body
Term-mode proof.
117 refine ⟨hρ, ?_, ?_, ?_, doubledZeroDefect_recurrence ρ⟩
118 · exact zero_pairing_under_reflection Ξ hρ
119 · exact zero_pairing_under_conjugation Ξ hρ
120 · exact zero_pairing_under_critical_reflection Ξ hρ
121
122/-- The current pure Vector C package is realized by an off-critical toy zero. -/