IndisputableMonolith.Cost.CauchyAuxiliary
Auxiliary module for the d'Alembert functional equation on the cost side. It defines φ(t) = H(t) + √(H(t)² - 1) for solutions with H ≥ 1, and records the elementary identities that turn multiplicative Cauchy data for φ into the exponential form of H. Anyone citing the conditional Aczél classification or the passage from H-Cauchy to cosh will pull these lemmas.
claimFor a d'Alembert solution $H$ with $H(t)\ge 1$, the auxiliary $\varphi(t)=H(t)+\sqrt{H(t)^2-1}$ satisfies $\varphi>0$, $\varphi(0)=1$, and converts the additive Cauchy equation on $\log\varphi$ into the multiplicative form that yields $H(t)=\cosh(\lambda t)$ (or the constant solution $H\equiv 1$).
background
The parent module AczélTheorem treats continuous solutions of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$. Its classification states that every such continuous $H$ is $C^\infty$ and equals either the constant $1$ or $\cosh(\lambda t)$ for some $\lambda$.
When $H\ge 1$, the algebraic inverse of the cosh parametrization is the map $\varphi(t)=H(t)+\sqrt{H(t)^2-1}$. This $\varphi$ is strictly positive, satisfies $\varphi(0)=1$, and turns the original two-variable identity into a multiplicative Cauchy equation for $\varphi$ (equivalently an additive Cauchy equation for $\log\varphi$). The present module isolates that change of unknown and the elementary positivity and reconstruction lemmas needed downstream.
In the Recognition cost hierarchy these identities sit under the J-cost / RCL layer: the same hyperbolic solutions appear as the unique smooth generators compatible with the Recognition Composition Law.
proof idea
Definition-and-lemma module, not a single theorem. It introduces $\varphi$ from $H$, proves $\varphi(0)=1$ and $\varphi>0$ by direct algebra under $H\ge 1$, reconstructs $H=(\varphi+\varphi^{-1})/2$, and records that multiplicative Cauchy data for $\varphi$ imply the exponential (hence cosh) form of $H$. The conditional Aczél classification wrapper simply packages these facts with the smoothness result imported from AczelTheorem.
why it matters in Recognition Science
Supplies the change-of-unknown bridge between raw d'Alembert solutions and the exponential/cosh normal form used throughout the cost stack. Downstream consumers (conditional Aczél classification, any theorem that quotes $H=\cosh(\lambda t)$ from Cauchy data) depend on $\varphi$ being well-defined, positive, and invertible back to $H$. In the broader Recognition forcing chain this is the analytic step that lets the unique smooth cost generator be identified with a hyperbolic cosine, which later feeds J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6).
scope and limits
- Does not prove continuity or smoothness of H; that is imported from AczelTheorem.
- Does not treat the regime H < 1 (trigonometric solutions).
- Does not fix the constant λ; only the functional form.
- Does not derive the Recognition Composition Law or J-uniqueness itself.