CoshAddIdentity
CoshAddIdentity names the cosh-addition functional equation satisfied by the reparametrized cost G_F in log coordinates. T5 uniqueness proofs in Recognition Science cite it when converting the multiplicative composition law into an additive identity. The definition directly encodes the stated relation for all real t and u without further derivation.
claimLet $G_F(t) := F(e^t)$ for a function $F : ℝ → ℝ$. Then CoshAddIdentity($F$) asserts that for all real $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)$.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument. The reparametrization $G_F(t) := F(e^t)$ converts the original multiplicative arguments of the cost into additive ones. Upstream results include the definition of G in Constants and the identity event at the J-cost minimum. The composition law on F is shown equivalent to this identity via the substitution $x = e^s$, $y = e^t$.
proof idea
As a definition the body simply states the universal quantification over t and u. It functions as the target property in the equivalence theorem composition_law_equiv_coshAdd, which establishes both directions by direct substitution of the exponential and algebraic rearrangement.
why it matters in Recognition Science
The definition bridges the Recognition Composition Law to the hyperbolic form required for T5 J-uniqueness. It is invoked by washburn_uniqueness_of_contDiff, composition_law_forces_reciprocity, and the explicit verification that Jcost satisfies the identity. In the forcing chain it supports passage from the composition law to the self-similar fixed point phi and the eight-tick octave.
scope and limits
- Does not impose continuity or differentiability on F.
- Does not encode normalization or calibration conditions.
- Does not derive the identity from the J-cost formula; it only names the property.
- Does not extend to complex arguments or other base fields.
formal statement (Lean)
29def CoshAddIdentity (F : ℝ → ℝ) : Prop :=
proof body
Definition body.
30 ∀ t u : ℝ,
31 G F (t+u) + G F (t-u) = 2 * (G F t * G F u) + 2 * (G F t + G F u)
32
33/-- Direct cosh-add identity on a function. -/
used by (15)
-
composition_law_forces_reciprocity -
washburn_uniqueness_of_contDiff -
composition_law_equiv_coshAdd -
CoshAddIdentity_implies_DirectCoshAdd -
Jcost_cosh_add_identity -
normalized_implies_G_zero -
washburn_uniqueness -
washburn_uniqueness_aczel -
washburn_uniqueness_aczel -
T5_uniqueness_complete -
UniqueCostAxioms -
extraction_cost_strict_minimum -
Composition_implies_CoshAddIdentity -
nothing_costs_infinity -
uniqueness_specification