self_composition_cosh
plain-language theorem explainer
The double-angle identity equates cosh(4η) minus one to twice the square of cosh(2η) minus one plus four times cosh(2η) minus one, for real η. Researchers mapping the Riemann xi functional equation onto J-cost symmetry via defect coordinates cite it to handle cost amplification under x to x squared. The proof reduces both sides to the common expression 2c squared minus two by invoking the standard cosh double-angle and square identities, then equates them with linear arithmetic.
Claim. For all real numbers η, cosh(4η) − 1 = 2(cosh(2η) − 1)² + 4(cosh(2η) − 1).
background
The ξ(s)–J(x) Bridge identifies the completed Riemann xi functional equation ξ(s) = ξ(1−s) with J-cost reciprocal symmetry J(x) = J(1/x) under the defect-coordinate change x = exp(2(Re(s) − 1/2)). J(x) is defined as (x + x^{-1})/2 − 1, equivalently cosh(log x) − 1. The module shows that this map converts xi reflection into J-symmetry and turns zero defect into the critical line Re(s) = 1/2.
proof idea
The proof applies Real.cosh_two_mul to 2η and Real.cosh_sq to 2η. It introduces the abbreviation c for cosh(2η), rewrites the left-hand side as 2c² − 2 by the double-angle relation, expands the right-hand side to the identical polynomial via ring, and finishes with linarith.
why it matters
This identity supplies the cosh-form self-composition step required for the paired_zero_composition claim in the same module, which states J(x²) = 2J(x)² + 4J(x). It instantiates the Recognition Composition Law in logarithmic coordinates and supports the equivalence between the Riemann hypothesis and zero J-cost on the critical line. The doc-comment notes that the identity follows from the cosh double-angle formula, itself a consequence of the RCL in log-coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.