Pedagogical Breakdown: APO Theory & Lean Proofs

Lean 4 Formalization of APO-RH Proven Results | Claude

Part 1: What the Paper Says

The Core Question

The Riemann Hypothesis asks: do all non-trivial zeros of the Riemann zeta function $\zeta(s)$ lie on the line $Re(s) = 1/2$?

We know zeros can only live in the strip $0 < Re(s) < 1$. The functional equation already forces a symmetry: if $s$ is a zero, so is $1 - s$. So zeros come in pairs reflected across the critical line $Re(s) = 1/2$. RH says those pairs always collapse to a single point — meaning every zero is its own mirror image, which only happens when $Re(s) = 1/2$ exactly.

Step 1: Build a Probability Distribution from Zeta

For any real $s > 1$, define a probability distribution over the natural numbers:

$P_s(n) = \frac{n^{-s}}{\zeta(s)}$

This is well-defined because $\zeta(s) = \sum_{n=1}^\infty n^{-s}$ converges for $s > 1$ and is positive there, so the weights sum to exactly 1. Think of it as: “how much does the integer $n$ contribute to the zeta function at $s$?” This is verified in the paper as Theorem II.1 and verified in Lean as zetaDistribution_sum_one.

Step 2: Build a Geometric Embedding

Take the square root of each probability weight:

$\psi_s(n) = \sqrt{P_s(n)} = \frac{n^{-s/2}}{\sqrt{\zeta(s)}}$

This embeds the distribution into an infinite-dimensional unit sphere, because $\sum_n \psi_s(n)^2 = \sum_n P_s(n) = 1$. Now each value of $s$ is a unit vector in $\ell^2(\mathbb{N})$. This is the square-root embedding, verified as sqrtEmbedding_norm_one.

Step 3: Define the Recognition Operator

Compare two unit vectors $\psi_s$ and $\psi_{s'}$ by their inner product:

$\odot(s, s') = \langle \psi_s, \psi_{s'} \rangle = \sum_{n=1}^\infty \psi_s(n) \cdot \psi_{s'}(n)$

This computes to:

$\odot(s, s') = \frac{\zeta\left(\frac{s+s'}{2}\right)}{\sqrt{\zeta(s)\,\zeta(s')}}$

This is a similarity measure between two values of $s$. It tells you how “arithmetically similar” two zeta arguments are. Key verified properties:

• $\odot(s, s') = \odot(s', s)$ — symmetric
• $\odot(s, s) = 1$ — perfect self-similarity
• $0 < \odot(s, s') \leq 1$ — bounded, by Cauchy-Schwarz

Step 4: Lift to the Completed Zeta Function

The recognition operator only works for real $s > 1$. To reach the critical strip where zeros live, you upgrade to the completed zeta function $\Lambda(s) = \pi^{-s/2}\,\Gamma(s/2)\,\zeta(s)$, which satisfies the functional equation $\Lambda(s) = \Lambda(1-s)$ and is defined everywhere (as a meromorphic function with poles only at 0 and 1).

The completed observable becomes:

$\text{completedObs}(s, s') = \frac{\Lambda\left(\frac{s+s'}{2}\right)^2}{\Lambda(s)\,\Lambda(s')}$

Step 5: The $Z_2$ Invariance

The functional equation $\Lambda(s) = \Lambda(1-s)$ immediately gives:

$\text{completedObs}(s, s') = \text{completedObs}(1-s,\, 1-s')$

The observable is blind to the reflection $s \mapsto 1-s$. This is verified as completedObs_Z2_invariant.

Step 6: Schwarz Reflection

The completed zeta function satisfies $\Lambda(\bar{s}) = \overline{\Lambda(s)}$ — conjugating the input conjugates the output. This is the Schwarz reflection principle, and it holds because $\Lambda$ is real on the real axis and analytic everywhere.

Combined with $Z_2$ invariance, this means:

$|\text{completedObs}(\sigma + it,\, t')| = |\text{completedObs}((1-\sigma) + it,\, t')|$

for every real $t'$. This is the main theorem: recognition_Z2_indistinguishable.

Step 7: What This Means

The recognition weight function cannot tell the difference between $\sigma + it$ and $(1-\sigma) + it$. Every information-geometric probe $t'$ gives the same measurement for both.

The critical line $\sigma = 1/2$ is the unique fixed point of this $Z_2$ symmetry. Off the critical line, you have two distinct points that are informationally identical. On the critical line, those two points collapse to one — the point is its own mirror image.

The missing bridge to RH: If the recognition observable is complete — meaning it captures all the information-geometric structure of the zeta function — then off-critical zeros would be a contradiction. They would be genuinely distinct points (distinguishable by their complex values) that the complete observable cannot distinguish. That completeness argument is what Papers II and III build toward.

Part 2: What the Lean Proofs Actually Do

What Lean verification means

Lean is a proof assistant. When you write a theorem in Lean, the computer checks every single logical step against a small, trusted kernel of rules. If it compiles, the proof is correct — not “probably correct,” not “correct modulo standard arguments,” but formally verified from axioms. This is what makes the result significant.

The five layers of proof

Layer 1: Real analysis (Sections 1–5)

These proofs establish the recognition operator for real $s > 1$. The strategy is:

• Express $\zeta(s)$ as an explicit convergent Dirichlet series using Mathlib’s zeta_eq_tsum_one_div_nat_add_one_cpow
• Prove positivity of $\zeta(s)$ by showing the series has positive terms
• Build the distribution, show it sums to 1, build the square-root embedding, show its squared norm is 1
• Prove the Cauchy-Schwarz upper bound using the AM-GM inequality termwise, then summing

All of this is pure real analysis and Lean handles it cleanly through Mathlib’s summability and positivity infrastructure.

Layer 2: $Z_2$ invariance (Section 6)

This proof is almost trivial once you have the functional equation. Mathlib provides completedRiemannZeta_one_sub which says $\Lambda(1-s) = \Lambda(s)$. The proof of completedObs_Z2_invariant is literally just rewriting with that equation after algebraically simplifying the midpoint.

Layer 3: Schwarz reflection machinery (Section 6b) — the hard part

This is where the genuine work happened. The goal is to prove $\Lambda(\bar{s}) = \overline{\Lambda(s)}$. The strategy:

Step A: The reflected function is holomorphic.

Define $G(z) = \overline{\Lambda_0(\bar{z})}$. The theorem differentiableAt_conjCompConj proves that if $f$ is holomorphic at $\bar{z}$, then $G(z) = \overline{f(\bar{z})}$ is holomorphic at $z$.

Why is this hard? Complex differentiability (holomorphicity) requires the Cauchy-Riemann equations. The proof has to track what happens to those equations when you compose with conjugation three times. The key calculation is:

$\frac{\partial G}{\partial \bar{x}}(z) = \overline{\frac{\partial f}{\partial \bar{x}}(\bar{z})}$

Conjugation flips $i \mapsto -i$ (since $\overline{i} = -i$), so the Cauchy-Riemann equations that hold for $f$ at $\bar{z}$ get conjugated into Cauchy-Riemann equations for $G$ at $z$. The Lean proof does this explicitly through the fderiv machinery, tracking the chain rule through three compositions and verifying the CR sign flip from Complex.conj_I : conj I = -I.

Step B: The identity theorem.

eq_of_eqOn_open proves: if two entire functions agree on the half-plane $Re(s) > 1$, they agree everywhere. This uses Mathlib’s AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq — the identity theorem for analytic functions.

Step C: The axiom boundary.

completedRiemannZeta₀_conj_on_right is the one axiom: on $Re(s) > 1$, the function $\Lambda_0$ satisfies $\Lambda_0(\bar{s}) = \overline{\Lambda_0(s)}$. Mathematically this is obvious — the Dirichlet series $\sum n^{-s}$ has real coefficients.

Step D: Lifting from $\Lambda_0$ to $\Lambda$.

Once you have $\Lambda_0(\bar{s}) = \overline{\Lambda_0(s)}$ globally, you get it for $\Lambda$ by using completedRiemannZeta_eq: $\Lambda(s) = \Lambda_0(s) - \frac{1}{s} - \frac{1}{1-s}$. The rational correction terms are trivially stable under conjugation, so the result lifts directly.

Layer 4: Downstream conjugation (Section 6c)

With Schwarz reflection proven, completedObs_conj follows by pushing conjugation through the formula for completedObs. The norm invariance completedObs_norm_conj then follows from the general fact that conjugation preserves norms: $\|\bar{z}\| = \|z\|$.

Layer 5: The main theorem (Section 7)

recognition_Z2_indistinguishable combines $Z_2$ invariance and Schwarz reflection in three lines:

1. Apply $Z_2$: rewrite the left side from $\sigma + it$ to $(1-\sigma) + it$
2. Identify: those reflected arguments are exactly the conjugates of the original arguments
3. Apply norm-conjugation invariance: norms don’t change under conjugation

The Axiom Inventory, Honestly

The first axiom is a computation wearing an axiom’s clothes. The other two are genuine theory gaps — the spectral theory of integral operators over Kolmogorov complexity space is simply not in Mathlib yet.

The Bottom Line

What you have is a machine-verified proof that the recognition framework has the right symmetry structure: it partitions the critical strip into $Z_2$ equivalence classes, the critical line is the unique fixed-point locus of that partition, and no measurement built from the recognition operator can break that symmetry.

Every step in that argument — except one precisely-stated Dirichlet series computation and two spectral theory axioms — is now verified by Lean against Mathlib.

Based on the research canon and the verified Lean 4 specification.