Content is user-generated and unverified.

PROOF_STRUCTURE_LEAN4.md — Lean 4 Formalization of APO-RH Proven Results

Created: April 8, 2026
Last updated: April 14, 2026 (v8.0 — 0 sorries, 20+ verified theorems)
Parent: APO Initiative — PROOF_STRUCTURE_RH.md
Working document: Sandbox/ApoRhSpec.lean (v8.0)
Companion: PROOF_STRUCTURE_RH.md (mathematical proof chain), ApoRhSpec.lean (logical specification)
Lean version: 4.29.0
Mathlib: current as of April 2026

Purpose

This document tracks the Lean 4 formalization status of results labeled PROVEN in APO-RH Paper I ("The Arithmetic Recognition Operator"). Only PROVEN results are formalized; ARGUED/CONJECTURED results are excluded by design.

Verification Summary

Metric	Count
`sorry` warnings	0
Theorems verified (standard axioms only)	17
Theorems verified (modulo Schwarz axiom A1)	+4
Custom axioms	3 (1 closeable, 2 blocked)
Axiomatized zeta functions	0 (all from Mathlib)

Axiom Inventory

#	Axiom	What it encodes	Closeable?
A1	`completedRiemannZeta₀_conj_on_right`	Dirichlet series has real coefficients → Λ₀(s̄) = Λ̄₀(s) on Re s > 1	Yes — finite computation via Dirichlet series term-by-term conjugation
A2	`solomonoffMeasure`	Spectral theory for integral operators	Blocked by Mathlib
A3	`kraft_inequality`	Bound on A2	Blocked by Mathlib

Key distinction: A1 is a verifiable computation. A2–A3 are genuine theory gaps. The analytic continuation from A1 to global Schwarz reflection is fully verified via the identity theorem.

Master Status Table

★ Verified — depends only on [propext, Classical.choice, Quot.sound]

#	Result	Paper Ref	Proof Method
L1	`recognitionOp_symm` — ⊙(s,s') = ⊙(s',s)	Thm III.2(1)	`rw [add_comm, mul_comm]`
L2	`recognitionOp_self` — ⊙(s,s) = 1	Thm III.2(2)	`Real.sqrt_sq` + `div_self`
L3	`completedObs_Z2_invariant` — O_ξ(s,s') = O_ξ(1−s,1−s')	Thm III.5 ★	`ring` + 3× `completedRiemannZeta_one_sub`
L4	`even_function_deriv_zero` — f even ⇒ f'(0) = 0	Prop III.7	`HasDerivAt` chain rule + `.unique` + `linarith`
L5	`riemannZeta_re_pos` — ζ(s) > 0 for real s > 1	Infrastructure	Dirichlet series + `Complex.re_tsum` + `tsum_pos`
L6–L8	Series summability + cast lemmas	Infrastructure	Standard Mathlib transfers
L9	`zetaDistribution_sum_one` — Σ P_s(n) = 1	Eq. 1 ★	`tsum_div_const` + `div_self`
L10	`sqrtEmbedding_norm_one` — ‖ψ_s‖² = 1	Eq. 8 ★	`rpow_natCast` + `rpow_mul` + `convert` from L9
L11	`recognitionOp_eq_tsum` — ⊙ = Σ ψ_s ψ_{s'}	Def. III.1	`div_mul_div_comm` + `sqrt_mul` + `rpow_add`
L12	`recognitionOp_bounded` — 0 < ⊙(s,s') ≤ 1	Thm III.2(3) ★	AM-GM + `Summable.tsum_le_tsum` + L10
L13–L15	Summability + nonnegativity helpers	Infrastructure	Comparison tests
L16	`differentiableAt_conjCompConj`	Infrastructure	CR equations through conjCLE
L17	`eq_of_eqOn_open` — identity theorem	Infrastructure	`AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq`

★★ Verified modulo A1

#	Result	Paper Ref	Proof Method
L18	`completedRiemannZeta_conj` — Λ(s̄) = Λ̄(s)	Infrastructure	A1 + identity theorem (L17) + Λ₀→Λ lift
L19	`completedObs_conj` — O_ξ(s̄,s̄') = Ō_ξ(s,s')	Infrastructure	L18 + ring hom lemmas
L20	`completedObs_norm_conj`	Infrastructure	L19 + `RCLike.norm_conj`
L21	`recognition_Z2_indistinguishable`	Prop IV.2 ★★★	Z₂ (L3) + conjugate ID + Schwarz (L20)

Dependency Graph

Mathlib riemannZeta API
  └─→ L6 (series summable)
       └─→ L7 (cast) → L8 (real summable)
            └─→ L5 (ζ(s).re > 0) ★
                 └─→ L9 (Σ P_s = 1) ★
                      └─→ L10 (‖ψ_s‖² = 1) ★
                           └─→ L12 (0 < ⊙ ≤ 1) ★★★
                 └─→ L2 (⊙(s,s) = 1) ★

  └─→ L1 (⊙ symmetric) ★

Mathlib completedRiemannZeta API
  └─→ L3 (O_ξ Z₂ invariant) ★★★
       │
       ├── A1 [AXIOM: Dirichlet series conjugation]
       │    └─→ L16 (conjCompConj holomorphic) ★
       │    └─→ L17 (identity theorem) ★
       │         └─→ L18 (Schwarz reflection) ★★
       │              └─→ L19–L20 (O_ξ conjugation/norm) ★★
       │
       └─→ L21 (Z₂ indistinguishability) ★★★

L4 (even deriv zero) ★ — standalone

Session Log

April 8–12, 2026 — v1 through v7.9

See previous entries. Summary: built from 0 to 15 verified theorems, 1 sorry.

Multi-model contributions: Perplexity (API discovery), GPT-4o (scalar-series architecture, normalization), Claude (AM-GM design, error diagnosis), Gemini (Lean 4.29.0 compat), Sonnet (tactical iteration v7.3→v7.9).

April 14, 2026 — v8.0: Zero Sorries (Sonnet)

Closed the last sorry by factoring Schwarz reflection into verified analytic machinery plus one axiom:

differentiableAt_conjCompConj — PROVEN. Hardest new lemma: CR equations for reflected function G(z) = f(z̄)̄, chain rule through three conjCLE compositions.
eq_of_eqOn_open — PROVEN. Identity theorem for entire functions agreeing on {Re s > 1}.
completedRiemannZeta_conj — PROVEN from A1. Lifts from Λ₀ (entire) to Λ via completedRiemannZeta_eq, handles pole corrections algebraically.
recognition_Z2_indistinguishable — PROVEN. The proof uses two symmetries: Z₂ sends (σ+it, ½+it') → ((1-σ)-it, ½-it'), then conjugate identification restores imaginary parts, and ‖conj z‖ = ‖z‖ gives norm equality. Neither symmetry alone suffices — you need both.

Result: 0 sorries, 3 axioms. All core Paper I theorems machine-checked.

Next Steps

Priority 1: Close axiom A1

Prove completedRiemannZeta₀_conj_on_right from Mathlib's Dirichlet series
Would make all 21 results depend only on standard axioms

Priority 2: Merge conditional chain

Port Parts 3–5 of ApoRhSpec.lean onto v8.0's Mathlib-native definitions

Priority 3: `lean4checker --fresh`

Strongest kernel-level validation