pureVectorCDoublingData_offline_example

formal source

 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⟩
 145  exact hline (zeroCompositionWitness_forces_on_critical_line w)
 146
 147/-- In particular, pure FE symmetry plus the current doubling law do not by
 148themselves force the critical line. -/
 149theorem pureVectorCDoublingData_not_enough_for_critical_line :
 150    ¬ (∀ (Ξ : CompletedXiSurface) (ρ : ℂ),
 151        PureVectorCDoublingData Ξ ρ → OnCriticalLine ρ) := by
 152  intro h
 153  obtain ⟨Ξ, ρ, hpure, hline⟩ := pureVectorCDoublingData_offline_example