IndisputableMonolith.Foundation.LogicComplexCompat

   1import IndisputableMonolith.Foundation.ComplexFromLogic
   2import IndisputableMonolith.NumberTheory.EulerProductEqualsZeta
   3import IndisputableMonolith.NumberTheory.CompletedZetaLedger
   4
   5/-!
   6  LogicComplexCompat.lean
   7
   8  Compatibility layer between recovered complex numbers and Mathlib's analytic
   9  complex substrate.
  10
  11  Phase 2 decision: we do not redefine holomorphy, contour integration, or the
  12  Riemann zeta function on a separate complex analysis stack.  We use Mathlib
  13  `ℂ` as the analytic substrate, and this module makes that use explicit:
  14  every recovered-complex statement is transported through
  15  `LogicComplex.toComplex`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace LogicComplexCompat
  21
  22open ComplexFromLogic
  23open ComplexFromLogic.LogicComplex
  24open Filter Topology
  25
  26noncomputable section
  27
  28/-- The Riemann zeta function read on recovered complex inputs. -/
  29def logicRiemannZeta (s : LogicComplex) : ℂ :=
  30  riemannZeta (toComplex s)
  31
  32/-- The completed zeta function read on recovered complex inputs. -/
  33def logicCompletedRiemannZeta (s : LogicComplex) : ℂ :=
  34  completedRiemannZeta (toComplex s)
  35
  36@[simp] theorem logicRiemannZeta_fromComplex (s : ℂ) :
  37    logicRiemannZeta (fromComplex s) = riemannZeta s := by
  38  simp [logicRiemannZeta]
  39
  40@[simp] theorem logicCompletedRiemannZeta_fromComplex (s : ℂ) :
  41    logicCompletedRiemannZeta (fromComplex s) = completedRiemannZeta s := by
  42  simp [logicCompletedRiemannZeta]
  43
  44/-- Recovered-complex real part agrees with the real part after transport. -/
  45theorem toComplex_re_eq (s : LogicComplex) :
  46    (toComplex s).re = RealsFromLogic.LogicReal.toReal s.re := rfl
  47
  48/-- The Euler product theorem, read on recovered complex inputs. -/
  49theorem logicRiemannZeta_eulerProduct_tendsto
  50    (s : LogicComplex) (hs : 1 < (toComplex s).re) :
  51    Tendsto (fun n : ℕ ↦
  52        NumberTheory.finitePrimeLedgerPartition (toComplex s) (Nat.primesBelow n))
  53      atTop (𝓝 (logicRiemannZeta s)) := by
  54  simpa [logicRiemannZeta] using
  55    NumberTheory.EulerProductEqualsZeta.ledger_partition_equals_zeta
  56      (toComplex s) hs
  57
  58/-- Completed zeta satisfies the functional equation on recovered complex
  59inputs, by transport to Mathlib's `completedRiemannZeta`. -/
  60theorem logicCompletedRiemannZeta_one_sub (s : LogicComplex) :
  61    logicCompletedRiemannZeta (fromComplex (1 - toComplex s)) =
  62      logicCompletedRiemannZeta s := by
  63  simp [logicCompletedRiemannZeta, completedRiemannZeta_one_sub]
  64
  65/-- Certificate that all analytic zeta operations are performed in Mathlib `ℂ`
  66through the recovered-complex equivalence. -/
  67structure LogicComplexAnalyticSubstrateCert where
  68  carrier_equiv : LogicComplex ≃ ℂ
  69  zeta_transport : ∀ s : LogicComplex,
  70    logicRiemannZeta s = riemannZeta (toComplex s)
  71  completed_zeta_transport : ∀ s : LogicComplex,
  72    logicCompletedRiemannZeta s = completedRiemannZeta (toComplex s)
  73  euler_product :
  74    ∀ s : LogicComplex, 1 < (toComplex s).re →
  75      Tendsto (fun n : ℕ ↦
  76        NumberTheory.finitePrimeLedgerPartition (toComplex s) (Nat.primesBelow n))
  77        atTop (𝓝 (logicRiemannZeta s))
  78  completed_functional_equation :
  79    ∀ s : LogicComplex,
  80      logicCompletedRiemannZeta (fromComplex (1 - toComplex s)) =
  81        logicCompletedRiemannZeta s
  82
  83/-- The analytic substrate compatibility certificate for Phase 2. -/
  84def logicComplexAnalyticSubstrateCert : LogicComplexAnalyticSubstrateCert where
  85  carrier_equiv := equivComplex
  86  zeta_transport := fun _ => rfl
  87  completed_zeta_transport := fun _ => rfl
  88  euler_product := logicRiemannZeta_eulerProduct_tendsto
  89  completed_functional_equation := logicCompletedRiemannZeta_one_sub
  90
  91end
  92
  93end LogicComplexCompat
  94end Foundation
  95end IndisputableMonolith
  96