Request build/review - boundary-product-route

Stream: new members

[Jonathan Washburn]

Hi all — I’d appreciate help spotting anything I’m missing.

Repo (tagged release): riemann-hypothesis v1.0.1-annals

Repro:

• git clone https://github.com/jonwashburn/riemann-hypothesis
• cd riemann-hypothesis
• git checkout v1.0.1-annals
• lake update && lake build
• bash scripts/verify.sh
• bash scripts/print-keys.sh

Scope/claims:

• Only the rh/ tree builds. Pinned toolchain via lean-toolchain.
• No new axioms, no sorries.
• Named theorems compile: RH, no_offcritical_zeros_from_schur, ZetaNoZerosOnRe1FromSchur, zeta_nonzero_re_eq_one (delegate). Feedback welcome on the new off‑zeros wrapper ZetaNoZerosOnRe1_from_offZerosAssignmentStatement.

Notes on (P+) handoff:

• (P+) is via a statement‑level interface: a Prop‑level KxiBound gives Kξ ≥ 0, an adapter exposes Cζ := K0 + Kξ, and PPlusFromCarleson_exists F yields (P+). I’d value feedback on whether this interface shape is reasonable and how to strengthen it with mathlib‑level lemmas.

What I’m asking for:

• Independent build verification (including “no axioms/sorries”).
• Feedback on module/API structure, naming, and acceptability of the statement‑level interfaces.
• Suggestions on splitting out neutral pieces suitable for mathlib.

Thanks — happy to iterate on structure/lints/docs.

[Ruben Van de Velde]

What do you claim to have proved, in simple prose?

[Jonathan Washburn]

Hi Ruben,

Well with this post I'm looking to make sure I'm not missing anything obvious in the build, or structure, and generally any advice anyone has.

[Robin Arnez]

If you allow me to look into "quarantined" files, then there are tons of errors regarding lemmas that are written there but never existed in mathlib, such as

lemma norm_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (s : ℂ) : ‖z ^ s‖ = ‖z‖ ^ s.re := by
  exact Complex.abs_cpow_eq_rpow_re_of_ne_zero hz s

(which is false btw!)

lemma not_norm_cpow_of_ne_zero : ¬ ∀ {z : ℂ} (_hz : z ≠ 0) (s : ℂ), ‖z ^ s‖ = ‖z‖ ^ s.re := by
  push_neg
  use I, by simp, I
  simp only [ne_eq, I_ne_zero, not_false_eq_true, cpow_def_of_ne_zero, log_I, mul_assoc, I_mul_I,
    mul_neg, mul_one, Complex.norm_eq_abs, abs_I, I_re, rpow_zero]
  norm_cast
  simp only [Real.abs_exp, Real.exp_eq_one_iff, neg_eq_zero, div_eq_zero_iff, pi_ne_zero,
    OfNat.ofNat_ne_zero, or_self, not_false_eq_true]

Otherwise Axioms.lean doesn't compile because it's invalid syntax.
Then there is this theorem RH which is really mathematical trivial but you can't instantiate it with the riemann zeta function because of the lack of such symmetry (e.g. riemann zeta function at -2 is 0 and at 3 = 1 - (-2) it is 1.2020569).
Also what is this supposed to be?

/-- Entry point availability placeholder for the final assembly theorem (interface). -/
def main_outline_available : Prop := True

Another thing is that there are tons of warnings; these should be easy to fix. I'm slightly skeptical of the assumptions of the other statements but I can't really tell whether that is reasonable.

[Jonathan Washburn]

I really appreciate you looking into it!

I'm deleting the quarantined files, and working on finalizing the final proof theorem now.