IndisputableMonolith.NumberTheory.ZeroDoublingLaw

   1import Mathlib
   2import IndisputableMonolith.Foundation.DiscretenessForcing
   3import IndisputableMonolith.NumberTheory.ZeroLocationCost
   4import IndisputableMonolith.NumberTheory.XiJBridge
   5
   6/-!
   7# Zero Doubling Law
   8
   9This file records the strongest concrete Vector C instantiation currently
  10obtained from the functional-equation/J-symmetry bridge:
  11
  12the defect observable satisfies a **doubling recurrence**
  13
  14`D(2t) = 2 * D(t)^2 + 4 * D(t)`.
  15
  16This is substantial evidence that FE symmetry interacts nontrivially with the
  17RS defect, but it is still weaker than the full d'Alembert interface packaged in
  18`ZeroCompositionInterface.lean`.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace NumberTheory
  23
  24noncomputable section
  25
  26/-- The defect obtained by doubling the zero deviation. This is the virtual
  27next-step observable suggested by FE reflection plus RCL self-composition. -/
  28def doubledZeroDefect (ρ : ℂ) : ℝ :=
  29  Foundation.DiscretenessForcing.J_log (2 * zeroDeviation ρ)
  30
  31/-- Closed form for the doubled zero defect. -/
  32theorem doubledZeroDefect_eq_cosh_sub_one (ρ : ℂ) :
  33    doubledZeroDefect ρ = Real.cosh (2 * zeroDeviation ρ) - 1 := by
  34  simp [doubledZeroDefect, Foundation.DiscretenessForcing.J_log]
  35
  36/-- The FE/RCL bridge yields a doubling recurrence on the zero defect.
  37
  38This is the concrete Phase 4 instantiation currently available: a one-step
  39self-composition law on doubled deviation. -/
  40theorem doubledZeroDefect_recurrence (ρ : ℂ) :
  41    doubledZeroDefect ρ = 2 * (zeroDefect ρ) ^ 2 + 4 * zeroDefect ρ := by
  42  rw [doubledZeroDefect_eq_cosh_sub_one, zeroDefect_eq_cosh_sub_one]
  43  rw [Real.cosh_two_mul]
  44  nlinarith [Real.cosh_sq (zeroDeviation ρ)]
  45
  46/-- The doubled zero defect is always nonnegative. -/
  47theorem doubledZeroDefect_nonneg (ρ : ℂ) : 0 ≤ doubledZeroDefect ρ := by
  48  rw [doubledZeroDefect_eq_cosh_sub_one]
  49  linarith [Real.one_le_cosh (2 * zeroDeviation ρ)]
  50
  51/-- Doubling the deviation still vanishes exactly on the critical line. -/
  52theorem doubledZeroDefect_zero_iff_on_critical_line (ρ : ℂ) :
  53    doubledZeroDefect ρ = 0 ↔ OnCriticalLine ρ := by
  54  rw [doubledZeroDefect_eq_cosh_sub_one]
  55  constructor
  56  · intro h
  57    have hz : 2 * zeroDeviation ρ = 0 := by
  58      by_contra hne
  59      have hgt : 1 < Real.cosh (2 * zeroDeviation ρ) := Real.one_lt_cosh.mpr hne
  60      linarith
  61    have hdev : zeroDeviation ρ = 0 := by linarith
  62    exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).mp hdev
  63  · intro h
  64    have hdev : zeroDeviation ρ = 0 :=
  65      (zeroDeviation_eq_zero_iff_on_critical_line ρ).mpr h
  66    simp [hdev]
  67
  68/-- Packaging of the strongest currently instantiated Vector C data. -/
  69theorem current_vectorC_attempt_data (ρ : ℂ) :
  70    (zeroDefect ρ = 0 ↔ OnCriticalLine ρ) ∧
  71      0 ≤ doubledZeroDefect ρ ∧
  72      doubledZeroDefect ρ = 2 * (zeroDefect ρ) ^ 2 + 4 * zeroDefect ρ := by
  73  exact ⟨zeroDefect_zero_iff_on_critical_line ρ, doubledZeroDefect_nonneg ρ,
  74    doubledZeroDefect_recurrence ρ⟩
  75
  76end
  77
  78end NumberTheory
  79end IndisputableMonolith
  80