BalancedArithmeticLedger
plain-language theorem explainer
BalancedArithmeticLedger defines the property that a map F from complex numbers to complex numbers remains unchanged under s to 1 minus s, with all fixed points confined to the line of real part one half. Researchers linking the completed Riemann zeta to Recognition Science arithmetic ledgers cite this structure to encode the reciprocal balance law. The declaration is a direct two-field structure with no proof body.
Claim. A function $F : ℂ → ℂ$ is a balanced arithmetic ledger when $F(1-s) = F(s)$ for all $s ∈ ℂ$ and the fixed-point condition $s = 1-s$ forces $Re(s) = 1/2$.
background
The CompletedZetaLedger module packages Mathlib's completed-zeta functional equation as the reciprocal balance law for the arithmetic ledger. BalancedArithmeticLedger encodes invariance under the coordinate change s ↦ 1-s together with the requirement that the fixed locus lies on the critical line. Upstream structures such as LedgerFactorization.of supply the underlying (ℝ₊, ×) factorization and J-calibration, while PhiForcingDerived.of supplies the strict convexity of J(x) = (x + x⁻¹)/2 - 1 whose unique minimum at x=1 motivates the ledger balance.
proof idea
Direct structure definition containing exactly two fields. The first field states the symmetry F(1-s)=F(s); the second states that any fixed point of the involution satisfies Re(s)=1/2. No lemmas or tactics are applied.
why it matters
The definition supplies the target property proved by the downstream theorem completedZeta_balanced and appears inside the certificate CompletedZetaLedgerCert. It realizes the reciprocal balance law that connects the zeta functional equation to the T5 J-uniqueness step of the forcing chain and to the phi-ladder arithmetic structures. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.