phi
plain-language theorem explainer
The auxiliary φ converts a d'Alembert solution H with H(t) ≥ 1 into the positive function satisfying the multiplicative Cauchy equation. Cost theorists in Recognition Science cite it when reducing the Recognition Composition Law to the standard d'Alembert form and classifying its continuous solutions. The definition is the direct algebraic expression H(t) plus the positive square root of H(t) squared minus one.
Claim. $φ(t) := H(t) + √(H(t)^2 - 1)$ where $H : ℝ → ℝ$ satisfies the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$ and $H(t) ≥ 1$.
background
The module formalizes the cosh branch of the Aczél classification for continuous d'Alembert solutions arising from the Recognition Composition Law. Given a continuous H with H(0) = 1 that attains values > 1, the auxiliary φ is introduced so that φ(t+u) = φ(t) φ(u) holds, forcing φ(t) = e^{λt} and therefore H(t) = cosh(λt). Upstream, H is the shifted cost H(x) = J(x) + 1, where J satisfies the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y); the shift converts this exactly into the d'Alembert equation quoted above. The module states that this branch is the one relevant to Recognition Science because J-cost grows unboundedly.
proof idea
One-line definition that directly encodes the positive branch of the d'Alembert solution as H(t) plus the square root of H(t) squared minus one.
why it matters
This definition supplies the starting point for proving that φ is multiplicative, which then forces the exponential form and the cosh solution for H. It fills the Branch 1 step in the Aczél classification strategy of the module, connecting the Recognition Composition Law to hyperbolic solutions used in the phi-ladder and mass formulas. The parent results are the subsequent theorems phi_pos, phi_at_zero, phi_multiplicative and H_CauchyToExponential that rely on this auxiliary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.