Kernel-checked Hermite–Biehler theorems for shifted Riemann ξ, with disk localization

Let Ξ(z)=ξ(1/2+iz) and, for h>0, E_h(z)=Ξ(z+ih), E_h^#(z)=Ξ(z-ih). We give a Lean 4 formalization of Hermite–Biehler modulus inequalities, phase monotonicity, and simple interlacing zeros for the combinations S_θ=A_h cos θ+B_h sin θ of these imaginary translates, where A_h=(E_h+E_h^#)/2 and B_h=i(E_h-E_h^#)/2. The development is built on a formal Hadamard factorization of ξ and proceeds through an abstract theorem for convergent products of conjugate-pair and quartet factors. Unconditionally, every non-real zero of every S_θ lies in a union of closed disks |z-Re γ|^2≤(Im γ)^2-h^2 determined by the non-real zeros γ of Ξ; this extends de Bruijn's disk theorem for real polynomials to Ξ, and the disk radius is sharp, including for a non-degenerate quartet. This yields global Hermite–Biehler structure for h≥1/2, and, under an explicit verified-height hypothesis, local real-rootedness, simplicity, interlacing, an exact phase-counting formula, upper bounds on zero gaps, and a local first Laguerre inequality for Ξ below that height. All final declarations depend only on the standard axioms of Lean. The global conclusions are classical; our contribution is their kernel-checked derivation, the extension of de Bruijn's disk localization to Ξ with its finite-height consequences, and certified numerical examples at h=1/8 obtained separately with ball arithmetic. Contents of the release paper/ — the manuscript (LaTeX source and PDF), debranges_hb_gen.py, which reads every stated number from the certificate records, the Lean sources and the axiom report and writes debranges_hb_numbers.tex (--check fails on any typed decimal), and debranges_hb_runs/axioms.log, the build log with the axiom report of every final declaration. lean/ — the Lean 4 project (14 modules in lean/Debranges/, 2{, lines, 47 final declarations); it requires only PrimeNumberTheoremAnd at a pinned revision, which pins Lean and Mathlib. certificates/ — the ball-arithmetic scripts (python-flint/Arb) and their JSON records: zero isolation and winding counts up to height 240, shifted-zero isolation and interlacing brackets at h = 1/8, the c4 coefficients, the phase bounds, and the Gram-matrix scope example. These computations are not checked by Lean. REPLAY.md and replay/ — a clean replay from this bundle alone: 7 of 7 steps pass (Lean build with the axiom report, every certificate script rerun with identical records, numbers regenerated identically). SHA256SUMS — the SHA-256 of every file. Verification In lean/ (Lean via elan): lake exe cache get && lake build. Every #print axioms line in the build log must report only propext, Classical.choice, Quot.sound. In certificates/ (Python 3 with python-flint, mpmath and SymPy): python3 shifted_xi_kernel.py, python3 sweep.py out.json, python3 local_L1.py out.json, python3 local_L1_extra.py out.json; each exits 0 iff every certificate passes. In paper/: python3 debranges_hb_gen.py --check. Integrity: shasum -a 256 -c SHA256SUMS. Hardware One MacBook Pro (Apple M3 Pro, 11 CPU cores, 18 GB memory); no GPU, no cluster. License: Licensed by SmartLedger Solutions under CC BY-NC 4.0 (LICENSE.md). Commercial use requires a written license from SmartLedger Solutions ([email protected]). No patent license is granted.