DirectCoshAdd
plain-language theorem explainer
DirectCoshAdd encodes the property that a real function Gf obeys Gf(t+u) + Gf(t-u) = 2 Gf(t) Gf(u) + 2(Gf(t) + Gf(u)) for all real t,u. Analysts reducing the composition law inside the T5 uniqueness argument cite it when passing from SatisfiesCompositionLaw to an explicit additive form on G. The declaration is a direct Prop definition with no proof content.
Claim. A function $G:ℝ→ℝ$ satisfies the direct cosh-add identity when $G(t+u)+G(t-u)=2G(t)G(u)+2(G(t)+G(u))$ for all real $t,u$.
background
The module supplies functional-equation helpers for the T5 cost uniqueness proof. DirectCoshAdd is the explicit additive identity on the G-cost, where G arises from the normalized cost F via the map G F. Sibling definitions include CoshAddIdentity on F and the equivalence CoshAddIdentity_implies_DirectCoshAdd that converts between the two forms. The local setting is preparation for showing that the Recognition Composition Law forces the canonical J-cost.
proof idea
This is a definition, not a theorem. It directly states the quantified identity as a Prop.
why it matters
The definition is invoked inside H_dAlembert_of_composition and the main uniqueness results washburn_uniqueness and T5_uniqueness_complete. It supports reduction of the composition law to the cosh-add form that establishes J-uniqueness (T5) in the forcing chain. It appears in AczelClassification and ContDiffReduction as the intermediate step toward the reciprocal cost without assuming reciprocity a priori.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.