BalancedArithmeticLedger

formal source

  12
  13/-- A balanced arithmetic ledger is invariant under the reciprocal coordinate
  14`s ↦ 1 - s`; its fixed locus is the critical line. -/
  15structure BalancedArithmeticLedger (F : ℂ → ℂ) : Prop where
  16  reciprocal_symmetry : ∀ s : ℂ, F (1 - s) = F s
  17  balance_line_fixed : ∀ s : ℂ, s = 1 - s → s.re = 1 / 2
  18
  19/-- The fixed locus of `s ↦ 1 - s` has real part `1/2`. -/
  20theorem reciprocal_fixed_re_eq_half {s : ℂ} (hs : s = 1 - s) :
  21    s.re = 1 / 2 := by
  22  have hre := congrArg Complex.re hs
  23  simp [Complex.sub_re, Complex.one_re] at hre
  24  linarith
  25
  26/-- The completed zeta function is reciprocal-balanced. -/
  27theorem completedZeta_balanced :
  28    BalancedArithmeticLedger completedRiemannZeta where
  29  reciprocal_symmetry := by
  30    intro s
  31    rw [completedRiemannZeta_one_sub]
  32  balance_line_fixed := by
  33    intro s hs
  34    exact reciprocal_fixed_re_eq_half hs
  35
  36/-- Certificate for the completed-zeta ledger bridge. -/
  37structure CompletedZetaLedgerCert where
  38  balanced : BalancedArithmeticLedger completedRiemannZeta
  39  critical_line_unique : ∀ s : ℂ, s = 1 - s → s.re = 1 / 2
  40
  41/-- Completed zeta ledger certificate. -/
  42def completedZetaLedgerCert : CompletedZetaLedgerCert where
  43  balanced := completedZeta_balanced
  44  critical_line_unique := fun _ hs => reciprocal_fixed_re_eq_half hs
  45