IndisputableMonolith.NumberTheory.Port

   1/-
   2# Number Theory Ports
   3
   4This module imports all theorems ported from the riemann repositories:
   5- github.com/jonwashburn/riemann (riemann-main)
   6- github.com/jonwashburn/riemann (riemann-geometry-rs)
   7
   8## Ported Results
   9
  10### From BrunTitchmarsh.lean (riemann-main)
  11- `card_range_filter_prime_isBigO`: π(N) = O(N / log N)
  12- `prime_counting_explicit_bound`: π(N) ≤ 4N/log N + O(√N log³ N)
  13- Asymptotic helper lemmas
  14
  15### From PNT files (riemann-main)
  16- `WeakPNT`: ∑Λ(n)/N → 1
  17- `MediumPNT`: ψ(x) = x + O(x exp(-c (log x)^{1/10}))
  18- `prime_counting_asymptotic`: π(x) ~ x/log x
  19
  20### From RiemannRecognitionGeometry (riemann-geometry-rs)
  21- `completedRiemannZeta_ne_zero_of_re_gt_one`: ξ(s) ≠ 0 for Re > 1
  22- `zero_in_critical_strip`: ξ-zeros have 0 < Re < 1
  23- `RiemannHypothesis_conditional`: Conditional RH proof structure
  24
  25## Usage
  26
  27```lean
  28import IndisputableMonolith.NumberTheory.Port
  29
  30open IndisputableMonolith.NumberTheory.Port.BrunTitchmarsh
  31open IndisputableMonolith.NumberTheory.Port.PNT
  32open IndisputableMonolith.NumberTheory.Port.RiemannHypothesis
  33```
  34
  35## Notes
  36
  37These ports contain `sorry` placeholders because:
  381. The source repositories use Lean 4.25.0-rc2 (vs 4.27.0-rc1 here)
  392. Some proofs depend on custom Mathlib extensions in the source repos
  403. Full proofs are available in the original repositories
  41
  42The sorries document mathematically verified results that are proven elsewhere.
  43-/
  44
  45import IndisputableMonolith.NumberTheory.Port.BrunTitchmarsh
  46import IndisputableMonolith.NumberTheory.Port.PNT
  47import IndisputableMonolith.NumberTheory.Port.RiemannHypothesis
  48