feat(rh-dlvp): obligation (i-a) CAPSTONE — ζ'/ζ = Herglotz zero-sum + entire part

[DrMurphyIsIn]

Summary

Closes obligation (i-a) of the de la Vallée Poussin zero-free-region frontier for the Riemann ζ, kernel-verified.

The new capstone DlvpZetaSplit.zeta_logDeriv_split assembles the full split for the actual ζ on a disk about c (Re c > 1) avoiding s = 1:

logDeriv ζ z = Σ_ρ (divisor ζ ρ)/(z − ρ) + logDeriv g z    ( = Z + E )

with g analytic and zero-free. It ties together the previously-landed pieces:

• zeta_extract_zeros_poles — the ζ canonical factorization (codiscrete);
• zeta_finprod_analyticOnNhd (new, piece A) — the zero-part finprod is analytic (divisor ζ ≥ 0 since ζ has no poles on the disk);
• logDeriv_congr_of_codiscrete — codiscrete equality of analytic functions ⟹ pointwise log-derivative equality (transferred to the open ball via codiscreteWithin_mono);
• herglotz_split_finprod — logDeriv of the factored form = Herglotz sum + logDeriv g.

What's left

The sole remaining analytic step is (i-b') the Borel–Carathéodory bound ‖E‖ = ‖logDeriv g‖ ≤ A·L on the entire part. With it, the split feeds the hzero/htwo inputs and the whole region follows through the already-kernel-clean reduction skeleton; optimizing σ = 1 + c/L → β ≤ 1 − c/log|t| is the final real-algebra step.

Verification

• New module DlvpZetaSplit.lean builds kernel-clean (lake build DlvpZetaSplit, no sorry, no extra axioms).
• New CI job rh-dlvp-zetasplit.
• 10-module kernel-clean chain; obligation (i) closed.

conjecture1_proved = False — this is a rigorous reduction, not a proof of RH.

🤖 Generated with Claude Code

https://claude.ai/code/session_01NzN1Gt4Fqo9uKNst5zhred