completedZeta_balanced
plain-language theorem explainer
The completed Riemann zeta function satisfies invariance under s to 1 minus s together with the property that fixed points of this map have real part exactly 1/2. Researchers embedding the classical functional equation into the Recognition Science arithmetic ledger would cite the result. The proof rewrites the symmetry axiom with the completed-zeta identity and applies the algebraic fixed-locus lemma to the second axiom.
Claim. The completed Riemann zeta function satisfies $F(1-s)=F(s)$ for all complex $s$, and $s=1-s$ implies $s.re=1/2$.
background
The module packages Mathlib's completed zeta as the reciprocal balance law for an arithmetic ledger. BalancedArithmeticLedger on a map $F:ℂ→ℂ$ requires reciprocal symmetry $F(1-s)=F(s)$ for all $s$ and that the fixed locus of the involution $s↦1-s$ lies on the critical line. The upstream theorem reciprocal_fixed_re_eq_half states that the fixed locus of $s↦1-s$ has real part $1/2$, proved by applying congrArg to the real-part projection and simplifying.
proof idea
The tactic proof splits on the two fields of BalancedArithmeticLedger. Reciprocal symmetry is discharged by introducing $s$ and rewriting with the Mathlib lemma completedRiemannZeta_one_sub. The balance-line-fixed field is discharged by introducing $s$ and hypothesis $hs:s=1-s$, then applying the lemma reciprocal_fixed_re_eq_half directly.
why it matters
The theorem supplies the balanced property required by the downstream CompletedZetaLedgerCert, which records that the completed zeta furnishes a balanced arithmetic ledger together with uniqueness of the critical line. It thereby embeds the classical functional equation of the Riemann zeta into the Recognition Science framework as an instance of the reciprocal balance law. No open questions are directly closed or opened.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.