CoshAddIdentity_implies_DirectCoshAdd
plain-language theorem explainer
The lemma establishes equivalence between the cosh-add identity on a cost function F and the direct cosh-add identity on its log-reparametrized version G F. Researchers deriving T5 uniqueness for the J-cost in Recognition Science cite it when moving between original and reparametrized forms of the functional equation. The proof is a one-line wrapper that applies the hypothesis directly.
Claim. If $F : ℝ → ℝ$ satisfies $∀ t,u ∈ ℝ, G_F(t+u) + G_F(t-u) = 2 G_F(t) G_F(u) + 2 G_F(t) + 2 G_F(u)$, then the reparametrized function $G_F$ satisfies $∀ t,u ∈ ℝ, G_F(t+u) + G_F(t-u) = 2 G_F(t) G_F(u) + 2 G_F(t) + 2 G_F(u)$, where $G_F(t) := F(e^t)$.
background
The Cost.FunctionalEquation module supplies helper lemmas for the T5 cost uniqueness proof. G is the log-coordinate reparametrization defined by $G_F(t) := F(e^t)$. CoshAddIdentity F asserts the cosh-type addition formula holds for this $G_F$, while DirectCoshAdd asserts the identical formula when applied directly to its argument function.
proof idea
The proof is a one-line wrapper that directly invokes the hypothesis h, since CoshAddIdentity F is defined to be exactly the statement DirectCoshAdd (G F).
why it matters
It is invoked in downstream results including H_dAlembert_of_composition and washburn_uniqueness to convert between composition-law statements and the direct cosh-add form on G F. The lemma supports the T5 J-uniqueness step in the Recognition Science forcing chain by enabling the Recognition Composition Law to be applied after reparametrization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.