PureVectorCDoublingData

formal source

 101
 102/-- The strongest concrete Vector C data currently available from pure
 103completed-ξ symmetry plus the FE/RCL doubling law. -/
 104structure PureVectorCDoublingData (Ξ : CompletedXiSurface) (ρ : ℂ) : Prop where
 105  zero : Ξ.xi ρ = 0
 106  reflection_zero : Ξ.xi (functionalReflection ρ) = 0
 107  conjugation_zero : Ξ.xi (conj ρ) = 0
 108  critical_reflection_zero : Ξ.xi (criticalReflection ρ) = 0
 109  doubled_recurrence :
 110    doubledZeroDefect ρ = 2 * (zeroDefect ρ) ^ 2 + 4 * zeroDefect ρ
 111
 112/-- Any actual completed-ξ zero carries the current pure Vector C package:
 113pairing invariants plus the FE/RCL doubling recurrence. -/
 114theorem pureVectorCDoublingData_of_zero (Ξ : CompletedXiSurface) {ρ : ℂ}
 115    (hρ : Ξ.xi ρ = 0) :
 116    PureVectorCDoublingData Ξ ρ := by
 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. -/
 123theorem pureVectorCDoublingData_offline_example :
 124    ∃ Ξ : CompletedXiSurface, ∃ ρ : ℂ,
 125      PureVectorCDoublingData Ξ ρ ∧ ¬ OnCriticalLine ρ := by
 126  refine ⟨toyCompletedXiSurface, (3 / 4 : ℂ), ?_, ?_⟩
 127  · exact pureVectorCDoublingData_of_zero toyCompletedXiSurface
 128      toyCompletedXiSurface_has_off_critical_zero.1
 129  · exact toyCompletedXiSurface_has_off_critical_zero.2
 130
 131/-- Even after adding the current FE/RCL doubling law, pure completed-ξ
 132symmetry data still cannot force a `ZeroCompositionWitness`.
 133
 134Therefore any successful upgrade from honest zeta-derived phase data to