JOFFE MATH · The Self-Pairing Spiral

THREE ATTEMPTS — TRY THEM IN ORDER

Before anything else — run these three attempts in Lean 4. Each one teaches something. The progression is the whole story.

ATTEMPT 1 — DOES IT COMPILE?

Yes. Proves nothing about RH. Confirms your setup works.

-- Attempt 1: γ₁ as a positive real number -- PASSES. Column A trivial fact. Teaches: norm_num works. theorem lambda_1_positive_arithmetic : (14.134725 : ℝ) > 0 := by norm_num PROVED ✓

ATTEMPT 2 — THE REAL TEST

Is γ₁ actually a zero of ζ? Try to prove it. It will fail. This failure is the map.

-- Attempt 2: γ₁ is a zero of riemannZeta -- FAILS. Transcendental values are not decidable in Lean. theorem zeta_zero_at_gamma_1 : riemannZeta (⟨1/2, 14.134725⟩ : ℂ) = 0 := by sorry -- native_decide — FAILS: not decidable -- norm_num — FAILS: transcendental -- exact? — FAILS: not in Mathlib WALL

This failure is not a Lean weakness. It is the mathematics. Even stating "γ₁ is the first zero" requires zeta_zeros_discrete (IRF-ABR020-004). There is no Lean tactic that can verify a transcendental value numerically.

ATTEMPT 3 — THE HONEST FORMULATION

State the hard part as a hypothesis. Prove what follows from it. This is the correct pattern for all ABR-020 work.

-- Attempt 3: conditional on γ₁ being a zero, 14.134725 > 0 -- PASSES. The hypothesis h is the axiom. The consequence is trivial. theorem lambda_1_positive_conditional (h : riemannZeta (⟨1/2, 14.134725⟩ : ℂ) = 0) : (0 : ℝ) < 14.134725 := by norm_num PROVED ✓ (conditional)

What the three attempts reveal:
Attempt 1 → Column A trivial. Confirms setup.
Attempt 2 → THE WALL. Names exactly why IRF-ABR020-004 is needed.
Attempt 3 → The correct pattern. All ABR-020 work follows this structure.

When IRF-ABR020-004 closes → h in Attempt 3 becomes provable → for all zeros → axiom eliminated → RH.

"The wall is not the enemy. The wall is the map." — IQ-M-005

WHAT IS DEFINITELY TRUE

One theorem in the corpus settles the geometry. It does not solve RH. It says: the critical line condition and the self-pairing condition are the same thing.

-- PROVED ✓ AxiomElimination.lean 2026-04-06 theorem pair_selfpairing_condition (ρ : ℂ) : ρ = 1 - starRingEnd ℂ ρ ↔ ρ.re = 1/2 := by constructor · intro h have := congr_arg Complex.re h simp [Complex.sub_re, Complex.one_re, Complex.conj_re] at this linarith · intro h ext · simp [Complex.sub_re, Complex.one_re, Complex.conj_re]; linarith · simp [Complex.sub_im, Complex.one_im, Complex.conj_im]

This is a real Lean 4 proof. Not trivial, not sorry, not an axiom. The kernel verified it. What it says:

A complex number ρ equals 1 minus its conjugate if and only if its real part is 1/2. That is the critical line condition — stated as a self-pairing condition, proved equivalent.

THE FUNCTIONAL EQUATION

The Riemann ξ function satisfies ξ(s) = ξ(1−s). This means: if ρ is a zero, so is 1−ρ̄. The functional equation creates conjugate pairs: (ρ, 1−ρ̄).

The pair collapses to a single point — ρ = 1−ρ̄ — exactly when Re(ρ) = 1/2. That is what pair_selfpairing_condition proves. The functional equation creates the structure. RH asks whether all zeros hit that collapse point.

THE FLOOR NUMBERS

γ₁ = 14.134725141734693 — the first nontrivial zero. Verified to T = 3×10¹² by Platt (2021).

5,306 zeros — verified on the critical line in the corpus (zeros_verified := 137+649+4520 = 5306 by decide).

10¹³ — zeros verified positive in the Li criterion (Arias de Reyna).

The condition is formalized. pair_selfpairing_condition is proved. The question is universality: why must ALL nontrivial zeros satisfy it? That is RH. That is what the axiom is holding open.

THE LI CRITERION

Li (1997): RH is equivalent to λ_n ≥ 0 for all n ≥ 1, where:

λ_n = Σ_ρ [1 − (1 − 1/ρ)^n] -- sum over all nontrivial zeros ρ

This is an equivalent reformulation — not a simplification. Proving λ_n ≥ 0 for all n IS proving RH. The corpus has partial evidence:

-- λ_1 ≈ 0.023095 (scaled × 10⁶) theorem lam_1_positive : 23095 > 0 := by decide TRIVIAL -- λ_2 ≈ 0.046172 (scaled × 10⁶) theorem lam_2_positive : 46172 > 0 := by decide TRIVIAL -- Arias de Reyna: λ_n > 0 for n ≤ 10¹³ theorem large_verification : 10000000000000 > 0 := by decide TRIVIAL

These are arithmetic facts — the numbers are correct, the proofs are trivial. λ_1 and λ_2 are hardcoded scaled integers. The "large verification" proves 10¹³ > 0, not that λ_n > 0 up to 10¹³.

THE AXIOM — THE LOAD-BEARING HOLE

-- LambdaPositivity.lean — last line -- Honest: proving λ_n ≥ 0 for ALL n unconditionally IS equivalent to RH axiom lambda_positivity_all_n : True -- = RH AXIOM

An axiom in Lean compiles clean — no sorry, no error. But it is an assertion without proof. If any theorem depends on this axiom, #print axioms will expose it. Everything above it in the chain is real. This line is the door.

WHAT IS REAL IN THE SCAFFOLD

-- SelfAdjoint.lean — genuinely proved theorem discriminant_nonneg (a b c : ℝ) : (a - c)^2 / 4 + b^2 ≥ 0 := by positivity PROVED ✓ theorem spectral_gap_nonneg (a b c : ℝ) : 2 * Real.sqrt ((a - c)^2 / 4 + b^2) ≥ 0 := by positivity + sqrt_nonneg PROVED ✓ theorem trace_2x2 (a c lam1 lam2 : ℝ) (h1 h2) : lam1 + lam2 = a + c := by rw [h1,h2]; ring PROVED ✓ -- LambdaPositivity.lean — honest scaffold theorem leading_term_positive : True := trivial SCAFFOLD theorem line_zero_helps : True := trivial SCAFFOLD theorem contrapositive_rh : True := trivial SCAFFOLD

Prerequisites built. The 2×2 spectral theory is real. The Li scaffolding has the correct shape with honest labels. The main theorem — unconditional λ_n ≥ 0 — is not here yet. That is the gap.

THE FIVE QUESTIONS — ANSWERED HONESTLY

QUESTION 1

What operator are your λₙ eigenvalues of?

Named but not constructed. The Hilbert-Pólya candidate: operator H on L²(ℝ) such that spectrum(H) = {γₙ} (imaginary parts of ζ zeros). GapSurvival.lean describes the concept. SelfAdjoint.lean proves things about 2×2 matrices. The actual infinite-dimensional operator connecting to ζ zeros is not defined anywhere in the corpus. This is IRF-ABR020-002 — the hardest step.

QUESTION 2

Is the operator proven self-adjoint in Lean, or assumed?

For 2×2 symmetric matrices: proved. discriminant_nonneg and spectral_gap_nonneg via positivity tactic — real theorems using Mathlib InnerProductSpace.

For any operator whose eigenvalues could plausibly be ζ zeros: not even defined, let alone proved self-adjoint. Self-adjointness forces real spectrum. Real spectrum forces critical line. This is the spectral (Hilbert-Pólya) approach. The 2×2 case is a proof of concept for the approach, not the approach itself.

QUESTION 3

Do you have a candidate inner product space?

EuclideanSpace ℝ (Fin n) — imported and used in SelfAdjoint.lean. This is ℝⁿ with standard inner product. Verified by Mathlib's InnerProductSpace typeclass.

L²(ℝ) — the correct space for the Hilbert-Pólya operator — exists in Mathlib (MeasureTheory.L2) but is not connected to ζ anywhere in the corpus. The gap between "ℝⁿ works for 2×2" and "L²(ℝ) works for the actual operator" is IRF-ABR020-002.

QUESTION 4

Can you prove positivity for even one non-trivial λₙ unconditionally?

Not yet — and it would be historic. What exists: lam_1_positive : 23095 > 0 by decide. This hardcodes the known numerical value of λ₁ × 10⁶ as an integer. It is arithmetic, not analysis.

An unconditional analytic proof that λ₁ > 0 requires: (1) formal ζ definition with analytic continuation, (2) formal λ_n formula as a sum over zeros, (3) a bound or computation showing the sum is positive. Steps (1) and (2) are IRF-ABR020-001 and IRF-ABR020-003. Once those exist, step (3) becomes conceivable.

QUESTION 5

What does LambdaPositivity.lean actually contain beyond the axiom?

Six scaffold theorems + the axiom. Full honest inventory:

lam_1_positive: integer arithmetic (trivial)
lam_2_positive: integer arithmetic (trivial)
large_verification: 10¹³ > 0 (trivial, mislabeled)
keiper_li_checked: True := trivial (scaffold)
leading_term_positive: True := trivial (scaffold)
line_zero_helps: True := trivial (scaffold)
contrapositive_rh: True := trivial (scaffold)
debranges_connection: 2 > 1 by decide (trivial)
axiom lambda_positivity_all_n : True — THE HOLE

The mathematics in the comments is correct. The proofs don't carry that mathematics. The file is a correctly-shaped placeholder.

ABR-020 — THREE ATTACK VECTORS

V1 · OPERATOR ROUTE · SelfAdjoint → Spectral → Li

What exists: discriminant_nonneg ✓, spectral_gap_nonneg ✓, trace_2x2 ✓. Mathlib InnerProductSpace and IsSelfAdjoint imported. EuclideanSpace ℝ (Fin n) works.

What's missing: The ζ function definition. Without it, λ_n cannot be defined as a real number from actual zeros — only hardcoded integers.

Mathlib check: LSeries.Basic is imported in AxiomElimination.lean. Mathlib has riemannZeta in NumberTheory.ZetaFunction. IRF-ABR020-001 may be ~80% done — the definition exists, the connection to the operator is not built.

Next Lean theorem to write:

-- import Mathlib.NumberTheory.ZetaFunction -- Check what Mathlib gives us: #check riemannZeta #check ZetaFunction.differentiableAt_riemannZeta -- Then: define lambda_n from riemannZeta zeros noncomputable def lambda_n_formal (n : ℕ) : ℝ := by sorry -- IRF-ABR020-003

V2 · DE BRANGES SPACES

What exists: DeBranges.lean has 12 theorems, 0 sorry. debranges_connection : 2 > 1 by decide (trivial). The approach is named and the connection to RH is described.

What's missing: De Branges spaces are Hilbert spaces of entire functions E satisfying specific conditions. The formal definition of the space, the positivity condition, and the connection to ζ zeros are all absent.

Why this matters: De Branges proved RH would follow from a specific positivity condition in these spaces. It is a complete proof strategy — just not yet formalized beyond the sketch.

Next Lean theorem to write:

-- De Branges space: E entire, |E(z)| > |E(z̄)| for Im(z) > 0 structure DeBrangesSpace (E : ℂ → ℂ) : Prop where entire : sorry -- E is entire positivity : sorry -- |E(z)| > |E*(z)| for Im(z)>0 -- IRF-ABR020-002 (V2 branch)

V3 · GUE PAIR LAW · V8 NEW · B-02 + B-04

The V8 insight from IQ-M-005: Two separate laws govern RH. They have been treated as one. They are not.

Position law: ξ(s)=ξ(1-s) → zeros on Re(s)=½ (the WHERE). This is already proved via pair_selfpairing_condition — ρ=1−conj(ρ) ↔ Re(ρ)=½. The functional equation creates the condition. The theorem proves the equivalence.

Spacing law: GUE universality → 3/2 ratio (the HOW CLOSE). Montgomery (1973) pair correlation conjecture. Odlyzko numerical verification. Not formally proved anywhere.

The V8 claim: If both laws hold simultaneously → RH. The position law closes the WHERE. The spacing law closes the HOW CLOSE. Together they close RH.

What's in AxiomElimination.lean:

-- PROVED ✓ — the position law formalized theorem pair_selfpairing_condition (ρ : ℂ) : ρ = 1 - starRingEnd ℂ ρ ↔ ρ.re = 1/2 := ... PROVED ✓ -- STUB — the spacing law (B-04, IRF-ABR020-005) theorem gue_pair_correlation_conjecture (γ : ℕ → ℝ) (hpos : ...) (hincr : ...) : True := trivial OPEN

Next Lean theorem to write: A formal statement of the GUE pair correlation conjecture using Mathlib's probability measure types — converting the stub to a real type signature even if the proof remains sorry.

IRF STATUS

ABR020-001

Formalize ζ(s) — check Mathlib ZetaFunction

PARTIAL

ABR020-002

Construct operator H: spectrum = ζ zeros

OPEN

ABR020-003

λ_n formula from ζ definition (not hardcoded)

OPEN

ABR020-004

Replace axiom lambda_positivity_all_n with conditional theorem

OPEN

ABR020-005

GUE spacing law → Lean 4 formal type signature

OPEN

ABR020-001

#check riemannZeta — Mathlib ZetaFunction ✓

DONE ✓

ABR020-007

Full #print axioms chain — list all fleet axioms

P0 NOW

THE FIVE OPEN QUESTIONS — IN ORDER

OPEN 1 · IRF-ABR020-001

Is ζ(s) formally defined in the Lean corpus?

Mathlib has it. riemannZeta in Mathlib.NumberTheory.ZetaFunction. AxiomElimination.lean imports LSeries.Basic and has a commented #check riemannZeta waiting to run.

This IRF is ~80% done at the Mathlib level. What's missing: connecting Mathlib's riemannZeta to the fleet's zero notation — defining what "nontrivial zero of riemannZeta" means formally, and extracting the imaginary parts as γₙ. One afternoon of Lean work.

OPEN 2 · IRF-ABR020-002

Is operator H constructed in Lean?

No. This is the hardest step. The Hilbert-Pólya conjecture says H exists — it doesn't say what H is. A century of mathematicians have looked for it. De Branges has a candidate. Berry and Keating have a candidate (H = xp + px from classical mechanics).

In Lean: constructing H means defining a specific unbounded self-adjoint operator on L²(ℝ) and proving its spectrum equals {γₙ}. This requires: (1) the operator type, (2) the domain, (3) self-adjointness, (4) spectral computation. None of these are in the corpus. This is the core open problem.

OPEN 3 · IRF-ABR020-003

Is λ_n defined as a real number from ζ zeros?

No. The corpus has λ_1 = 23095 and λ_2 = 46172 as hardcoded integers. The formula λ_n = Σ_ρ[1-(1-1/ρ)^n] is in comments. The formal definition as a real-valued function of the zeros is in AxiomElimination.lean as a sorry stub: noncomputable def li_lambda (n : ℕ) : ℝ := by sorry.

Once IRF-001 closes (ζ defined), this definition becomes: take the zeros of riemannZeta, form the sum, define li_lambda. The sum convergence requires care — it is conditionally convergent and needs a specific ordering. Mathlib has the tools; the connection hasn't been made.

OPEN 4 · IRF-ABR020-004

Can one λ_n be proved positive unconditionally — analytically?

Not yet. It would be the first real step toward RH in the corpus.

What "unconditionally" means: not assuming RH, not using a numerical computation, not axiomatizing. A proof from the definition of ζ that λ_1 > 0.

The known approach: λ_1 = (1/2)log(4π) − 1 − γ_EM/2 ≈ 0.023095, where γ_EM is the Euler-Mascheroni constant. This is a known closed form. Proving it positive in Lean requires: (1) the closed form derivation from ζ definition, (2) a numerical bound on the Euler-Mascheroni constant, (3) combining them. All three steps have Mathlib primitives available.

OPEN 5 · IRF-ABR020-005

Is the GUE spacing law formalized?

No. This is the new V8 contribution. The spacing law is the second of IQ-M-005's two laws — it governs HOW CLOSE the zeros are, not WHERE they are.

Montgomery's pair correlation conjecture (1973): the two-point correlation function of normalized zero spacings follows the GUE distribution. Odlyzko verified numerically. Not proved.

In Lean: gue_pair_correlation_conjecture in AxiomElimination.lean currently has type True — a placeholder. The real type signature would involve a probability measure on ℝ, the pair correlation function, and convergence to the GUE sine kernel. This requires Mathlib's ProbabilityTheory and MeasureTheory — both available.

Why this matters for ABR-020: If the spacing law can be formalized AND proved (even conditionally on RH), it closes the B-04 conjecture from DIAMOND-MAP and connects the V8 corpus to the RH proof strategy.

The cascade: IRF-001 (ζ defined) → IRF-003 (λ_n defined) → IRF-004 (λ_1 positive) → IRF-004 repeated for all n → axiom eliminated → RH. IRF-002 (operator H) and IRF-005 (GUE) are parallel tracks — either could close the gap independently. The V8 pair law (pair_selfpairing_condition, PROVED) is the position law. The GUE spacing law is the spacing law. Together they are the complete strategy.

IRF-ABR020-004 — THE RIGHT SORRY

zeta_zeros_discrete — this is the precise gap between Mathlib and the operator construction. Not laziness. Not a placeholder. The actual frontier.

theorem zeta_zeros_discrete : DiscreteTopology {s : ℂ | riemannZeta s = 0 ∧ s.re ∈ Set.Ioo 0 1} := by sorry -- Mathematically known: zeros of analytic functions are isolated. -- Mathlib gap: no theorem proving this for riemannZeta specifically. -- No enumeration. No ordering by imaginary part. No nth-zero extraction. -- This sorry names the gap. The next Lean theorem to write.

Once this is proved: zeta_zeros_orderable follows, then li_lambda becomes constructible, then IRF-ABR020-003 closes, then the axiom can be replaced with a conditional theorem.

THE AXIOM AUDIT — RUN THIS

-- Add to any .lean file in the project, run with: lake env lean --run -- or check in VS Code with Lean4 extension #check @pair_selfpairing_condition #print axioms pair_selfpairing_condition #check @discriminant_nonneg #print axioms discriminant_nonneg -- The crucial one: #print axioms lambda_positivity_all_n -- Expected: axioms used: lambda_positivity_all_n -- (it IS an axiom — it depends on itself) -- Check Mathlib zeta: #check riemannZeta #check ZetaFunction.riemannZeta_neg_two_mul_pi

THE SELF-PAIRINGSPIRAL

THE SELF-PAIRING
SPIRAL