composition_law_equiv_coshAdd
plain-language theorem explainer
Equivalence between the multiplicative Recognition Composition Law on a cost function F and the additive cosh-add identity on its log-reparametrized G is established here. T5 uniqueness arguments in Recognition Science cite this to switch between multiplicative and additive forms of the functional equation. The tactic proof splits into two directions, each using exponential substitution together with exp_add, exp_sub, and algebraic simplification.
Claim. For a function $F : ℝ → ℝ$, the following are equivalent: $F$ satisfies the composition law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for all $x,y > 0$, and the reparametrized function $G(t) := F(e^t)$ satisfies $G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u)$ for all real $t,u$.
background
This declaration belongs to the Cost.FunctionalEquation module, which supplies lemmas for the T5 cost uniqueness proof. The Recognition Composition Law is the predicate SatisfiesCompositionLaw F, requiring $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for all positive $x,y$. The auxiliary map G reparametrizes via the exponential: $G(t) = F(e^t)$. CoshAddIdentity is the corresponding additive equation on G: $G(t+u) + G(t-u) = 2G(t)G(u) + 2G(t) + 2G(u)$ for all real $t,u$.
proof idea
The proof applies the constructor tactic. Forward direction assumes the composition law, substitutes $x = e^t$ and $y = e^u$, rewrites using exp_add and exp_sub, then closes with linarith. Reverse direction assumes the cosh-add identity, substitutes $t = log x$ and $u = log y$, rewrites with exp_log, applies the identity, and finishes with ring after exp_add and exp_sub rewrites.
why it matters
This equivalence is invoked by downstream theorems including washburn_uniqueness, washburn_uniqueness_of_contDiff, and H_dAlembert_of_composition to convert the Recognition Composition Law into d'Alembert form. It fills the T5 step of the forcing chain by enabling the transition from multiplicative RCL to the additive identity that forces J-uniqueness. The module positions the result as a helper for deriving the canonical reciprocal cost under normalization and calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.