cosh_eq_one_iff
plain-language theorem explainer
The declaration establishes that cosh t equals 1 precisely when t vanishes. Workers on zero-composition interfaces in the Recognition Science alternate path cite it to obtain uniqueness of the minimum for the composed cost function H. The proof splits the biconditional and invokes the strict inequality one_lt_cosh for the nontrivial direction.
Claim. For every real number $t$, one has $cosh(t) = 1$ if and only if $t = 0$.
background
The Zero Composition Interface module supplies the abstract theorem interface that Vector C would require to convert a zero-location observable into a critical-line forcing statement. It is classified as ALTERNATE and does not lie on the primary unconditional RH route. The module assumes the Recognition Science J-cost (defined by $J(x) = (x + x^{-1})/2 - 1$, equivalently $cosh(log x) - 1$) together with the Recognition Composition Law, and isolates the minimal algebraic facts needed to force a unique minimum at the origin.
proof idea
The term-mode proof applies constructor to split the biconditional. The forward direction assumes cosh t = 1 yet t ≠ 0, obtains the contradiction 1 < cosh t via one_lt_cosh, and closes with linarith. The reverse direction substitutes the hypothesis and simplifies.
why it matters
It is invoked directly by zeroCompositionLaw_forces_unique_minimum to conclude that the minimum value 1 of the composed cost occurs exactly at t = 0. The module doc states that any successful Vector C path must import extra Euler/Hadamard analytic data beyond pure FE symmetry and RCL doubling; this lemma supplies the elementary cosh identity that closes the uniqueness step inside that interface. It touches the open question whether completed-ξ data can instantiate the full ZeroCompositionWitness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.