CoshAddFromLedger
plain-language theorem explainer
Cosh-Add is the log-axis d'Alembert identity G(t+u)+G(t−u)=2G(t)G(u)+2(G(t)+G(u)), the T5 form of composition law C6. Anyone working the T5 uniqueness chain or the ledger no-go cites this predicate as the independent hypothesis that symmetry, unit, continuity, and curvature alone cannot force. Pure Prop definition: no proof content, only the quantified identity.
Claim. A real function $G$ satisfies the Cosh-Add (ledger) property when, for all real $t,u$, $$G(t+u)+G(t-u)=2\,G(t)\,G(u)+2\bigl(G(t)+G(u)\bigr).$$
background
This module sits in the T5 verification layer. From ledger structure (T3) it derives reciprocal symmetry $F(x)=F(1/x)$ and unit normalization $F(1)=0$, then proves that the remaining T5 ingredient, the composition law, cannot be obtained from those ledger facts plus regularity.
On the log axis one reparametrizes by $G(t)=F(e^t)$ (the G of Cost.FunctionalEquation). Multiplicative Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ becomes, under that change of variable, the additive d'Alembert / Cosh-Add identity packaged here. In the honest forcing diagram, C6 is an independent load-bearing hypothesis; C7 is only a calibration choice $\lambda=1$. Together with C1–C5 they feed the Aczél-type classification that pins $J(x)=\frac12(x+1/x)-1$.
proof idea
Definitional Prop only. The body is the single universal quantification of the additive identity; there are no tactics, no lemmas, and no reduction steps. Downstream lemmas apply the predicate by specializing $t,u$ or by unfolding it under a concrete witness $G$.
why it matters
Names the exact identity that the T5 characterization treats as composition law C6 on the log axis. Downstream, aczel_theorem_3_1_3_hypothesis asserts (falsely) that evenness, $G(0)=0$, continuity, and unit log-curvature force this identity; quadraticWitness_not_coshAdd shows the quadratic $G(t)=t^2/2$ violates it at $(t,u)=(1,1)$. That pair is the kernel-checked no-go (2026 audit, Finding 2): C6 is not derivable from ledger symmetry and unit alone, correcting an earlier mis-citation of Aczél (1966, Thm. 3.1.3), which classifies solutions of d'Alembert rather than deriving the equation from regularity. In the primer chain this is the independent gate before T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.