DirectCoshAdd
DirectCoshAdd encodes the additive form of the Recognition Composition Law for an auxiliary real function Gf. Researchers proving T5 uniqueness in Recognition Science cite this definition when converting the multiplicative RCL into its d'Alembert-style additive version. The definition is a direct encoding of the equation without lemmas or reductions.
claimLet $G_f : ℝ → ℝ$. The predicate DirectCoshAdd($G_f$) holds precisely when $G_f(t+u) + G_f(t-u) = 2 G_f(t) G_f(u) + 2 G_f(t) + 2 G_f(u)$ for all real $t,u$.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument. Gf denotes the transformed cost obtained from a normalized F via the map G, which converts the multiplicative composition law into an additive equation on the real line.
proof idea
This is a definition. It directly states the quantified equation with no lemmas, tactics, or reductions applied.
why it matters in Recognition Science
DirectCoshAdd supplies the target predicate for lemmas that derive the d'Alembert form from the composition law, feeding washburn_uniqueness and washburn_uniqueness_aczel. These theorems establish that any reciprocal normalized cost obeying the RCL and calibration must coincide with the J-cost J(x) = (x + x^{-1})/2 - 1, closing the T5 step of the forcing chain.
scope and limits
- Does not assume continuity, differentiability, or any regularity on Gf.
- Does not derive the identity from the multiplicative RCL; it is the target statement.
- Does not reference the phi-ladder, Berry threshold, or spatial dimension D=3.
- Does not impose normalization or calibration conditions on Gf.
formal statement (Lean)
34def DirectCoshAdd (Gf : ℝ → ℝ) : Prop :=
proof body
Definition body.
35 ∀ t u : ℝ,
36 Gf (t+u) + Gf (t-u) = 2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)
37