IndisputableMonolith.NumberTheory.VectorCSymmetryOnlyNoGo

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.CompletedXiSymmetry
   3import IndisputableMonolith.NumberTheory.ZeroDoublingLaw
   4import IndisputableMonolith.NumberTheory.ZeroCompositionInterface
   5
   6/-!
   7# Vector C Symmetry-Only No-Go
   8
   9This module formalizes the main stage gate for Vector C:
  10
  11functional-equation reflection symmetry plus conjugation symmetry give
  12pairing data on zeros, but do not by themselves force the critical line.
  13
  14We certify this with an explicit toy completed-ξ surface whose zeros occur on
  15the off-line pair `Re(s) = 1/4, 3/4`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace NumberTheory
  20
  21open scoped ComplexConjugate
  22
  23noncomputable section
  24
  25/-- A toy completed-ξ-style function depending only on the real part.
  26
  27Its zero set is exactly the union of the two vertical lines `Re(s) = 1/4` and
  28`Re(s) = 3/4`, so it satisfies reflection and conjugation symmetry while still
  29admitting off-critical-line zeros. -/
  30def toyXi (s : ℂ) : ℂ :=
  31  Complex.ofReal (((s.re - 3 / 4) ^ 2) * ((s.re - 1 / 4) ^ 2))
  32
  33theorem toyXi_reflection (s : ℂ) :
  34    toyXi (functionalReflection s) = toyXi s := by
  35  simp [toyXi, functionalReflection]
  36  ring
  37
  38theorem toyXi_conjugation (s : ℂ) :
  39    toyXi (conj s) = conj (toyXi s) := by
  40  unfold toyXi
  41  rw [Complex.conj_ofReal]
  42  have hre : (conj s).re = s.re := by simp
  43  rw [hre]
  44
  45/-- A concrete symmetry surface showing that FE-style pairing data alone does
  46not force critical-line support. -/
  47def toyCompletedXiSurface : CompletedXiSurface where
  48  xi := toyXi
  49  reflection := toyXi_reflection
  50  conjugation := toyXi_conjugation
  51
  52/-- The toy surface has a zero at `s = 3/4`. -/
  53theorem toyCompletedXiSurface_has_off_critical_zero :
  54    toyCompletedXiSurface.xi (3 / 4 : ℂ) = 0 ∧
  55      ¬ OnCriticalLine (3 / 4 : ℂ) := by
  56  constructor
  57  · norm_num [toyCompletedXiSurface, toyXi]
  58  · norm_num [OnCriticalLine]
  59
  60/-- Reflection/conjugation symmetry of the completed-ξ surface alone is
  61insufficient to force the critical line. -/
  62theorem completedXiSurface_symmetry_only_no_go :
  63    ¬ (∀ Ξ : CompletedXiSurface, ∀ s : ℂ, Ξ.xi s = 0 → OnCriticalLine s) := by
  64  intro h
  65  obtain ⟨hzero, hline⟩ := toyCompletedXiSurface_has_off_critical_zero
  66  exact hline (h toyCompletedXiSurface (3 / 4 : ℂ) hzero)
  67
  68/-- The negation-closed deviation-set property obtained from the functional
  69equation does not force `0` to be the only realized deviation. -/
  70theorem zeroDeviationSet_neg_closed_not_enough :
  71    ∃ Ξ : CompletedXiSurface,
  72      (1 / 2 : ℝ) ∈ zeroDeviationSet Ξ ∧
  73      (-1 / 2 : ℝ) ∈ zeroDeviationSet Ξ ∧
  74      0 ∉ zeroDeviationSet Ξ := by
  75  refine ⟨toyCompletedXiSurface, ?_, ?_, ?_⟩
  76  · refine ⟨(3 / 4 : ℂ), ?_, ?_⟩
  77    · exact toyCompletedXiSurface_has_off_critical_zero.1
  78    · norm_num [zeroDeviation]
  79  · have hhalf : (1 / 2 : ℝ) ∈ zeroDeviationSet toyCompletedXiSurface := by
  80      refine ⟨(3 / 4 : ℂ), ?_, ?_⟩
  81      · exact toyCompletedXiSurface_has_off_critical_zero.1
  82      · norm_num [zeroDeviation]
  83    have hneg : (-(1 / 2 : ℝ)) ∈ zeroDeviationSet toyCompletedXiSurface :=
  84      zeroDeviationSet_neg_closed toyCompletedXiSurface hhalf
  85    norm_num at hneg ⊢
  86    exact hneg
  87  · intro hzero
  88    rcases hzero with ⟨s, hs, hdev⟩
  89    have hline : OnCriticalLine s :=
  90      (zeroDeviation_eq_zero_iff_on_critical_line s).mp hdev
  91    have hvalue :
  92        toyCompletedXiSurface.xi s =
  93          (((1 / 2 - 3 / 4) ^ 2 * (1 / 2 - 1 / 4) ^ 2 : ℝ) : ℂ) := by
  94      simp [toyCompletedXiSurface, toyXi, show s.re = 1 / 2 by exact hline]
  95    have hnonzero :
  96        ((((1 / 2 - 3 / 4) ^ 2 * (1 / 2 - 1 / 4) ^ 2 : ℝ) : ℂ)) ≠ 0 := by
  97      norm_num
  98    have hxine : toyCompletedXiSurface.xi s ≠ 0 := by
  99      simpa [hvalue] using hnonzero
 100    exact hxine hs
 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
 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
 154  exact hline (h Ξ ρ hpure)
 155
 156end
 157
 158end NumberTheory
 159end IndisputableMonolith
 160