phi_pos
plain-language theorem explainer
The auxiliary phi(t) equals H(t) plus the positive square root of H(t) squared minus one, hence is strictly positive whenever H(t) is at least one. Researchers classifying continuous d'Alembert solutions cite it to justify the positivity hypothesis needed before proving multiplicativity in the cosh branch. The proof is a short tactic sequence that unfolds the definition, applies nlinarith to the squared term, invokes sqrt nonnegativity, and closes with linarith.
Claim. If $H(t)geq 1$ then $phi(t)>0$, where $phi(t):=H(t)+sqrt{H(t)^2-1}$.
background
The module supplies auxiliary functions for the Aczel classification of continuous d'Alembert solutions H satisfying H(xy)+H(x/y)=2H(x)H(y) with H(0)=1. In Branch 1 (the cosh case relevant to RS), when H exceeds 1 at some point one defines phi(t)=H(t)+sqrt(H(t)^2-1). The upstream H is the shifted cost H(x)=J(x)+1=1/2(x+x^{-1}), which satisfies the d'Alembert equation by the Recognition Composition Law. The module doc states that this branch yields H(t)=cosh(lambda t) once phi is shown multiplicative and continuous.
proof idea
Unfolds the definition of phi. From the hypothesis 1 leq H t the tactic nlinarith produces 0 leq H t^2-1. Real.sqrt_nonneg then gives 0 leq sqrt(H t^2-1). Linear arithmetic on the sum H t + sqrt(...) finishes the strict inequality.
why it matters
Secures positivity of the auxiliary function in the cosh branch of the Aczel strategy, the branch required for Recognition Science because J-cost is unbounded. It precedes phi_multiplicative and H_CauchyMultiplicative, which together force the exponential form H(t)=cosh(lambda t). This step aligns with the framework's T5 J-uniqueness and the self-similar fixed point phi, closing one link in the chain from the functional equation to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.