IndisputableMonolith.NumberTheory.EulerLedgerPartition

   1import Mathlib
   2import Mathlib.NumberTheory.EulerProduct.DirichletLSeries
   3import IndisputableMonolith.NumberTheory.PrimeLedgerAtom
   4
   5/-!
   6# Euler Ledger Partition
   7
   8This module packages the Euler product as the partition function of independent
   9prime-ledger postings.
  10
  11The finite product statements are proved directly.  The infinite equality with
  12`riemannZeta` is isolated in `EulerLedgerPartitionCert`, because the exact
  13Mathlib Euler-product API is an analytic import boundary rather than RS
  14structure.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NumberTheory
  19
  20open scoped Topology
  21
  22noncomputable section
  23
  24/-- One prime posting weighted at complex scale `s`. -/
  25def primePostingWeight (s : ℂ) (p : ℕ) : ℂ :=
  26  (p : ℂ) ^ (-s)
  27
  28/-- Local geometric partition attached to one prime ledger atom. -/
  29def primeLedgerLocalPartition (s : ℂ) (p : ℕ) : ℂ :=
  30  (1 - primePostingWeight s p)⁻¹
  31
  32/-- A finite prime-ledger partition over a finite set of primes. -/
  33def finitePrimeLedgerPartition (s : ℂ) (S : Finset ℕ) : ℂ :=
  34  ∏ p ∈ S, if Nat.Prime p then primeLedgerLocalPartition s p else 1
  35
  36/-- Finite prime-ledger partition is insensitive to non-prime entries. -/
  37theorem finitePrimeLedgerPartition_insert_nonprime
  38    (s : ℂ) (S : Finset ℕ) {n : ℕ} (hnS : n ∉ S) (hn : ¬ Nat.Prime n) :
  39    finitePrimeLedgerPartition s (insert n S) = finitePrimeLedgerPartition s S := by
  40  unfold finitePrimeLedgerPartition
  41  simp [hnS, hn]
  42
  43/-- Inserting a new prime multiplies the partition by its local factor. -/
  44theorem finitePrimeLedgerPartition_insert_prime
  45    (s : ℂ) (S : Finset ℕ) {p : ℕ} (hpS : p ∉ S) (hp : Nat.Prime p) :
  46    finitePrimeLedgerPartition s (insert p S) =
  47      primeLedgerLocalPartition s p * finitePrimeLedgerPartition s S := by
  48  unfold finitePrimeLedgerPartition
  49  simp [hpS, hp]
  50
  51/-- The Euler ledger partition as a formal infinite product over prime atoms. -/
  52def PrimeLedgerPartition (s : ℂ) : Prop :=
  53  ∃ F : (Finset ℕ → ℂ), ∀ S, F S = finitePrimeLedgerPartition s S
  54
  55/-- The formal partition exists, by finite partial products. -/
  56theorem primeLedgerPartition_formal (s : ℂ) : PrimeLedgerPartition s :=
  57  ⟨fun S => finitePrimeLedgerPartition s S, fun _ => rfl⟩
  58
  59/-- Analytic certificate connecting the formal prime-ledger partition to zeta
  60on a convergence domain. -/
  61structure EulerLedgerPartitionCert where
  62  /-- Euler product agrees with `riemannZeta` for `Re(s) > 1`, expressed as
  63  convergence of finite prime-ledger partitions. -/
  64  eulerProduct_eq_zeta :
  65    ∀ s : ℂ, 1 < s.re →
  66      Filter.Tendsto (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n))
  67        Filter.atTop (𝓝 (riemannZeta s))
  68  /-- The formal prime-ledger partition exists at every complex scale. -/
  69  formal_partition : ∀ s : ℂ, PrimeLedgerPartition s
  70  /-- Primes are exactly the ledger atoms. -/
  71  prime_atoms : PrimeLedgerCert
  72
  73/-- The structural Euler ledger certificate.  The analytic equality field now
  74uses Mathlib's Euler-product theorem for `riemannZeta` on `Re(s) > 1`; the
  75finite products are exactly the finite prime-ledger partitions. -/
  76def eulerLedgerPartitionCert : EulerLedgerPartitionCert where
  77  eulerProduct_eq_zeta := by
  78    intro s hs
  79    have hmathlib :
  80        Filter.Tendsto (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹)
  81          Filter.atTop (𝓝 (riemannZeta s)) :=
  82      _root_.riemannZeta_eulerProduct hs
  83    have hpart : (fun n : ℕ ↦ finitePrimeLedgerPartition s (Nat.primesBelow n)) =
  84        (fun n : ℕ ↦ ∏ p ∈ Nat.primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹) := by
  85      funext n
  86      unfold finitePrimeLedgerPartition primeLedgerLocalPartition primePostingWeight
  87      apply Finset.prod_congr rfl
  88      intro p hp
  89      have hprime : Nat.Prime p := (Nat.mem_primesBelow.mp hp).2
  90      simp [hprime]
  91    simpa [hpart] using hmathlib
  92  formal_partition := primeLedgerPartition_formal
  93  prime_atoms := primeLedgerCert
  94
  95end
  96
  97end NumberTheory
  98end IndisputableMonolith
  99