CoshAddIdentity
plain-language theorem explainer
CoshAddIdentity defines the additive functional equation satisfied by the reparametrized cost G_F(t) = F(exp t). Researchers proving T5 uniqueness of the J-cost under the Recognition Composition Law cite this when converting between multiplicative and additive forms. The definition is a direct statement of the identity with no lemmas or tactics applied.
Claim. Let $G_F(t) := F(e^t)$. The predicate CoshAddIdentity$(F)$ holds when $G_F(t+u) + G_F(t-u) = 2 G_F(t) G_F(u) + 2 G_F(t) + 2 G_F(u)$ for all real $t,u$.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument. G is the log reparametrization $G(F,t) := F(e^t)$ that converts the multiplicative composition law on $F$ into an additive identity on $G$. Upstream results include the explicit J-cost form $G(t) = cosh(t)-1$ and the identity event at the J-cost minimum.
proof idea
This is a definition that states the cosh-add identity directly on the reparametrized function $G_F$. No lemmas are invoked; the body is the Prop itself.
why it matters
CoshAddIdentity is the target of composition_law_equiv_coshAdd, which equates the composition law on $F$ to this identity on $G$. It is invoked by washburn_uniqueness and washburn_uniqueness_of_contDiff, which close the T5 step of the forcing chain by showing that normalization plus the composition law already force the canonical reciprocal cost $J(x) = (x + x^{-1})/2 - 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.