# ERURH: A Conditional, Formalized Route to the Riemann Hypothesis through ERU framework
(AI-Assisted)

Robert Duran

► To cite this version:

Robert Duran. ERURH: A Conditional, Formalized Route to the Riemann Hypothesis through ERU framework (AI-Assisted). 2026. hal-05501445

HAL Id: hal-05501445

https://hal.science/hal-05501445v1

Preprint submitted on 9 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# ERURH: A Conditional, Formalized Route to the Riemann Hypothesis

Robert Duran

DOI (artefacts and reproducibility): https://doi.org/10.5281/zenodo.18010407

## Abstract

ERURH is presented here as a high-difficulty applied case study of the ERU framework. The Riemann Hypothesis for the ERURH completed function $\xi_\alpha$ is used as a stress-test to demonstrate a reduction to explicit analytic obligations and finite, auditable certificates. All conclusions are conditional on the external analytic inputs and certified data stated below. We present a precise conditional proof of the Riemann Hypothesis for the completed zeta-like function $\xi_\alpha$ used in the ERURH framework. The argument reduces RH to a finite set of auditable numerical certificates and a small collection of classical analytic assumptions about the Riemann zeta function and its explicit formula. The logical chain is fully formalized in Lean (Lean 4.25.0-rc2 + mathlib). This paper states the exact hypotheses, explains the ERU energy/inertia machinery, and gives a rigorous, end-to-end proof of the conditional theorem.

**Status / Scope.** This document is a logical reduction and an explanatory bridge between the Lean formal statement and external analytic hypotheses. It does not contain independent analytic proofs of the A/B/C estimates; those appear in Theorem_ABC_preprint.tex. Its purpose is to fix dependencies (ERURH_GlobalAssumptions $\Rightarrow$ RH for $\xi_\alpha$) and provide cross-references for audit. See docs/core/ERURH_Assumptions_Report.md and docs/core/ERURH_Analytic_Theorems_ABC.md for consolidated assumption summaries and A/B/C pointers. **Trust boundary note.** The Lean bundle AxiomsShimAccepted is the trust base (Lean kernel + mathlib axioms only). The window and normalization bridges are coverage/compatibility conditions audited structurally against the numeric certificates, not deep analytic conjectures.

## 1 Introduction

The ERURH program reformulates the Riemann Hypothesis (RH) in terms of a finite set of numerically checkable certificates. It is presented here as a high-difficulty applied case study of the ERU framework, using RH for $\xi_\alpha$ as a stress-test of the reduction-to-certificates paradigm. A brief system-level overview is provided in the accompanying repository documentation (docs/ERU_AT_A(GLANCE.md). The strategy is to translate the classical explicit formula for $\psi(x)$ into an "energy-inertia" framework on the logarithmic scale $s = \log x$, and then show that the absence of supercritical exponential modes (modes with real part > 1/2) forces the RH for a completed zeta-like function $\xi_\alpha$. The novel content is encapsulated in finite certificates; the classical analytic inputs are isolated as explicit assumptions. The entire logical chain is formalized in Lean.

**Main Claim (scope-exact).** ERURH provides a complete, formally verified (Lean) reduction of the Riemann Hypothesis for $\xi_\alpha$ to a finite and explicit set of external analytic statements (A/B/C and normalization bridges), together with a family of finite, reproducible numerical certificates
whose verification is mechanical. The repository includes a machine-checked proof of the conditional implication ERURH.GlobalAssumptions ⇒ RH(ξ_α), and a deterministic pipeline that regenerates and verifies all referenced numeric artifacts.

This paper is a rigorous, stand-alone description of the conditional proof at the level of the reduction and the Lean-verified logical chain. The analytic proofs of the classical inputs appear in the companion preprint Theorem. We make no unconditional claims; all analytic inputs are enumerated and treated as hypotheses. The main theorem mirrors the Lean theorem RH_from_ERURH_conditional.

## 2 Notation and ERU observables

Let ξ_α denote the completed zeta-like function used in the ERURH alpha layer. Its analytic properties (functional equation, explicit formula, and RH equivalences) are listed in Assumption 11.1.

Let $\psi(x) = \sum_{p^k \le x} \log p$ and $E(x) = \psi(x) - x$. Define

$$s = \log x, \quad \log R(s) = \frac{E(e^s)}{e^s}, \quad J_{\text{rel}}(s) = \frac{d}{ds} \log R(s). \qquad (1)$$

The explicit formula for $\psi(x)$ can be written on the s-scale in the form

$$\log R(s) = \sum_{\rho} a_{\rho} e^{(\rho-1)s} + \dots, \quad J_{\text{rel}}(s) = \sum_{\rho} \frac{\rho-1}{\rho} a_{\rho} e^{(\rho-1)s} + \dots, \qquad (2)$$

where $\rho = \beta + i\gamma$ ranges over non-trivial zeros of $\zeta(s)$ and $\dots$ denotes terms from trivial zeros and smooth test factors. We introduce abstract coefficients $b_{\rho}^{\text{Lean}}$ for the Lean formalization. For the analytic preprint (Theorems A/B/C) we use coefficients $b_{\rho}^{\text{ABC}}$ defined in the “Classical analytic estimates” section; a bridge between $b_{\rho}^{\text{ABC}}$ and $b_{\rho}^{\text{Lean}}$ is stated explicitly below. For Lean we fix a normalization in which the explicit-formula package identifies $b_{\rho}^{\text{Lean}}$ with the prefactor

$$\text{explicit\_b}_{\rho}(\rho) := \pi^{-\rho/2}\Gamma\left(\frac{\rho}{2}\right).$$

This normalization matches the Lean definition explicit\_b\_rho\_expression. Any additional holomorphic factors (e.g., $H(s)$ or $(\rho-1)/\rho$) appear only in the analytic coefficient $b_{\rho}^{\text{ABC}}$ and are related to $b_{\rho}^{\text{Lean}}$ by Assumption 11.3.

## Notation summary

* $\xi_\alpha$: the completed zeta-like function of the ERURH alpha layer.

* $s = \log x$, $\log R(s) = E(e^s)/e^s$, $J_{\text{rel}}(s) = d(\log R)/ds$.

* $\rho = \beta + i\gamma$: a non-trivial zero of $\zeta(s)$.

* $b_{\rho}^{\text{Lean}}$: Lean-side explicit-formula coefficient.

* $b_{\rho}^{\text{ABC}}$: analytic preprint coefficient used in Theorems A/B/C.

* $C_{\text{env}}$: formal RMS envelope constant.

**Notation convention.** The symbol $\alpha$ is reserved for the fixed alpha layer (e.g., $\xi_\alpha$, alphaBridge). The weight of a mode is denoted $\beta$; “supercritical” always means $\beta > 1/2$. We avoid phrases like “mode of weight $\alpha > 1/2$” to keep the roles disjoint.
## 3 Main theorem (conditional)

**Theorem 3.1** (Conditional ERURH master theorem). Assume the classical zeta package (Assumption 11.1), the ERU explicit formula (Assumption 11.2), spectral decay (Assumption 11.6), the large-sieve estimate (Assumption 11.7), the RMS window hypotheses (Assumption 11.9), the window-coverage bridge (Assumption D.1), and the correctness of the alpha certificates and numeric coverage (Assumption 11.13). Then there are no ERU modes with weight $\beta > 1/2$, the ERU strong inertia bound holds, and the Riemann Hypothesis for $\xi_\alpha$ follows.

The exact Lean statement additionally takes an explicit `AxiomsShimAccepted` package and separates `CertificatesCorrectAlpha` from `NumericCoverageAlpha`; see the machine-generated exports below.

**Remark 3.2.** A proof is given in Section 13 using the Plan B RMS-local route and the gate-closure implications of the alpha certificates. This theorem is conditional: the Lean development proves the implication under the analytic packages and numeric certificates listed above, and acceptance of the result depends on external verification of those analytic proofs and the gate-certified data.

**Referee-grade summary.** If one accepts the explicit analytic assumptions listed in this paper (including the A1/A2 window implications, the window-coverage bridge, and the coefficient-normalization bridge where applicable), the analytic inputs from the companion preprint (Theorems A/B/C as used for A2), the finite certificate checks (`CertificatesCorrectAlpha` plus `NumericCoverageAlpha`), and the explicit Lean hypothesis bundle `AxiomsShimAccepted`, then Lean verifies the implication up to *RiemannHypothesisxiAlpha*. The paper explains the intermediate chain “no supercritical modes $\Rightarrow$ strong inertia $\Rightarrow$ RH($\xi_\alpha$)” under Assumption 11.1.

## 4 Formal verification in Lean

The conditional ERURH master theorem is formalized in Lean 4 (mathlib). The exact statement and axiom footprint below are machine-generated and included in the arXiv bundle. These files are produced by running `lake env lean` on `docs/core/PrintMasterStatement.lean` and `docs/core/PrintAxioms_Numeric.lean`. The outputs are redirected to `arxiv_submission/lean_master_statement.txt` and `arxiv_submission/lean_master_axioms.txt`.

theorem ERURH.RH_from_ERURH_conditional : ∀ (G : ERURH.ERURH_GlobalAssumptions) (hAxioms : ERURH.Axioms : G) ERURH.CertificatesCorrectAlpha → ERURH.NumericCoverageAlpha G.window.ctx → ERURH.RiemannHypothesis ERURH.CertificatesCorrectAlpha hAxioms hCerts hNumeric

ERURH.ERURH_GlobalAssumptions.casesOn (motive := fun x =>

ERURH.NumericCoverageAlpha x.window.ctx → ERURH.RiemannHypothesis ERURH.xiAlpha) G (fun eru window hNumeric =>

ERURH WindowScalingAssumptions.casesOn (motive := fun x =>

ERURH.NumericCoverageAlpha { eru := eru, window := x }.window.ctx → ERURH.RiemannHypothesis ERURH.NumericCoverageAlpha hAxioms hCerts hNumeric

(fun ctx hA1 hLow hTail hNumeric =>

ERURH.RH_from_ERURH_assumptions eru ctx hA1 hLow hTail hAxioms hCerts hNumeric) hNumeric)

hNumeric

structure ERURH.ERURH：<u>GlobalAssumptions</u> : Type 1

number of parameters: 0

fields:

ERURH.ERURH：<u>GlobalAssumptions</u>.eru : ERURH.ERURH_Assumptions
ERURH.ERURH_GlobalAssumptions.window : ERURH WindowScalingAssumptions
constructor:

ERURH.ERURHatsHGlobalAssumptions.mk (eru : ERURH.ERURH-Assumptions) (window : ERURH WindowScalingAssumptions
ERURH.ERURHGlobalAssumptions

structure ERURH.ERURH-Assumptions : Type
number of parameters: 0

fields:

ERURH.ERURH-Assumptions.classical : ERURHClassicalZetaAssumptions

ERURH.ERURH-Assumptions.spectral : ERURH Alpha.SpectralAssumptionsAlpha

ERURH.ERURH-Assumptions.ls_ga : ERURH Alpha.LSGammaAssumptions

ERURH.ERURH-Assumptions.explicit-formula-ERU : ERURH. Alpha.ExplicitFormulaERU

ERURH.ERURH-Assumptionsnebeta_inert : ERURH.BetaInertiaAssumptions

constructor:

ERURH.ERURH-Assumptions.mk (classical : ERURHClassicalZetaAssumptions)
(spectral : ERURH. Alpha.SpectralAssumptionsAlpha) (ls_ga : ERURH. Alpha.LSGammaAssumptions)
(explicit formula ERU : ERURH. Alpha.ExplicitFormulaERU) (beta_inert : ERURH.BetaInertiaAssumptions)
ERURH.ERURH-Assumptions

structure ERURH WindowScalingAssumptions : Type 1
number of parameters: 0

fields:

ERURH. WindowScalingAssumptions. ctx : ERURH.RMSLocalContext

ERURH. WindowScalingAssumptions.hA1 : ERURH.A1_mode self. ctx

ERURH. WindowScalingAssumptions.hLow : ERURH.A2Low_RMS self. ctx

ERURH. WindowScalingAssumptions.hTail : ERURH.A2Tail_RMS self. ctx

constructor:

ERURH. WindowScalingAssumptions.mk (ctx : ERURH.RMSLocalContext) (hA1 : ERURH.A1_mode ctx) (hLow : ERURH.RMSLocalContext) (hTail : ERURH.A2Tail_RMS ctx) : ERURH. WindowScalingAssumptions

Axiom footprint for the master theorem:

'ERURH.RH_from_ERURH_conditional' depends on axioms: [propext,
Classical.choice,
Lean.ofReduceBool,
Lean.trustCompiler,
Quot.sound]

'ERURH.RH_unconditional_core' depends on axioms: [propext, Classical.choice, Quot.sound]

'ERURH.GlobalEnergyCertificateCorrect_alpha' depends on axioms: [propext, Classical.choice, Quot.sound]

'ERURH.globalEnergyCertificate-true alpha' depends on axioms: [propext, Classical.choice, Quot.sound]

'ERURH.KernelBlowupCertificateCorrect alpha' depends on axioms: [propext, Classical.choice, Quot.sound]

'ERURH.kernelBlowupCertificate-true alpha' depends on axioms: [propext, Classical.choice, Quot.sound]

'ERURHAlpha.RMS_envelope_closed' depends on axioms: [propext, Classical.choice, Quot.sound]

ERURH.Beta.BetaInertiaBundle : Type

ERURH.Beta.StrongInertiaCertificate_beta : Type

ERURH.Beta.StrongInertiaComposite_beta : Type

ERURH.Beta.StrongInertiaCertificateCorrect_beta (cert : ERURH.Beta.StrongInertiaCertificate_beta) : Prop

ERURH.Beta.StrongInertiaCompositeCorrect_beta (comp : ERURH.Beta.StrongInertiaComposite_beta) : Prop

Axioms shim bundle (Lean export):

structure ERURH.AxiomsShimAccepted : Type

number of parameters: 0

fields:

ERURH.AxiomsShimAccepted.alphaInterfacesBase : ERURH AlphaInterfaces

ERURH.AxiomsShimAccepted.explicit alpha via stages : ERURH.ExplicitFormulaLaws ERURH.alphaBridge ERURHAlphaPsi
ERURH.AxiomsShimAccepted.xiicomments : Prop
ERURH.AxiomsShimAccepted.h_xiaroundalpha : self.xi around alpha
ERURH.AxiomsShimAccepted.xiargumentalpha : Prop
ERURH.AxiomsShimAccepted.h_xiargumentalpha : self.xiargumentalpha
ERURH.AxiomsShimAccepted.xiaroundalpha of hypotheses : ERURH.xi around hypotheses alpha -> self.xi around hypotheses alpha
ERURH.AxiomsShimAccepted.xiargumentalpha of hypotheses : ERURH.xiargumenthypothesesalpha -> self.xiargumenthypothesesalpha
ERURH.AxiomsShimAccepted.rh_from_E alpha of hypotheses : ERURH.E around strong alpha /
self.xi around alpha /
self.xiargumentalpha /
ERURH.explicit rect alpha /
Nonempty (ERURH.ExplicitFormulaLaws ERURH alpha Bridge ERURH.xiAlpha ERURH AlphaPsi) ->
ERURH.RHfromE ERURH.xiAlpha ERURH AlphaPsi
ERURH.AxiomsShimAccepted.h_inertia to_E : ERURH.InertiaERU alpha strong -> ERURH.E around strong alpha
ERURH.AxiomsShimAccepted.h_inertia of E : ERURH.E around strong alpha -> ERURH.InertiaERU alpha strong
ERURH.AxiomsShimAccepted.h_RH_to_E : ERURH.RiemannHypothesis ERURH.xiAlpha -> ERURH.E around strong alpha
constructor:
ERURH.AxiomsShimAccepted.mk (alphaInterfacesBase : ERURH AlphaInterfaces)
(explicit alpha via stages : ERURH.ExplicitFormulaLaws ERURH alpha Bridge ERURH.xiAlpha ERURH AlphaPsi)
(xi around alpha : Prop) (h_xi around alpha : xi around alpha) (xi argument alpha : Prop)
(h_xiargumentalpha : xiargumentalpha)
(xi around alpha of hypotheses : ERURH.xi around hypotheses alpha -> xi around alpha)
(xi argument alpha of hypotheses : ERURH.xiargumenthypothesesalpha -> xiargumentalpha)
(rh_from_E alpha of hypotheses :
ERURH.E around strong alpha /
xi around alpha /
xi argument alpha /
ERURH.explicit rect alpha /
Nonempty (ERURH.ExplicitFormulaLaws ERURH alpha Bridge ERURH.xiAlpha ERURH AlphaPsi) ->
ERURH.RHfromE ERURH.xiAlpha ERURH AlphaPsi)
(h_inertia to_E : ERURH.InertiaERU alpha strong -> ERURH.E around strong alpha)
(h_inertia of E : ERURH.E around strong alpha -> ERURH.InertiaERU alpha strong)
(h_RH_to_E : ERURH.RiemannHypothesis ERURH.xiAlpha -> ERURH.E around strong alpha) : ERURH.AxiomsShim

Gap statements (machine-generated):

The following are exactly the gap statements exported by this Lean version (see Appendix for the verbatim file):

* ERURH.A1_from_supercritical_buchstab ctx_real

* ERURH.MODE_RMSLowerBound_from_buchstab ctx_real

* ERURH ALPHA MODE THRESHOLD CONTROL ON CTXREALWINDOWFAMILY

* ERURH.ExplicitBRhoExpression

ERURH.A1_from_supercritical_buchstab ERURH Alpha.GeneratedRMSContext.ctx_real : Prop

ERURH.MODE_RMSLowerBound_from_buchstab ERURH Alpha.GeneratedRMSContext.ctx_real : $\mathbb{R} \to \mathbb{R} \to \text{Prop}$

ERURH ALPHA MODE THRESHOLD CONTROL ON CTXREALWINDOWFAMILY : Prop

ERURH.ExplicitBRhoExpression : Prop

These gap statements are the authoritative Lean gaps for this version. We provide full proofs for the primary legacy window-free route (A1 and A2) in this paper, and full proofs of the A/B/C analytic inputs in the companion preprint. The Buchstab-specific gaps are A1_from_supercritical
_buchstab, ModeRMSLowerBound_from_buchstab, and ExplicitBRhoExpression. These are explicit paper-level assumptions for the optional Buchstab route. The fixed-window threshold control remains a documented analytic gap, as noted in Assumption 11.10.

Discharge map for AxiomsShimAccepted:

<table><thead><tr><td>Field(s)</td><td>Discharge path</td></tr></thead><tbody><tr><td>alphaInterfacesBase, explicit_alpha_via_stages xi bounds alpha, xi argument alpha and their hypothesis bridges rh from E alpha of hypotheses h inertia to E, h inertia of E, h RH to E</td><td>Assumption 11.2 (explicit formula package).<br/>Classical/citable implications (Assumptions Ledger).<br/>Classical/citable implications (Assumptions Ledger).<br/>Classical/citable implications (Assumptions Ledger).</td></tr></tbody></table>

Route B bridge assumptions (primary legacy window-free or alternative fixed-window computational) are listed in Section 5 and are not part of AxiomsShimAccepted.

The beta layer is now an explicit hypothesis bundle (no frozen numeric input is present in data/releases/erurh-v2-core/formal); see the Assumptions Ledger section below.

# 5 No supercritical ERU modes

**Proposition 5.1** (No supercritical ERU modes (conditional)). Assume the Plan B RMS-local hypotheses (Assumption 11.9), the window-coverage bridge (Assumption D.1), and the correctness of the alpha certificates and numeric coverage (Assumption 11.13). Then for every $\beta > 1/2$, there is no ERU exponential mode of weight $\beta$.

*Proof.* Fix $\beta > 1/2$ and suppose for contradiction that $\text{ERU\_mode\_beta}(\beta)$ holds. By Lemma 12.1, there exists a window $w$ with $\text{RMS}_\alpha(w) > C_{\text{env}}$. By Assumption D.1, we may choose $w$ in the certified family $W_{\text{cert}}$, so gate bounds apply. By Lemma 12.2, the renormalization gate is open. Assumption 11.13 implies the relevant renormalization gates are closed, a contradiction. Hence $\text{ERU\_mode\_beta}(\beta)$ does not hold. Since $\beta > 1/2$ was arbitrary, no supercritical ERU exponential mode can exist. □

**Two Route B bridges (primary legacy window-free vs alternative fixed-window).**

* **Legacy window-free bridge (primary route).**

The paper-level lemma A1_from_supercritical (Lemma 5.3) supplies the A1 mode lower bound in an abstract RMS context. A2-low/tail are supplied by Lemma 10.4.

* **Fixed-window bridge (alternative computational route).**

The Lean hypothesis ERURH. Alpha. ModeThresholdControlOnContextRealWindowFamily asserts that the supercritical-mode threshold can be chosen within the `ctx_real` window family. This is a paper-level analytic assumption; the gate checks only the numeric side conditions (see Assumption 11.10).
<table><thead><tr><th>Route</th><th>Lean gap</th><th>Discharge</th><th>Reference</th></tr></thead><tbody><tr><td>Primary (legacy window-free)</td><td>A1_from_supercritical and A2</td><td>Paper</td><td>Lemmas 5.3, 10.4</td></tr><tr><td>Alternative (fixed-window)</td><td>ModeThreshold<br>Control<br>OnContextReal<br>WindowFamily</td><td>Paper + gate</td><td>Assm. 11.10</td></tr></tbody></table>

The main narrative below follows the primary legacy window-free route; the fixed-window computational bridge is included as a documented alternative.

**Lemma 5.2** (Exponential dominates polynomial). Let $a > 0$, $k \ge 0$, and $C > 0$. Then there exists $S_1$ such that for all $S \ge S_1$,

$$ \frac{\exp(aS)}{S^k} > C. $$

*Proof.* Set $f(S) = \exp(aS)/S^k$ for $S > 0$. Then $\log f(S) = aS - k \log S \to \infty$ as $S \to \infty$. Choose $S_1$ so that $\log f(S) > \log C$ for all $S \ge S_1$, hence $f(S) > C$. $\square$

### Legacy window-free A1 lemma (primary route).

**Lemma 5.3** (A1 from supercritical mode (legacy window-free)). Let $\beta \in \mathbb{R}$ with $\beta > 1/2$. If ERU_mode beta ($\beta$) holds, then A1_mode holds for the chosen RMS context. Equivalently, this is the statement ERURH. A1_from_supercritical.

*Proof.* We use the admissibility (cofinality) of the window family (Definition 11.8) and the elementary fact that $\exp(aS)/S^2 \to \infty$ for any $a > 0$.

**Step 1 (mode threshold).** By ERU_mode beta ($\beta$) there exists $s_0$ such that for all $s \ge s_0$, $|\log R_{\alpha}^{\text{mode}}(s)| \ge \exp((\beta - 1/2)s)$. Here ERU_mode beta is interpreted on the supercritical mode component $\log R_{\alpha}^{\text{mode}}$; this is the analytic content of the A1 bridge.

**Step 2 (exp dominates the envelope).** Let $C_* := c_{\text{low}} + c_{\text{tail}} + C_{\text{env}}$. Since $\beta > 1/2$, Lemma 5.2 (with $a = \beta - 1/2$, $k = 2$) yields an $S_1$ such that for all $S \ge S_1$, $\exp((\beta - 1/2)S)/S^2 > C_*$.

**Step 3 (choose a large window).** By admissibility (Definition 11.8), there exists a window $w = [S, S + L]$ with $S \ge \max\{s_0, S_1, 1\}$. For any $s \in I_w = [S, S + L]$ we have $s \ge S \ge s_0$, hence $|\log R_{\alpha}^{\text{mode}}(s)| \ge \exp((\beta - 1/2)s) \ge \exp((\beta - 1/2)S)$.

**Step 4 (pointwise to RMS).** By Lemma 5.8, $\text{RMS}_{\text{mode}}(w) \ge \exp((\beta - 1/2)S) \ge \exp((\beta - 1/2)S)/S^2$. Set $K := \exp((\beta - 1/2)S)/S^2$; then $K > C_*$ by Step 2 and $\text{RMS}_{\text{mode}}(w) \ge K$. This is exactly A1_mode. $\square$

The Buchstab bridge below provides one concrete derivation of ERU_mode beta and the mode coefficient lower bound; in Lean, A1_from_supercritical is derived from that packaging via A1_from_supercritical_of_buchstab.

### Buchstab bridge (analytic derivation of A1)

The Buchstab bridge supplies one analytic route to Lemma 5.3. The remaining analytic gap is the bridge ERURH. A1_from_supercritical_buchstab for a chosen RMS context, together with the explicit-formula identification ERURH. ExplicitBRhoExpression. The exact Lean statements are machine-exported below.

ERURH.A1_from_supercritical_buchstab ERURH Alpha.GeneratedRMSContext.ctx_real : Prop
ERURH.MODE.RMSLowerBound_from_buchstab ERURH Alpha.GeneratedRMSContext.ctx_real : $\mathbb{R} \to \mathbb{R} \to \text{Prop}$
ERURH ALPHA.MODEThresholdControlOnContextRealWindowFamily : Prop
ERURH.ExplicitBRhoExpression : Prop
**Definition (Buchstab mode lower bound).** Fix an RMS context ctx with window type and RMS_mode. For $\beta, \gamma \in \mathbb{R}$, we write $\text{ModeRMSLowerBound\_from\_buchstab}(ctx, \beta, \gamma)$ for the statement that there exists a structural coefficient $c_{\text{struct}} \neq 0$ and a threshold $S_0$ such that for all $S \geq S_0$ there exists a window $w$ with

$$ \text{RMS\_mode}(w) \geq |c_{\text{struct}} m(\beta + i\gamma)| \cdot \frac{\exp((\beta - 1/2)S)}{S^2}. $$

This is exactly the Lean predicate `ERURH ModeRMSLowerBound_from\_buchstab`.

**Lemma 5.4** (A1 from supercritical mode (Buchstab bridge)). Let $\beta \in \mathbb{R}$ with $\beta > 1/2$. If `ERU_mode\_beta(\beta)` holds, then there exists $\gamma \in \mathbb{R}$ such that the predicate `ModeRMSLowerBound\_from\_buchstab(ctx, \beta, \gamma)` holds. Equivalently, this is the statement `ERURH A1\_from\_supercritical\_buchstab`.

*Proof.* **Step 1 (unpack the mode).** By `ERU_mode\_beta(\beta)` there exists $s_0$ such that for all $s \geq s_0$, $|\log R_\alpha(s)| \geq \exp((\beta - 1/2)s)$.

**Step 2 (explicit formula coefficient; paper assumption).** The explicit formula package identifies the supercritical mode coefficient with the explicit prefactor (Assumption 11.2); combined with Lemma 5.6, this yields a factorization $b_\rho^{\text{Lean}} = c_{\text{struct}}(\rho) m(\rho)$ with $c_{\text{struct}}(\rho) \neq 0$. This is the central paper-level input in the Buchstab bridge. The normalization of $b_\rho^{\text{Lean}}$ matches the preprint coefficient via Assumption 11.3; see Remark 11.4.

**Step 3 (non-vanishing of the multiplier).** Lemma 5.5 gives $m(\beta + i\gamma) \neq 0$ for $\beta > 0$, hence the mode coefficient is nonzero.

**Step 4 (RMS lower bound).** By the definition of `RMS_mode` for the mode contribution and the admissibility of the window family (Definition 11.8), one can choose windows with arbitrarily large base $S$ and obtain the stated lower bound with coefficient $|c_{\text{struct}} m(\beta + i\gamma)|$. This is precisely the predicate `ModeRMSLowerBound_from\_buchstab(ctx, \beta, \gamma)`. $\square$

**Buchstab multiplier non-vanishing (paper bridge for A1).**

Recall the multiplicative averaging operator

$$ (Th)(u) := \frac{1}{u} \int_{u/3}^{u/2} h(t) dt. $$

For a monomial $h(t) = t^{\rho-1}$ with $\rho = \beta + i\gamma$, one computes

$$ (Th)(u) = u^{\rho-1} m(\rho), \quad m(\rho) = \frac{2^{-\rho} - 3^{-\rho}}{\rho}, \quad 2^{-\rho} := \exp(-\rho \log 2). $$

**Lemma 5.5** (Buchstab multiplier non-vanishing). If $\beta > 0$ then $m(\beta + i\gamma) \neq 0$.

*Proof.* Write $2^{-\rho} = \exp(-\rho \log 2)$ and $3^{-\rho} = \exp(-\rho \log 3)$. Then $|2^{-\rho}| = 2^{-\beta}$ and $|3^{-\rho}| = 3^{-\beta}$. Since $\beta > 0$, we have $2^{-\beta} \neq 3^{-\beta}$, hence by the reverse triangle inequality

$$ |2^{-\rho} - 3^{-\rho}| \geq |2^{-\rho}| - |3^{-\rho}| = |2^{-\beta} - 3^{-\beta}| > 0. $$

Thus the numerator is nonzero. The denominator $\rho$ is also nonzero because $\Re(\rho) = \beta > 0$. Therefore $m(\rho) \neq 0$. $\square$
**Lemma 5.6** (Buchstab coefficient identification). Let $\rho = \beta + i\gamma$ be a nontrivial zero with $\beta > 1/2$. Assume the explicit-formula identification $b_{\rho}^{\text{Lean}} = \text{explicit}_b(\rho)$ with $\text{explicit}_b(\rho) = \pi^{-\rho/2}\Gamma(\rho/2)$ as in the explicit formula package. Then the ERU coefficient satisfies

$$b_{\rho}^{\text{Lean}} = c_{\text{struct}}(\rho) m(\rho) \quad \text{with} \quad c_{\text{struct}}(\rho) \neq 0.$$

*Proof (step-by-step). Step 1 (explicit formula identification).* By Assumption 11.2, $b_{\rho}^{\text{Lean}} = \text{explicit}_b(\rho) = \pi^{-\rho/2}\Gamma(\rho/2)$. Since $\Gamma$ has no zeros and $\pi^{-\rho/2} \neq 0$, we obtain $b_{\rho}^{\text{Lean}} \neq 0$ for $\beta > 0$.

**Step 2 (define the structural coefficient).** By Lemma 5.5, $m(\rho) \neq 0$ for $\beta > 0$. Define $c_{\text{struct}}(\rho) := b_{\rho}^{\text{Lean}}/m(\rho)$. This is a purely algebraic step once $m(\rho) \neq 0$. Then $b_{\rho}^{\text{Lean}} = c_{\text{struct}}(\rho) m(\rho)$ by construction.

**Step 3 (non-vanishing).** Since $b_{\rho}^{\text{Lean}} \neq 0$ and $m(\rho) \neq 0$, we have $c_{\text{struct}}(\rho) \neq 0$. $\square$

<figure><img src="image_2.png" /></figure>

**Lean correspondence.**

The explicit-formula identification is the Lean predicate: `ERURH.ExplicitBRhoExpression`. From it, Lean derives `ERURH.BuchstabCoefficientNonzero` via `buchstabCoefficient_nonzero_of_explicit_b_rho_expr`. The lemma above is the paper-level justification for the explicit identification and the derived factorisation.

**Consequences for A1.** If the supercritical mode contribution to $\log R_{\alpha}$ carries a coefficient that is proportional to $m(\rho)$ times a structural factor $c_{\text{struct}} \neq 0$ (from the explicit formula package), then the mode coefficient is nonzero. Lemma 5.6 provides this factorisation, and Lemma 5.5 ensures the multiplier is nonzero. This reduces the analytic content of A1 to the explicit-formula identification and the Buchstab lower-bound bridge; the exponential growth itself is already captured by the multiplier and the elementary exp-dominates-polynomial lemma used in the Lean core.

**Window semantics and admissibility.** The Lean predicate `A1_mode` is defined over an abstract `RMSLocalContext` with a type of windows and an associated `RMS_mode`. In the paper we model a window as an interval $w = [S, S+L]$ with $1 \ll L \ll S^{\alpha}$ and $I_w = [S, S+L]$. The only analytic input used in Steps 3 and 4 is *admissibility*, i.e., the ability to choose a window with arbitrarily large $S$. We build this cofinality into the definition of an admissible window family (Definition 11.8), so it is part of the window model rather than an extra analytic assumption. The separate window-coverage bridge (Assumption D.1) is still required when combining A1 with the finite certified family.

**Remark 5.7** (Does not replace A/B/C). Lemma 5.4 is an internal ERURH analytic bridge. It does not replace the classical assumptions A/B/C (zero-density, coefficient growth, and large-sieve style estimates), which are still required to derive the A2-tail bound and to connect the explicit formula to the ERU framework.

**Definitions (paper semantics).** Fix a window $w$ with associated interval $I_w \subset \mathbb{R}$ (paper-level window; in Lean this is represented abstractly by a 'Window' in 'RMSLocalContext'). Define the RMS-mode contribution by

$$\text{RMS\_mode}(w) := \left( \frac{1}{|I_w|} \int_{I_w} |\log R_{\alpha}^{\text{mode}}(s)|^2 ds \right)^{1/2},$$

where $\log R_{\alpha}^{\text{mode}}$ denotes the supercritical mode component of $\log R_{\alpha}$. The total RMS of $\log R_{\alpha}$ is denoted $\text{RMS}_{\alpha}(w)$ and is decomposed in Assumption 11.9. For Route B we use the unique window of `ctx_real` (since $n\_windows = 1$), written `ctx_real_windows` in Lean.
**Lemma 5.8 (Pointwise-to-RMS bridge).** If $|\log R_{\alpha}^{\text{mode}}(s)| \ge K$ for all $s \in I_w$ and $|I_w| > 0$, then $\text{RMS_mode}(w) \ge K$. This follows by squaring the pointwise bound, integrating over $I_w$, and taking square roots:

$$ \frac{1}{|I_w|} \int_{I_w} |\log R_{\alpha}^{\text{mode}}(s)|^2 ds \ge \frac{1}{|I_w|} \int_{I_w} K^2 ds = K^2. $$

**Lean correspondence.**

<table><thead><tr><th>Paper object</th><th>Lean name</th></tr></thead><tbody><tr><td>log R<sup>mode</sup><sub>α</sub>(s)</td><td>paper-only mode component of ERURH.logR<sub>α</sub></td></tr><tr><td>w (window)</td><td>w : ctx Window for an abstract RMSLocalContext</td></tr><tr><td>I<sub>w</sub></td><td>window interval associated to w (paper-level)</td></tr><tr><td>RMS_mode(w)</td><td>ctx.RMS_mode w</td></tr></tbody></table>

The Lean development does not define $\log R_{\alpha}^{\text{mode}}$ explicitly; instead, its effect is summarized by the hypothesis A1_mode. The A1 lemma above interprets ERU_mode_beta as a bound on the mode component.

**Gate/Lean alignment.** In the window-free legacy route, A1_from_supercritical is treated as an analytic lemma for an abstract RMS context. If one later instantiates this context with gate data (e.g., ctx_real), then RMS_mode and the envelope closure are discharged by the numeric certificates; the window-free core itself does not depend on any fixed window family.

**Semantic compatibility of RMS_mode.** For the fixed-window route, we also track a semantic lower bound

$$ \text{rms\_semantic}(w) := \inf_{s \in I_w} |\log R_{\alpha}(s)|. $$

In Lean this is the definition Alpha.rmsSemantic w. The gate provides a certificate (Lean: GeneratedRMSModeBridge.ctx_real_rms_mode_geSemantic) that for each ctx_real window, ctx_real.RMS_mode w ≥ rmsSemantic w. Together with Lemma 5.8, this ensures the numeric RMS_mode used by the gate is a valid lower bound for the analytic RMS in the fixed-window chain. The legacy window-free route does not use this certificate.

# 6 Reproducibility / Gate

The reproducible pipeline regenerates the numeric artifacts and rebuilds the Lean development:

python tools/make_rational bounds.py
python tools/make_certificate values.py
lake build ERURH
python scripts/verify gate.py --skip-pytests

The reproducibility data release includes all numeric inputs used by the gate (rational bounds, certificates, and RMS context JSON). These are regenerated by the scripts above and are distinct from the analytic assumptions listed in Assumption 11.1 and the lemma A1_from_supercritical.
**Reproducibility manifest.** The bundle includes `reproducibility manifest.txt` with tool versions and SHA256 hashes of the frozen numeric inputs used by the gate.

Reproducibility manifest

Generated: 2025-12-30T18:54:45

git head: 6af77717f487ccbb98b4843608b26cc206935868

python: Python 3.11.9

lake: Lake version 5.0.0-src+744f980 (Lean version 4.25.0-rc2)

lean_toolchain: leanprover/lean4:v4.25.0-rc2

os: Microsoft Windows 11 Home 10.0.26100

SHA256 hashes:

DB061BE2D5633EDFEE627500A70F100BBB9744A10C62A8D43336E174C6562EF6 data/docs/paper/rational bounds.json
D422545FCEC4AC951384491E6ACBDE6726E6CAB67E9E36E8BD05CEB090F4CB58 data/docs/paper/certificate values.js
A4440A79FA5F187BB838F9A746115787C1629A60E3D9D3BA14F0E5E2C80A2C8E data/docs/paper/rms context.json
C0C8734119A250BA68A794991835123AA7C9030DB592AF212C90E4AC56284009 data/docs/paper/rms mode bridge.json
79937ED5901C033B6179A5A70C2B8F1C2939F03B92D5D16116090F9FB5749D7C data/docs/paper/beta certificate.js
2FE62EE1A7AB82E39C762C1676ABD0010E1B8EE09C0893F1BF6D4E50B1014F32 arxiv submission/data/releases/erurh-v2-core/formal/)
C59146B32CFAEDF51227ADFF03AB89CB1FCCDDCB931E3BDA2CE01183FE77C430 arxiv submission/data/releases/erurh-v2-core/formal/)

**Trust boundary.** The formal logic is checked by the Lean kernel and mathlib. The numeric gate depends on the Python toolchain in `tools/` (including interval arithmetic via `mpmath.iv`) and OS-level arithmetic used for packaging (`tar`, `PowerShell`). These are the only computational dependencies outside Lean.

**Interval-checked numeric bridge (example).** The gate verifies the fixed-window RMS bridge using interval arithmetic on the witness points. The script `tools/check_rms_modeBridge.py` reads `rms_modeBridge.json` and `rms_context.json` from the frozen release data (bundled under `data/releases/erurh-v2-core/formal/`) and checks, for each window, that

$$| \log R_{\alpha}(s_{\text{wit}}) | \le u_{\text{wit}} \le \text{RMS\_mode}(w), \quad s_{\text{wit}} \in [s_{\text{min}}, s_{\text{max}}],$$

using interval enclosures (`mpmath.iv`) with adaptive precision (`dps` raised up to 200 if needed). This is a fully reproducible check:

python tools/check_rms_mode bridge.py

and it is executed by `scripts/verify gate.py`. The log line `"OK: RMS mode bridge certificate matches RMS context data."` confirms success.

# 7 Assumptions Ledger

* **Axioms footprint.** No project axioms: there are no `axiom/constant` declarations in `ERURH`. Lean kernel axioms still appear in `#print axioms`. (e.g., `propext`, `Classical.choice`, `Quot.sound`, `Lean.ofReduceBool`, `Lean.trustCompiler`).

* **A/B/C (analytic packages).** The analytic inputs used by Plan B: spectral decay (A), large-sieve bounds (B), and the uniform RMS tail bound (C) recorded in Theorem 10.3. These feed the A2 derivation (Lemma 10.4). Full proofs are included in Theorem ABC preprint.tex.

* **Route B bridges (primary + alternative).** We maintain a primary legacy window-free bridge and an alternative fixed-window computational bridge for Route B (exported in `lean gap statements.txt` via the Buchstab packaging):
- **Legacy window-free bridge (primary route).** The lemma `a1-from-supercritical` supplies A1 in an abstract RMS context, while A2 is discharged by Lemma 10.4. Admissibility (cofinality) of the window family is built into the paper definition of windows, not stated as a separate assumption.

- **Fixed-window bridge (alternative route).** The hypothesis `ERURH Alpha ModeThresholdControlOnContextWindowFamily` (Assumption 11.10) pairs with gate-verified constraints on `ctx_real`. The paper provides a discussion of the analytic gap; a full proof is deferred to a supplement.

- **Buchstab derivation (optional).** The hypotheses `ERURH.A1_from_supercritical_buchstab` and `ERURH.ExplicitBRhoExpression`. These are discharged by Lemmas 5.4 and 5.6, yielding `A1_from_supercritical`.

These bridges do not replace the classical A/B/C assumptions; they supply the A1/A2 inputs needed for the RMS-local contradiction.

* **Classical / citable.** Zeta explicit-formula setup and classical implications (including the ERU inertia $\leftrightarrow E$-bound links and RH $\Rightarrow E$-bounds). The zero-parameterization objects $\beta, \gamma$ and coefficients $b_\rho$ remain part of this classical package; the Lean normalization uses only the gamma prefactor, while any auxiliary holomorphic factors (e.g. $H(s)$) are absorbed into $b_\rho$ in the preprint. For the Buchstab kernel used in the alpha bridge, the Mellin multiplier $m(s)$ is nonzero on $\mathfrak{R}(s) > 0$ (Remark 11.5), so only the auxiliary holomorphic weights need to be nonvanishing.

* **Gate + certificates (alpha + RMS + beta).** The alpha certificates and RMS coverage are discharged by the reproducible pipeline (`verify_gateway.py`), which regenerates the rational bounds and certificate values and checks the Lean build. RMS A2-low/A2-tail are generated from frozen `rms_context.json` via `tools/make_rms_context.py`. The beta inertia bundle is generated from frozen JSON via `tools/make_beta_certificate.py` and is discharged in the same gate.

## AxiomsShimAccepted field map (explicit statements)

**alphaInterfacesBase.** Statement: existence of the alpha interface package ('AlphaInterfaces') providing the ERU observable log $R$ and $J_{rel}$ in the explicit-formula framework. Reference/proof: Assumption 11.2. Lean field: `AxiomsShimAccepted.alphaInterfacesBase`.

**explicit_alpha_via_stages.** Statement: the explicit-formula laws used by the alpha bridge hold, i.e. 'ExplicitFormulaLaws alphaBridge xiAlpha AlphaPsi'. Reference/proof: Assumption 11.2. Lean field: `AxiomsShimAccepted.explicit\_alpha\_via\_stages`.

**xiBoundsAlpha.**

Statement: the $\xi_\alpha$ bounds required by the ERU explicit-formula package hold (the proposition `xiBounds Alpha alpha`). Reference/proof: assumed as part of the explicit-formula bounds package; to be cited in the explicit-formula bounds section.
Lean field: `AxiomsShimAccepted.xi\_bounds\_alpha`.

**h_xiBoundsAlpha.** Statement: a proof witness of `xiBounds Alpha`. Reference/proof: immediate from the previous assumption. Lean field: `AxiomsShimAccepted.h\_xi\_bounds\_alpha`.
**xi_argument alpha.**

Statement: the $\xi_\alpha$ argument bounds required by ERURH hold (xi_argument alpha). Reference/proof: assumed as part of the explicit-formula bounds package; to be cited in the argument bounds section.

Lean field: AxiomsShimAccepted.xi\_argument\_alpha.

**h_xi_argument alpha.** Statement: a proof witness of xi_argument alpha. Reference/proof: immediate from the previous assumption. Lean field: AxiomsShimAccepted.h\_xi\_argument\_alpha.

**xi Bounds alpha of hypotheses.** Statement: xi Bounds hypotheses alpha ->

xi\_bounds\_alpha. Reference/proof: classical/citable implication (explicit-formula bounds package). Lean field: AxiomsShimAccepted.xi\_bounds\_alpha\_of\_hypotheses.

**xi_argument alpha of hypotheses.** Statement: xi_argument hypotheses alpha ->

xi\_argument\_alpha. Reference/proof: classical/citable implication (argument bounds package).

Lean field: AxiomsShimAccepted.xi\_argument\_alpha\_of\_hypotheses.

**rh_from_E alpha of hypotheses.**

Statement: (E\_bound\_strong\_alpha and xi\_bounds\_alpha and
xi\_argument\_alpha and explicit\_rect\_alpha and
Nonempty (ExplicitFormulaLaws alphaBridge xiAlpha AlphaPsi))

-> RHfromE

xiAlpha AlphaPsi. Reference/proof: classical/citable implications in the ERU explicit-formula framework.

Lean field: AxiomsShimAccepted.rh\_from\_E\_alpha\_of\_hypotheses.

**h_inertia_to_E.** Statement: InertiaERU\_alpha\_strong ->

E\_bound\_strong\_alpha. Reference/proof: classical ERU inertia $\Rightarrow$ strong E-bound implication.

Lean field: AxiomsShimAccepted.h\_inertia\_to\_E.

**h_inertia_of_E.** Statement: E\_bound\_strong\_alpha ->

InertiaERU\_alpha\_strong. Reference/proof: classical strong E-bound $\Rightarrow$ ERU inertia implication.

Lean field: AxiomsShimAccepted.h\_inertia\_of\_E.

**h_RH_to_E.** Statement: RiemannHypothesis xiAlpha ->

E\_bound\_strong\_alpha. Reference/proof: classical RH $\Rightarrow$ E-bound (Assumption 11.1). Lean field:

AxiomsShimAccepted.h\_RH\_to\_E.

## Classical/citable lemmas used as assumptions

The Lean bundle is AxiomsShimAccepted. It includes the following classical/citable implications, recorded as explicit hypotheses:

* InertiaERU\_alpha\_strong $\Rightarrow$ E\_bound\_strong\_alpha.

* E\_bound\_strong\_alpha $\Rightarrow$ InertiaERU\_alpha\_strong.

* RiemannHypothesis\_xiAlpha $\Rightarrow$ E\_bound\_strong\_alpha.
# 8 Energy, inertia, and ERU modes

The ERURH formalism introduces global energy functionals and “gates” that measure whether the observable $J_{rel}$ (or its smoothed variants) stays under a prescribed envelope. A key notion is the existence of an exponential ERU mode.

**Definition 8.1 (ERU mode).** An ERU mode of weight $\beta$ (Lean: ERU\_mode\_beta $\beta$) is an asymptotic component of $\log R(s)$ that grows like $\exp((\beta - \frac{1}{2})s)$ for large $s$. The ERURH theory is structured so that the presence of a mode with $\beta > 1/2$ forces energy blow-up beyond the allowable envelope.

**Definition 8.2 (Strong inertia).** Strong ERU inertia (Lean: InertiaERU\_alpha\_strong) is a quantitative upper bound on $J_{rel}(s)$ of the shape $|J_{rel}(s)| \le Ce^{-s/2}s^2$ for all sufficiently large $s$.

A central formal lemma is that the absence of supercritical modes implies strong inertia, and strong inertia implies RH for $\xi_{\alpha}$ under the classical zeta assumptions (Assumption 11.1).

# 9 Certificates and gates

ERURH isolates the new content into finite certificates, each of which is a finite list of rational inequalities derived from explicit computations. The alpha layer uses four certificates:

* GlobalEnergyCertificate\_alpha,

* KernelBlowupCertificate\_alpha,

* BridgeInertiaCertificate\_alpha,

* StrongInertiaCertificate\_alpha.

Correctness of these certificates is encoded as predicates in Lean. The certificates ensure that the global energy stays below a fixed envelope and that any supercritical mode would force a kernel energy blow-up. These implications are formalized as lemmas that close the ERURH gates. For the Plan B route, only the GlobalEnergy and KernelBlowup certificates are required to close the renormalization gate; the bridge/strong inertia certificates are used in the direct alpha route.

# 10 Classical analytic estimates (Theorems A, B, C)

This section records the classical analytic estimates for the explicit-formula coefficients $b_{\rho}^{ABC}$ that underlie the spectral hypotheses used in ERURH. The statements match the more detailed companion preprint and are included here to make the analytic inputs explicit.

## Standing hypotheses

Let $\rho = \beta + i\gamma$ range over the non-trivial zeros of $\zeta(s)$, counted with multiplicity, and let

$$b_{\rho}^{ABC} := \frac{\rho - 1}{\rho} G(\rho), \quad G(s) := \pi^{-s/2}\Gamma\left(\frac{s}{2}\right) H(s).$$

(H1) (Holomorphic model with gamma factor). The auxiliary factor $H(s)$ is holomorphic in a neighbourhood of the closed strip $0 \le Re(s) \le 1$, and the coefficients $b_{\rho}^{ABC}$ are defined by the above formula (in particular, the completed zeta factor $\pi^{-s/2}\Gamma(s/2)$ is present in $G(s)$).
(H2) (Polynomial vertical growth of H). There exist constants $C_H > 0$ and $A_H \ge 0$ such that

$$|H(\sigma + it)| \le C_H(1 + |t|)^{A_H} \quad (0 \le \sigma \le 1, t \in \mathbb{R}).$$

(H3) (Riemann–von Mangoldt and unit-interval zero counts). Let $N(T)$ denote the number of non-trivial zeros $\rho = \beta + i\gamma$ with $0 < \beta < 1$ and $0 < \gamma \le T$, counted with multiplicity. We use the Riemann–von Mangoldt formula and its consequence that, for $|y| \ge 3$,

$$\#\{\rho : y < \operatorname{Im}(\rho) \le y + 1\} \ll \log(|y| + 2),$$

with an absolute implied constant.

**Theorem 10.1** (Theorem A: Dyadic $L^2$ tail bound). Assume (H1)–(H3). Then there exist constants $c > 0$, $k \ge 0$, and $T_0 \ge 3$ such that, for all $T \ge T_0$,

$$\sum_{\rho} |b_{\rho}^{\text{ABC}}|^2 \ll T^{2k+1}(\log T) e^{-2cT}.$$

In particular, there exist constants $C > 0$ and $A > 0$ such that, for all $T \ge T_0$,

$$\sum_{\rho} |b_{\rho}^{\text{ABC}}|^2 \le C T (\log T)^A.$$

**Theorem 10.2** (Theorem B: Large-sieve mean-square bound). Assume (H3). Let $T \ge 3$ and $L \ge 1$, and define

$$F(u) = \sum_{\substack{\rho \\ T < |\gamma| \le 2T}} b_{\rho}^{\text{ABC}} e^{i\gamma u}.$$

Then

$$\frac{1}{L} \int_{0}^{L} |F(u)|^2 du \ll (\log T) \sum_{\substack{\rho \\ T < |\gamma| \le 2T}} |b_{\rho}^{\text{ABC}}|^2,$$

with an absolute implied constant. In particular, this holds in any admissible range $1 \ll L \ll T^\alpha$ with $0 < \alpha < 1$.

**Theorem 10.3** (Theorem C: Uniform RMS tail bound). Assume (H1)–(H3) and fix $B > 0$. Define

$$\tilde{F}_{\text{tail}}(s) := s^{-2} \sum_{|\gamma| > S^B} b_{\rho}^{\text{ABC}} e^{i\gamma s}, \quad K_{\text{tail}}(S, L)^2 := \frac{1}{L} \int_S^{S+L} |\tilde{F}_{\text{tail}}(s)|^2 ds.$$

Then there exist constants $c' > 0$ and $S_0 \ge 3$ such that, for all $S \ge S_0$ and all $L > 0$,

$$K_{\text{tail}}(S, L)^2 \ll S^{-4} \exp(-2c'S^B).$$

In particular, $K_{\text{tail}}(S, L)^2 \le M_{\text{tail}}^2$ uniformly in $S$ and $L$, for a suitable constant $M_{\text{tail}} > 0$.

Proofs of Theorems 10.1–10.3 are not reproduced here; see the companion preprint Theorem\_ABC\_preprint.tex. We record only the statements and use them as analytic inputs.
**Lemma 10.4** (A2-low and A2-tail from classical inputs). Assume the explicit-formula package (Assumption 11.2) together with Theorems 10.1–10.3. Then there exist constants $c_{low}$, $c_{tail}$ such that, for every admissible window $w = [S, S + L]$ with $1 \ll L \ll S^{\alpha}$, one has

$$ \text{RMS}_{\text{low}}(w) \le c_{\text{low}}, \quad \text{RMS}_{\text{tail}}(w) \le c_{\text{tail}}. $$

Equivalently, the A2-low and A2-tail clauses of Assumption 11.9 hold for the chosen RMS context.

*Proof. A2-low.* Choose a fixed cutoff $T_0$ and decompose the explicit formula into: (i) finitely many modes with $|\gamma| \le T_0$, (ii) trivial-zero terms, and (iii) the smooth test-factor contribution. Under Assumption 11.2 and the explicit-formula normalization, each of these pieces is uniformly bounded on admissible windows $[S, S + L]$ with $1 \ll L \ll S^{\alpha}$. The finite sum therefore yields a uniform constant $c_{low}$ for $\text{RMS}_{\text{low}}(w)$. The constant depends only on the fixed cutoff $T_0$ and the explicit-formula normalization, not on $S$ or $L$. The cutoff $T_0$ is fixed once in the analytic package (see the preprint), so $c_{low}$ is frozen with the choice of kernel and normalization.

**A2-tail.** The tail RMS on $w = [S, S + L]$ is, by definition, the normalized mean square of the tail contribution with the $s^{-2}$ weight. This is exactly the quantity $K_{\text{tail}}(S, L)$ in Theorem 10.3. Theorem 10.3 is derived from Theorems 10.1 and 10.2 in the preprint, using the dyadic $L^2$ tail bound and the large-sieve inequality for separated exponentials. Thus $K_{\text{tail}}(S, L)^2 \le M_{\text{tail}}^2$ uniformly on admissible windows, and we take $c_{\text{tail}} := M_{\text{tail}}$. Theorem 10.3 is stated uniformly in $S$ and $L$, so no extra hypotheses are required beyond Theorems 10.1–10.3 and the explicit-formula package. No additional hypotheses are used beyond Theorems 10.1–10.3 and the explicit-formula package. $\square$

Full derivations (including constants and admissible ranges) are in the bundled preprint. See Theorem_ABC_preprint.tex.

**Lean correspondence for A2.** The paper inequalities $\text{RMS}_{\text{low}}(w) \le c_{\text{low}}$ and $\text{RMS}_{\text{tail}}(w) \le c_{\text{tail}}$ are encoded in Lean as `ERURH.A2Low_RMSctx` and `ERURH.A2Tail_RMSctx`, where `ctx.RMS_low`, `ctx.RMSTail`, `ctx.c_low`, `ctx.cTail` live in `ERURH.RMSLocalContext`. The decomposition $\text{RMS}_{\alpha} \ge \text{RMS}_{\text{mode}} - (\text{RMS}_{\text{low}} + \text{RMS}_{\text{tail}})$ matches `ctx.RMS_decomp`. For the generated context `ctx_real`, the hypotheses are discharged by the generated lemmas `Alpha.GeneratedRMSContext.ctx_real_A2Low` and `Alpha.GeneratedRMSContext.ctx_real_A2Tail`.

These theorems provide the analytic content behind the spectral decay Assumption 11.6 and the large-sieve estimate Assumption 11.7. Proofs are given in the companion preprint Theorem_ABC_preprint.tex in the same submission folder, with references to standard sources (e.g. Titchmarsh, Montgomery–Vaughan, Ivic); we record only the statements here and treat them as classical inputs.

# 11 External analytic assumptions

The conditional theorem uses the following external packages. We list the assumptions explicitly to isolate analytic input from ERURH-specific logic.

**Assumption 11.1** (Classical zeta package). The completed function $\xi_{\alpha}$ satisfies the standard analytic properties of the Riemann zeta function: explicit formula for $\psi(x)$, functional equation, standard bounds for $\zeta'/\zeta$ in vertical strips, the Riemann–von Mangoldt zero counting formula (including local counts), and the classical equivalence between RH and bounds on $E(x)$. In particular, RH for $\xi_{\alpha}$ is equivalent to the classical RH for $\zeta$ under this package.
**Assumption 11.2** (Explicit formula for the ERU observable). The ERU observable $\log R(s)$ and its derivative $J_{rel}(s)$ admit an explicit formula of the form (2) in which the coefficients $b_{\rho}^{\text{Lean}}$ are identified with the explicit prefactor $\text{ explicit } b_{\rho}(\rho) = \pi^{-\rho/2}\Gamma(\rho/2)$ under the chosen normalization. Under this normalization, Lean takes $b_{\rho}^{\text{Lean}}$ to be the gamma prefactor; any additional holomorphic factors (e.g., $H(s)$ or $(\rho-1)/\rho$) are carried by $b_{\rho}^{\text{ABC}}$ and handled by Assumption 11.3.

**Assumption 11.3** (Coefficient normalization bridge). Let $b_{\rho}^{\text{ABC}}$ denote the analytic preprint coefficients $b_{\rho}^{\text{ABC}} := \frac{\rho-1}{\rho}G(\rho)$ with $G(s) = \pi^{-s/2}\Gamma(s/2)H(s)$. We assume there exists a holomorphic function $W(s)$, nonvanishing in $0 \le \text{Re}(s) \le 1$, such that for all nontrivial zeros $\rho$,

$$b_{\rho}^{\text{ABC}} = W(\rho) b_{\rho}^{\text{Lean}},$$

where $W$ captures the additional factors (e.g., $(s-1)/s$ and $H(s)$) from the preprint coefficient, and both $W$ and $1/W$ have at most polynomial growth in $|\text{Im}(s)|$. This bridge allows transfer of Theorems A/B/C bounds to the Lean coefficient once Assumption 11.2 fixes $b_{\rho}^{\text{Lean}}$; it is complementary to ExplicitBRhoExpression.

**Remark 11.4** (Mapping to the $H(s)$ factor). In the A/B/C preprint we write

$$b_{\rho}^{\text{ABC}} := \frac{\rho - 1}{\rho} G(\rho), \quad G(s) := \pi^{-s/2} \Gamma\left(\frac{s}{2}\right) H(s).$$

For ERURH, the factor $H(s)$ is the Mellin transform of the ERU kernel and auxiliary weights from the explicit formula. Under the normalization above, the Lean coefficient $b_{\rho}^{\text{Lean}}$ is exactly the gamma prefactor, while the remaining factors $(\rho-1)/\rho$ and $H(s)$ are carried by $b_{\rho}^{\text{ABC}}$ (equivalently by $W$ in Assumption 11.3). We assume $H(\rho) \neq 0$ in the analytic preprint to avoid trivial coefficients, so the analytic assumptions on $H(s)$ in the preprint (H1-H3) apply verbatim. The bridge between $b_{\rho}^{\text{ABC}}$ and $b_{\rho}^{\text{Lean}}$ is recorded in Assumption 11.3.

**Remark 11.5** (Nonvanishing for the Buchstab kernel). The alpha bridge data use the multiplicative averaging kernel $(\mathcal{T}h)(u) = \frac{1}{u} \int_{u/3}^{u/2} h(t) dt$, whose Mellin multiplier is $m(s) = (2^{-s} - 3^{-s})/s$ (Lemma 5.5). For $\Re(s) > 0$, Lemma 5.5 gives $m(s) \neq 0$, so the kernel contribution to $H(s)$ does not vanish on nontrivial zeros. The remaining nonvanishing requirement in Assumption 11.2 concerns only auxiliary holomorphic weights carried by $H(s)$ in the analytic preprint (hence by $W$), while Lean keeps $b_{\rho}^{\text{Lean}}$ as the gamma prefactor.

**Assumption 11.6** (Spectral decay: $H_b$). The coefficient family $\{b_{\rho}^{\text{ABC}}\}$ satisfies: (i) a pointwise polynomial (or exponential) bound in $|\gamma|$; (ii) a dyadic $L^2$ tail bound

$$\sum_{T < |\gamma| \le 2T} |b_{\rho}^{\text{ABC}}|^2 \le CT(\log T)^A$$

for sufficiently large $T$.

**Assumption 11.7** (Large-sieve for zero ordinates). For each dyadic band $T < |\gamma| \le 2T$ and each $L \ge 1$,

$$\frac{1}{L} \int_{0}^{L} \left| \sum_{T < |\gamma| \le 2T} b_{\rho}^{\text{ABC}} e^{i\gamma u} \right|^2 du \ll (\log T) \sum_{T < |\gamma| \le 2T} |b_{\rho}^{\text{ABC}}|^2.$$

This is a standard large-sieve inequality for separated exponentials combined with local zero counting.
**Definition 11.8 (Admissible window family).** A family of windows $w = [S, S+L]$ with $1 \ll L \ll S^\alpha$ is called *admissible* if it is cofinal: for every $S_0$ there exists a window with $S \ge S_0$ and $1 \ll L \ll S^\alpha$.

**Assumption 11.9 (RMS window hypotheses).** Fix an admissible window family (Definition 11.8) of windows $w = [S, S+L]$. Assume $1 \ll L \ll S^\alpha$ for each window. There exist RMS quantities RMS$_\alpha$, RMS$_{mode}$, RMS$_{low}$, RMS$_{tail}$ and constants $c_{low}$, $c_{tail}$, $C_{env}$ such that:

* **A1 (mode $\Rightarrow$ window bridge):** for every $\beta > 1/2$, if ERU\_mode\_beta($\beta$) holds then there exist an admissible window $w$ and a constant $K$ with $K > c_{low} + c_{tail} + C_{env}$ such that RMS$_{mode}(w) \ge K$.

* **A2-low:** for every admissible window $w$, RMS$_{low}(w) \le c_{low}$.

* **A2-tail:** for every admissible window $w$, RMS$_{tail}(w) \le c_{tail}$.

* **Decomposition:** for every admissible window $w$,

$$ \text{RMS}_{\alpha}(w) \ge \text{RMS}_{\text{mode}}(w) - \text{RMS}_{\text{low}}(w) - \text{RMS}_{\text{tail}}(w). $$

These hypotheses are the analytic inputs of the Plan B RMS-local route. In particular, A1 is formulated as a *conditional bridge*: it produces a witness window only under the presence of a putative supercritical mode, and therefore does not assert an RMS violation in the closed-gate regime. The admissibility (cofinality) of the window family is part of the window model, not an extra analytic assumption.

**Assumption 11.10 (Fixed-window threshold control).** Let $S_{max}$ denote the maximal lower end-point among the fixed $\text{ctx\_real}$ windows (Lean: windowMinMax). For every $\beta > 1/2$, if ERU\_mode\_beta($\beta$) holds then there exists $s_0 \le S_{max}$ such that for all $s \ge s_0$, $|\log R_\alpha(s)| \ge \exp((\beta - 1/2)s)$. This is precisely the Lean predicate ERURH. Alpha. ModeThresholdControl OnCxtRealWindowFamily.

**Remark 11.11.** This is a paper-level analytic assumption. The gate certifies the numeric inequality $S_{max} \ge s_0$ once the threshold control is supplied, but it does not prove the analytic implication from ERU\_mode\_beta to that bound. We provide a discussion of the analytic gap; a full proof is deferred to a supplement.

**Discussion (analytic gap for Assumption 11.10).** Step 1. Unpack ERU\_mode\_beta($\beta$) to obtain a threshold $s_0$ such that $|\log R_\alpha(s)| \ge \exp((\beta - 1/2)s)$ for all $s \ge s_0$.

Step 2. Establish an analytic upper bound on $s_0$ in terms of explicit-formula data (e.g., via a lower bound on the relevant mode coefficient and its contribution to $\log R_\alpha$). This is the only genuinely analytic input in the fixed-window bridge.

Step 3. Use the gate-certified numerical inequality $S_{max} \ge s_0$ to conclude $s_0 \le S_{max}$, which is exactly Assumption 11.10. The gate input is read from formal_report_analytic.json.

**Remark 11.12.** In the legacy window-free route, A1 is supplied by Lemma 5.4, while A2-low and A2-tail are discharged by Lemma 10.4 from the classical inputs.

**Assumption 11.13 (Numeric certificates).** The alpha certificates (GlobalEnergy and Kernel-Blowup) are correct, and the numeric coverage assumptions required to close the renormalization gates hold. In particular, the coverage asserts that for every admissible window $w$ in the covered family (the Lean predicate NumericCoverageAlpha), we have RMS$_\alpha(w) \le C_{env}$, i.e., the renormalization gate is closed on that family. These are finite rational inequalities generated by the ERURH pipeline.
**Assumption 11.14** (Beta inertia package). The beta-layer numerical inertia certificates are correct and supply any additional numeric bounds required by the pipeline. This package is external and is not used in the core alpha implication, but is included for completeness of the ERURH pipeline.

## 12 Plan B: RMS-local route

The Plan B proof decomposes the RMS of the ERU observable into mode/low/tail contributions. The following lemma is formalized in ERURH_A2Hypotheses.lean.

**Lemma 12.1** (Supercritical mode forces an RMS violation). Assume Assumption 11.9. Let $\beta > 1/2$. If ERU_mode_beta($\beta$) holds, then there exists a window $w$ with $\text{RMS}_{\alpha}(w) > C_{\text{env}}$.

*Proof.* Assume $\beta > 1/2$ and ERU_mode beta($\beta$). By the A1 clause of Assumption 11.9, choose an admissible window $w$ and $K$ such that $K > c_{\text{low}} + c_{\text{tail}} + C_{\text{env}}$ and $\text{RMS}_{\text{mode}}(w) \ge K$. Using the decomposition inequality and the A2-low/tail bounds from Assumption 11.9, we obtain

$$ \begin{aligned} \text{RMS}_{\alpha}(w) &\ge \text{RMS}_{\text{mode}}(w) - \text{RMS}_{\text{low}}(w) - \text{RMS}_{\text{tail}}(w) \\ &\ge K - c_{\text{low}} - c_{\text{tail}} \\ &> C_{\text{env}}. \end{aligned} $$

This is the desired RMS violation. □

A window whose RMS exceeds the envelope forces a renormalization gate to open. This is a direct consequence of the definition of the gate predicate.

**Lemma 12.2** (RMS violation opens a gate). If $\text{RMS}_{\alpha}(w) > C_{\text{env}}$ for some window $w$, then the renormalization gate is open.

The correctness of the certificates (Assumption 11.13) closes the renormalization gates; thus the RMS violation is incompatible with the closed gate regime. Consequently, under Assumptions 11.9, D.1, and 11.13, supercritical modes cannot exist.

## 13 Proof of the main theorem

We now prove Theorem 3.1. This is the mathematical counterpart of the Lean theorem RH_from_ERURH_conditional.

*Proof of Theorem 3.1.* By Proposition 5.1, there are no ERU exponential modes with weight > 1/2. The Lean lemma InertiaERU_alpha_strong_of_no modes via certificates yields strong ERU inertia from the absence of modes (using Assumption 11.13). Finally, the formal equivalence between strong ERU inertia and RH for $\xi_{\alpha}$ (under Assumption 11.1) gives RH. □

**Remark 13.1.** Assumptions 11.2–11.7 are classical analytic inputs (derivable from explicit formula technology, Stirling estimates, bounds for $\zeta'/\zeta$, and Riemann–von Mangoldt zero counts). The ERURH proof is a formal reduction: once these analytic statements and the finite certificates are established, RH follows mechanically.

**Remark 13.2.** In the Lean master statement, the Plan B window hypotheses are packaged as named fields hA1, hLow, and hTail inside WindowScalingAssumptions, with types A1_modectx, A2Low_RMSctx, and A2Tail_RMSctx. In this paper, Assumption 11.9 is formulated so that the
A1 clause is a mode-to-window bridge rather than an unconditional witness. This matches the intended analytic semantics: A1 produces a window only under a putative supercritical mode, so it is compatible with the closed-gate regime.

**Remark 13.3.** With A1 formulated as an implication from ERU_mode_beta to a witness window, the core Plan B contradiction has the standard form:

$$ (\exists \beta > 1/2 \text{ supercritical mode}) \Rightarrow (\exists w \text{ RMS violation}) \Rightarrow \text{gate opens,} $$

which contradicts gate closure from the finite certificates. Thus the conditional theorem is not vacuous: the hypotheses do not force an RMS violation unless a supercritical mode exists.

# 14 Formal status and gaps

The ERURH development separates formal logic from external analytic and numeric inputs. The current status can be summarized as follows.

* **Formalized in Lean:** definitions of the ERU observables, energy/inertia machinery, gate predicates, and the Plan B RMS-local chain. The conditional theorem is RH_from_ERURH \_conditional.

* **External classical assumptions:** explicit formula, functional equation, bounds for $\zeta'/\zeta$, and Riemann-von Mangoldt zero counts (Assumption 11.1). The explicit-formula framework for $b_{\rho}^{\text{Lean}}$ and the coefficient bridge to $b_{\rho}^{\text{ABC}}$ (Assumptions 11.2 and 11.3).

* **Analytic gap statements (Lean):**

- ERURH.A1_from_supercritical_buchstab ctx_real (A1 bridge, legacy window-free).

- ERURH.MODERMSLowerBound_from_buchstab ctx_real (mode lower bound via Buchstab).

- ERURH ALPHA.MODETHRESHOLDCONTROL OnCxtRealWindowFamily (fixed-window threshold control).

- ERURH.ExplicitBRhoExpression (explicit-formula coefficient identification).

Paper proofs cover the legacy A1 bridge and the A2 derivation from Theorems 10.1-10.3. The Buchstab-specific gaps and the explicit coefficient identification remain explicit assumptions for the optional Buchstab route, and the fixed-window threshold control is kept as a documented assumption. Full proofs of Theorems 10.1-10.3 are included in the bundled preprint Theorem_ABC_preprint.tex.

* **Numeric inputs:** correctness of the finite certificates and numeric coverage assumptions (Assumption 11.13), which are generated by the ERURH pipeline as exact rational data.

# Routes and scope clarification

Two complementary routes are presented.

* **Primary route (legacy, window-free).** This is the main route. It works in the abstract RMS context and does not require a fixed window family or computational threshold control. The window-free route is the core conceptual and logical chain of the reduction.
* **Secondary route (fixed-window, computational).** This alternative route anchors the RMS chain to a certified finite window family. It introduces additional hypotheses, including fixed-window threshold control. When instantiated via the Buchstab bridge, it also uses the coefficient-identification bridge *ExplicitBRhoExpression*. It is experimental and not required for the primary route.

The inclusion of the secondary route is not meant to compensate for a gap in the primary argument, but to illustrate how the ERU framework can be instantiated in a fully reproducible computational setting.

# 15 Formalization and reproducibility

The definitions and implications above are formalized in Lean. The main logical entry points are:

* `ERURH_MasterTheoremSummary.lean`: `RH_from_ERURH_conditional`.

* `ERURH_MasterTheoremPlanB.lean`: Plan B RMS-local route.

* `ERURH_A2Hypotheses.lean`: A1/A2 hypotheses and RMS decomposition.

* `ERURH_GatesAlpha.lean` and `ERURH_GatesFromRMS.lean`: gate closure and RMS-to-gate implications.

* Reproducibility gate: `scripts/verify gate.py` regenerates artifacts and checks the Lean build against the current certificate data.

The certificates are generated by reproducible scripts and imported as exact rational data. The Lean theorem itself does not execute floating-point arithmetic; interval arithmetic is used only in the external pipeline to produce the rational certificates.

# 16 Conclusion

ERURH provides a formal, conditional path from explicit-formula analysis to RH. All non-ERURH analytic content is isolated in a short list of assumptions, and all ERURH-specific reasoning is formalized. The remaining work is to supply proofs (or certified bounds) for the analytic assumptions and to validate the finite certificates with fully verified numerical pipelines.

## A Dependency map

This appendix summarizes the logical dependencies among the main components. Arrows indicate implication or usage.

### High-level chain

* Classical zeta inputs (Assumption 11.1) together with the ERU explicit-formula assumption (Assumption 11.2) supply the explicit-formula layer for $\log R$ and $J_{rel}$.

* Classical estimates (Theorems 10.1–10.3) ⇒ spectral decay and large-sieve inputs (Assumptions 11.6–11.7).
* A1/A2 window hypotheses (Assumption 11.9) plus a putative supercritical mode `ERU_mode Beta(β)` ⇒ RMS violation; the window-coverage bridge (Assumption D.1) selects a certified window, hence the gate opens.

* Certificates (Assumption 11.13) ⇒ gate closed.

* RMS violation and gate closed ⇒ contradiction; in the Plan B chain this excludes supercritical modes under A1/A2.

* No supercritical mode ⇒ strong inertia ⇒ RH for $ξ_α$ (using Assumption 11.1).

## Lean file map

* Main theorem: `lean/formal_proofs/ERURH/ERURH_MasterTheoremSummary.lean` (theorem `RH_from_ERURH_conditional`).

* Plan B chain:

`lean/formal_proofs/ERURH/ERURH_MasterTheoremPlanB.lean`

`lean/formal_proofs/ERURH/ERURH_A2Hypotheses.lean`.

* Gates:

`lean/formal_proofs/ERURH/ERURH_GatesAlpha.lean`

`lean/formal_proofs/ERURH/ERURH_GatesFromRMS.lean`.

* Assumption bundles:

`lean/formal_proofs/ERURH/ERURH_ClassicalZetaAssumptions.lean`

`lean/formal_proofs/ERURH/ERURH_ExplicitFormulaAlpha.lean`

`lean/formal_proofs/ERURH/ERURH_LargeSieveGammaSketch.lean`.

* Certificates:

`lean/formal_proofs/ERURH/EnergyCertificatesAlpha.lean`

`lean/formal_proofs/ERURH/InertiaCertificatesAlpha.lean`.

# B Proof obligations

This appendix records the remaining Lean-exported hypotheses required for the Route B closure. The machine-generated statements are included below.

ERURH.A1_from_supercritical_buchstab ERURH Alpha.GeneratedRMSContext.ctx_real : Prop
ERURHkarhModeRMSLowerBound_from_buchstab ERURH Alpha.GeneratedRMSContext.ctx_real : R → R → Prop
ERURHAlphakarhModeThresholdControlOnCtxRealWindowFamily : Prop
ERURHExplicitBRhoExpression : Prop

A field-by-field map from the Lean hypotheses to the paper proofs is maintained in the repository at docs/core/P9_PAPER_PROOF_MAP.md.
## C Normalization and Lean mapping for $b_{\rho}^{\text{Lean}}$ and $b_{\rho}^{\text{ABC}}$

This appendix fixes the normalization of the explicit-formula coefficients and records the exact Lean correspondence. In the companion preprint we define

$$b_{\rho}^{\text{ABC}} := \frac{\rho - 1}{\rho} G(\rho), \quad G(s) := \pi^{-s/2} \Gamma\left(\frac{s}{2}\right) H(s),$$

where $H(s)$ is a holomorphic factor encoding the ERU kernel normalization and any auxiliary weights. In the Lean development, $b_{\rho}^{\text{Lean}}$ is an abstract coefficient attached to a zero, and the explicit-formula identification is packaged by `HbExplicitData.h_b_rho`. The function `explicit_b_rho_expression` is defined as the gamma prefactor `gamma_prefactor`, i.e. $\pi^{-\rho/2}\Gamma(\rho/2)$. Any remaining holomorphic factors are absorbed into the preprint's $H(s)$ (equivalently $W$ in Assumption 11.3), while $b_{\rho}^{\text{Lean}}$ remains the gamma prefactor in Lean. Under Assumptions 11.2 and 11.3, the chosen normalization matches the Lean predicate `ERURH.ExplicitBRhoExpression`.

<table><thead><tr><th>Paper object</th><th>Lean name</th></tr></thead><tbody><tr><td>$\rho = \beta + i\gamma$</td><td>ERURH Alpha ZeroOfZeta (fields beta, gamma)</td></tr><tr><td>$b_{\rho}^{\text{ABC}}$</td><td>analytic coefficient in the A/B/C preprint</td></tr><tr><td>$b_{\rho}^{\text{Lean}}$</td><td>ERURH Alpha b_rho</td></tr><tr><td>$\pi^{-\rho/2}\Gamma(\rho/2)$</td><td>ERURH Alpha gamma_prefactor</td></tr><tr><td>Explicit identification $b_{\rho}^{\text{Lean}} =$</td><td>ERURH Alpha HbExplicitData.h_b_rho</td></tr><tr><td>explicit b<sub>ρ</sub>(ρ)</td><td></td></tr><tr><td>Bridge $b_{\rho}^{\text{ABC}} = W(\rho)b_{\rho}^{\text{Lean}}$</td><td>Assumption 11.3</td></tr><tr><td>Explicit formula package</td><td>ERURH ExplicitBRhoExpression</td></tr></tbody></table>

This normalization is the bridge between the analytic preprint (A/B/C) and the Lean formalization: the analytic estimates apply to the same coefficients once the explicit identification and the bridge assumption are fixed.

### Buchstab kernel factor for the alpha bridge

The alpha bridge data use the multiplicative averaging kernel $(Th)(u) = \frac{1}{u} \int_{u/3}^{u/2} h(t) dt$. For $h(t) = t^{s-1}$, the Mellin multiplier is

$$m(s) = \frac{2^{-s} - 3^{-s}}{s}, \quad 2^{-s} := \exp(-s \log 2),$$

so the kernel contribution to $H(s)$ is $m(s)$. For $\text{Re}(s) > 0$, Lemma 5.5 gives $m(s) \neq 0$. Thus the only remaining nonvanishing requirement in Assumption 11.2 concerns auxiliary holomorphic weights absorbed into $H(s)$.

## D Hypotheses glossary (Lean $\leftrightarrow$ paper)

For auditability we spell out the main predicates exactly as they are used in Lean.

* `ERU_mode_beta` ($\beta$): with $\beta > 1/2$, there exists $s_0 > 0$ such that for all $s \ge s_0$, the mode contribution in `logR_alpha` satisfies the exponential lower bound against the fixed polynomial divisor used in the Lean definition. Domain: $s \in \mathbb{R}_{\ge 0}$; no uniform bound in $\beta$ is claimed.
* **A1_mode (ctx):** the mode-to-window bridge: for any supercritical mode ERU_mode beta($\beta$) with $\beta > 1/2$, there exists an admissible window $w$ in the family of RMSLocalContext $\text{ctx}$ such that the mode RMS, RMS_mode($\text{ctx}, w$), exceeds the explicit threshold (of size $\exp((\beta - \frac{1}{2})S)/S^2$ in the window). The conclusion RMS_α($w$) > $C_{\text{env}}$ is obtained later by combining A1_mode with A2Low_RMS, A2Tail_RMS, and the decomposition RMS_decomp.

* **A2Low_RMS (ctx) and A2Tail_RMS (ctx):** inequalities (not equalities) controlling the low and tail parts of the RMS decomposition over the same admissible window family, with constants $C_{\text{low}}$, $C_{\text{tail}}$ fixed by $\text{ctx}$.

* **NumericCoverageAlpha (ctx_real):** certifies a finite set of admissible windows $W_{\text{cert}}$ sufficient for Route B; the gate only enforces RMS bounds on this finite family.

* **Gate statement (Route B):** for all $w \in W_{\text{cert}}$, $\text{RMS}_\alpha(w) \le C_{\text{env}}$, with $C_{\text{env}}$ the envelope constant of $\text{ctx_real}$.

### Coefficient normalisation $b_\rho$.

We distinguish the Lean coefficient $b_\rho^{\text{Lean}}$ and the analytic preprint coefficient $b_\rho^{\text{ABC}}$. The Lean predicate ExplicitBRhoExpression records the normalization $b_\rho^{\text{Lean}} = \pi^{-\rho/2}\Gamma(\rho/2)$. The analytic preprint uses $b_\rho^{\text{ABC}} := (\rho-1)/\rho \cdot G(\rho)$ with $G(s) = \pi^{-s/2}\Gamma(s/2)H(s)$, so the additional holomorphic factors live in $b_\rho^{\text{ABC}}$. The bridge between the two is declared explicitly in Assumption 11.3. If another normalization is used elsewhere, the equality (or a bound) must be stated explicitly.

**Assumption D.1 (Window coverage bridge).** Let $W_{\text{cofinal}}$ be the admissible window family for the context $\text{ctx_real}$. This is the family in which A1_mode witnesses a window under ERU_mode beta. Let $W_{\text{cert}}$ be the finite window family certified by NumericCoverageAlpha for $\text{ctx_real}$. We assume $W_{\text{cert}}$ is cofinal in $W_{\text{cofinal}}$ (or contains an equivalent representative) so that any A1-produced window can be chosen in $W_{\text{cert}}$. This bridge is required to combine A1 with the finite gate certificates.

## E Verification of H1–H3 for the ERU kernel

This short appendix explains why the hypotheses (H1)–(H3) used in Theorem_ABC_preprint.tex are reasonable for the ERU kernel in the ERURH setting.

### H1 (holomorphic model with gamma factor).

The explicit-formula package (Assumption 11.2) identifies the coefficients with the completed zeta prefactor $\pi^{-\rho/2}\Gamma(\rho/2)$ under the chosen normalization. The remaining kernel-dependent factor is absorbed into $H(s)$ in the preprint, matching the model $G(s) = \pi^{-s/2}\Gamma(s/2)H(s)$.

### H2 (polynomial growth of $H$).

For the ERU kernel, $H(s)$ is a Mellin transform of a smooth compactly supported test function and auxiliary weights. Such Mellin transforms are holomorphic in vertical strips and grow at most polynomially in $|\Im s|$. This is the standard setting of explicit-formula derivations (see [1] and the remark on hypothesis verification in the preprint).

### H3 (Riemann-von Mangoldt and local zero counts).

The unit-interval zero count bound is a direct consequence of the classical Riemann-von Mangoldt formula and is standard; see [1] and [2]. This is the only zero-distribution input in Theorem B.
References

[1] E. C. Titchmarsh, *The Theory of the Riemann Zeta-Function*, 2nd ed., revised by D. R. Heath-Brown, Oxford University Press, 1986.

[2] H. L. Montgomery and R. C. Vaughan, *Multiplicative Number Theory I. Classical Theory*, Cambridge University Press, 2007.

[3] A. Ivic, *The Riemann Zeta-Function: Theory and Applications*, Dover, 2003.