phi_at_zero
φ(0) equals 1 whenever a d'Alembert solution H satisfies H(0)=1. Researchers classifying continuous solutions to the functional equation inside the Recognition Science cost framework cite this normalization step. The argument is a direct term-mode simplification that unfolds the definition of the auxiliary φ and substitutes the given value at zero.
claimIf $H:ℝ→ℝ$ satisfies $H(0)=1$, then the auxiliary function satisfies $φ(H,0)=1$, where $φ(t)=H(t)+√(H(t)^2-1)$.
background
The module develops auxiliary functions for the cosh branch of the Aczél classification of continuous d'Alembert solutions H with H(0)=1. When H attains values above 1, one defines the auxiliary φ(t)=H(t)+√(H(t)^2-1) to convert the d'Alembert identity into the multiplicative Cauchy equation φ(t+u)=φ(t)·φ(u). In Recognition Science this branch is the relevant one because the shifted cost H=J+1 is unbounded above. Upstream, the CostAlgebra definition states that H(x)=J(x)+1=½(x+x^{-1}), so that the Recognition Composition Law becomes the standard d'Alembert equation H(xy)+H(x/y)=2·H(x)·H(y). The FunctionalEquation module supplies the reparametrization H_F t=G_F t+1.
proof idea
The proof is a one-line term-mode wrapper that applies simp to the definition of phi together with the hypothesis h_one.
why it matters in Recognition Science
The lemma is used inside aczel_classification_conditional to complete the conditional Aczél classification under the H_PhiMultiplicative bridge. It supplies the required base value for the multiplicative property in the cosh branch, which is the one needed for Recognition Science because J-cost grows without bound and H exceeds 1. The result therefore sits between the Recognition Composition Law and the exponential solutions that recover the phi-ladder.
scope and limits
- Does not prove the multiplicative property of φ.
- Does not assume or use continuity of H.
- Does not apply to the trigonometric branch where H remains ≤1.
- Does not derive the explicit form φ(t)=exp(λt).
formal statement (Lean)
54theorem phi_at_zero (H : ℝ → ℝ) (h_one : H 0 = 1) : phi H 0 = 1 := by
proof body
Term-mode proof.
55 simp [phi, h_one]
56
57/-- φ(t) > 0 when H(t) ≥ 1. -/