pureVectorCDoublingData_of_zero

formal source

 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
 135`ZeroCompositionWitness` must use genuinely extra analytic input not present in
 136the pure FE package; in this repository the natural candidates live on the
 137Euler/Hadamard side (`QuantitativeLocalFactorization`,
 138`phaseIncrementEpsilonBound`, perturbation/budget control). -/
 139theorem pureVectorCDoublingData_requires_extra_input :
 140    ¬ (∀ (Ξ : CompletedXiSurface) (ρ : ℂ),
 141        PureVectorCDoublingData Ξ ρ → Nonempty (ZeroCompositionWitness ρ)) := by
 142  intro h
 143  obtain ⟨Ξ, ρ, hpure, hline⟩ := pureVectorCDoublingData_offline_example
 144  rcases h Ξ ρ hpure with ⟨w⟩