reciprocal_fixed_re_eq_half
plain-language theorem explainer
The fixed point equation s = 1 - s for complex s forces the real part to be exactly one half. Researchers verifying the symmetry of the completed Riemann zeta function under the functional equation would invoke this result when establishing balance properties of the associated arithmetic ledger. The proof proceeds by applying congruence to the real-part projection of the given equality, followed by simplification of complex arithmetic and a linear-arithmetic closure.
Claim. If $s ∈ ℂ$ satisfies $s = 1 - s$, then Re$(s) = 1/2$.
background
The module CompletedZetaLedger packages Mathlib's completed-zeta functional equation as the reciprocal balance law for the arithmetic ledger. The reciprocal operation on events inverts the ratio while swapping source and target, and a ledger is balanced when its event list satisfies the corresponding symmetry. This theorem supplies the fixed-locus property needed to certify that the critical line is the unique line of symmetry for the completed zeta function.
proof idea
The proof extracts the real part via congruence on the hypothesis s = 1 - s, simplifies the resulting equation using the real-part rules for subtraction and the constant one, and closes with linear arithmetic.
why it matters
This result is invoked inside the definition of completedZetaLedgerCert to discharge the critical_line_unique field, which in turn supports the balanced property of the completed zeta ledger. It directly encodes the geometric content of the functional equation's symmetry axis at Re(s) = 1/2, aligning with the Recognition Science emphasis on reciprocal balance. No open scaffolding remains here; the statement is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.