pith. machine review for the scientific record. sign in
def definition def or abbrev high

phi

show as:
view Lean formalization →

The auxiliary phi extracts the exponential generator from a d'Alembert solution H via the explicit formula phi(t) = H(t) + sqrt(H(t)^2 - 1). Researchers classifying continuous solutions to the shifted cost equation in Recognition Science cite this to reach the cosh representation of H. The definition is a direct algebraic expression selecting the positive branch of the inverse hyperbolic cosine.

claim$phi(t) := H(t) + sqrt(H(t)^2 - 1)$ where $H : R to R$ satisfies the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$ with $H(t) geq 1$ for all $t$.

background

In Recognition Science the J-cost satisfies the Recognition Composition Law, which under the shift H(x) = J(x) + 1 becomes the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Upstream results from CostAlgebra establish that H(0) = 1 and that H(x) = 1/2 (x + x^{-1}) for the base case. The module CauchyAuxiliary isolates the branch in which H attains values strictly greater than 1, the regime relevant to unbounded J-cost growth.

proof idea

The definition is a one-line algebraic expression that adds the positive square root to H(t), selecting the branch greater than or equal to 1 that corresponds to the inverse of the hyperbolic cosine map.

why it matters in Recognition Science

This definition initiates the cosh branch of the Aczel classification for d'Alembert solutions, the branch required by Recognition Science because J-cost grows without bound. It supplies the starting point for sibling results such as phi_at_zero and phi_multiplicative that recover the exponential form H(t) = cosh(lambda t). The construction aligns with T5 J-uniqueness and the forcing of phi as the self-similar fixed point.

scope and limits

formal statement (Lean)

  50def phi (H : ℝ → ℝ) (t : ℝ) : ℝ :=

proof body

Definition body.

  51  H t + Real.sqrt (H t ^ 2 - 1)
  52
  53/-- φ(0) = 1 when H(0) = 1. -/

depends on (2)

Lean names referenced from this declaration's body.