costLambda_coshAddIdentity
plain-language theorem explainer
Every member of the one-parameter cost gauge family F_c(x) = (x^c + x^{-c})/2 - 1 satisfies the cosh-add (d'Alembert) identity that encodes the Recognition Composition Law in log coordinates. Anyone proving that the full gauge orbit obeys RCL cites this. The proof rewrites G(F_c) as cosh(c·t)-1 and applies the classical cosh addition formulas.
Claim. For every real calibration parameter $c$, the cost $F_c(x) = \frac{1}{2}(x^c + x^{-c}) - 1$ satisfies the cosh-add identity: if $G_F(t) := F(e^t)$, then $G_F(t+u) + G_F(t-u) = 2\,G_F(t)\,G_F(u) + 2\,(G_F(t) + G_F(u))$ for all real $t,u$.
background
In the Primitive Recognition Calculus, the admissible costs form a one-parameter gauge family $F_c(x) = \frac12(x^c + x^{-c}) - 1$ on the positive reals (real powers via rpow). The member $c=1$ is the canonical $J$-cost $J(x) = \frac12(x+x^{-1})-1$ forced by T5. In additive (log) coordinates one works with $G_F(t) := F(e^t)$; for this family that is exactly $\cosh(c,t)-1$.
The Recognition Composition Law (RCL) is the multiplicative identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. In log coordinates it becomes the cosh-add / d'Alembert identity on $G_F$: $G_F(t+u)+G_F(t-u)=2G_F(t)G_F(u)+2(G_F(t)+G_F(u))$. The module isolates calibration independence: every gauge member already obeys the structural cost laws; only the second-derivative normalization $G''(0)=1$ pins $c=1$.
Upstream, G_costLambda supplies the identification $G(F_c)(t)=\cosh(c,t)-1$, and CoshAddIdentity is the Prop packaging the d'Alembert form used by the functional-equation layer.
proof idea
Tactic proof. Fix real $t,u$. Unfold the goal via G_costLambda, so both sides are written in terms of $\cosh(c\cdot,)$. Two short ring lemmas distribute the scalar: $c(t+u)=ct+cu$ and $c(t-u)=ct-cu$. Rewrite with Real.cosh_add and Real.cosh_sub, then finish by ring. Both sides collapse to $2\cosh(ct)\cosh(cu)-2$, which is the classical cosh product identity in d'Alembert form.
why it matters
This is the structural half of calibration independence: every gauge orbit member already satisfies RCL, so the composition law does not force the unit. The immediate parent is costLambda_satisfiesCompositionLaw, which converts this identity through composition_law_equiv_coshAdd into the multiplicative SatisfiesCompositionLaw predicate. Downstream that feeds the headline that only the calibration condition $G''(0)=1$ (equivalently $c^2=1$) selects $J$ among the family, tying back to T5 J-uniqueness and the RCL landmark in the forcing chain. Without this lemma the gauge-orbit argument would be incomplete: one would know the cosh form but not that every $c$ still obeys the composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.