Composition_implies_CoshAddIdentity
plain-language theorem explainer
Any cost function F obeying the multiplicative composition axiom satisfies the additive cosh identity after logarithmic reparametrization via G(t) = F(exp t). Uniqueness arguments for the J-cost function cite this step when converting the d'Alembert form into the cosh-add form needed for T5. The proof substitutes exponential arguments into the composition law, invokes the dAlembert instance, and applies algebraic regrouping.
Claim. If $F : ℝ → ℝ$ satisfies $F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$ for all $x, y > 0$, then the reparametrized function $G(t) := F(e^t)$ satisfies $G(t+u) + G(t-u) = 2 G(t) G(u) + 2 G(t) + 2 G(u)$ for all real $t, u$.
background
The module CostAxioms encodes the three primitive axioms of Recognition Science. Composition is axiom A2, the Recognition Composition Law, which states that for positive x and y the cost satisfies the multiplicative d'Alembert relation F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y). The auxiliary function G is the log-coordinate reparametrization G(t) = F(exp t) supplied by Cost.FunctionalEquation.G.
proof idea
The tactic proof introduces t and u, records positivity of the exponentials, rewrites exp(t+u) and exp(t-u) via exp_add and exp_neg, then applies the dAlembert instance from the Composition class. A convert tactic followed by ring normalizes the resulting expression to the target cosh-add identity.
why it matters
This implication supplies the cosh-add identity required by the T5 uniqueness specification theorem uniqueness_specification. It directly links the Recognition Composition Law to the functional equation whose solutions are shown to be J in the forcing chain. The step is used in the derivation of J-uniqueness from the primitive axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.