Explanation of DirectCoshAdd in IndisputableMonolith.Cost.FunctionalEquation

(1) In plain English: DirectCoshAdd is a predicate on a function Gf : ℝ → ℝ. It asserts that Gf obeys the identity Gf(t + u) + Gf(t - u) = 2·(Gf(t)·Gf(u)) + 2·(Gf(t) + Gf(u)) for every pair of real numbers t and u. This is the direct form of an addition formula that matches the algebraic expansion of cosh(t + u) + cosh(t - u) after a logarithmic reparametrization.

(2) Why it matters in Recognition Science: The predicate supplies one of the functional-equation building blocks used to characterize the recognition cost Jcost. The module shows that Jcost satisfies the related CoshAddIdentity Jcost_cosh_add_identity, which immediately yields DirectCoshAdd (G Cost.Jcost) via the implication lemma. This identity is part of the infrastructure that isolates the unique reciprocal-symmetric cost function required by the T5 step of the forcing chain.

(3) How to read the formal statement: The declaration

def DirectCoshAdd (Gf : ℝ → ℝ) : Prop :=
  ∀ t u : ℝ,
    Gf (t+u) + Gf (t-u) = 2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)

introduces a named proposition (Prop) that takes a function Gf and universally quantifies the displayed equality over all real t and u. In Lean syntax the colon : separates the binder from the body; ∀ is universal quantification; Prop is the type of propositions.

(4) Visible dependencies or certificates in the supplied source: The definition appears directly in module IndisputableMonolith.Cost.FunctionalEquation. It is connected to the companion predicate by the lemma CoshAddIdentity_implies_DirectCoshAdd. The concrete cost function satisfies the antecedent via Jcost_cosh_add_identity and the auxiliary identity Jcost_G_eq_cosh_sub_one. All cited declarations are free of sorry and external axioms in the supplied slice.

(5) What this declaration does not prove: DirectCoshAdd is only a definition; it does not assert that any specific function (including Jcost) satisfies the property—that is supplied by the separate theorem Jcost_cosh_add_identity. It does not contain the smoothness or ODE-uniqueness arguments that complete the uniqueness proof for Jcost, nor does it derive physical constants or the full T5 forcing statement.