H_from_phi
plain-language theorem explainer
H(t) recovers from the auxiliary φ via the average of φ and its reciprocal whenever H(t) ≥ 1. Workers on functional equations for Recognition Science cost models cite this to invert the cosh representation. The argument is a short algebraic verification that exploits the conjugate relation built into the definition of φ.
Claim. For a real-valued function $H$ and real $t$ with $1 ≤ H(t)$, if $φ$ denotes the auxiliary map $φ(s) = H(s) + √(H(s)^2 - 1)$, then $H(t) = (φ(t) + φ(t)^{-1})/2$.
background
The module develops auxiliary constructions for the cosh branch of Aczél's classification of continuous d'Alembert solutions. When H satisfies H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 and attains values above 1, one defines φ(t) = H(t) + √(H(t)^2 - 1); this φ is positive and converts the problem into the multiplicative Cauchy equation. The module states that this branch is the one relevant to RS because J-cost grows unboundedly and H = 1 + J achieves values > 1. The present result inverts the construction. It rests on the shifted cost H = J + 1 from CostAlgebra, which satisfies the d'Alembert equation by the Recognition Composition Law.
proof idea
Unfold the definition of phi. Set s to the square root of H(t)^2 - 1 and record that s^2 equals the difference together with nonnegativity of s. Show that (H(t) + s) times (H(t) - s) equals 1, hence the reciprocal of H(t) + s is H(t) - s. Rewrite and apply the ring tactic to reach the average.
why it matters
The lemma feeds directly into aczel_classification_conditional, which completes the Aczél classification once the multiplicative property is assumed. It supplies the missing algebraic identity that lets the exponential solution for φ translate back into the hyperbolic form for H. In the Recognition Science chain this supports the identification of J with cosh(log x) - 1 at the level of T5 uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.