cosh_eq_one_iff
plain-language theorem explainer
The equivalence cosh t = 1 if and only if t = 0 supplies the uniqueness of the zero for the hyperbolic cosine on the reals. Workers on reduced phase potentials in scale-invariant energies cite it to conclude that J̃ vanishes exactly at integer mismatches. The proof splits the biconditional, derives a contradiction from the strict inequality cosh t > 1 for t ≠ 0, and substitutes directly at zero.
Claim. $cosh t = 1$ if and only if $t = 0$, for real $t$.
background
The module ReducedPhasePotential formalizes the reduced phase-mismatch potential J̃_b(δ) = cosh(lam · d_ℤ(δ)) − 1, where d_ℤ(δ) is the distance to the nearest integer and lam = ln b. This lemma supplies the elementary fact that the cosine term equals one precisely at zero, which is required to characterize the zeros of J̃. The local setting follows the Thapa–Washburn 2026 treatment of rigidity in scale-invariant ratio-based energies (Section IV). Upstream results include the parallel statement in ZeroCompositionInterface together with structural properties of the forcing self-reference and simplicial ledger.
proof idea
The term-mode proof opens with constructor to split the biconditional. The forward direction assumes cosh t = 1, negates t = 0, and applies one_lt_cosh to obtain the contradictory strict inequality. The reverse direction rewrites the assumption t = 0 into cosh 0 = 1.
why it matters
The lemma is invoked inside Jtilde_zero_iff to conclude that J̃(lam, δ) = 0 precisely when δ is integer (for lam ≠ 0), and it is reused in zeroCompositionLaw_forces_unique_minimum to establish the unique minimum of the composition law. It therefore closes the zero-characterization step required by the GCIC paper's phase-potential analysis and aligns with the J-uniqueness property in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.