H_PhiMultiplicative
plain-language theorem explainer
H_PhiMultiplicative encodes the statement that the auxiliary phi built from H obeys phi(t+u) = phi(t) * phi(u) for all t,u where H(t) >=1 and H(u)>=1. Analysts classifying continuous d'Alembert solutions in Recognition Science cite it to reach the exponential representation in the unbounded branch. The declaration is a direct definition of this multiplicative relation.
Claim. If $H : ℝ → ℝ$ and $ϕ(t) := H(t) + √(H(t)^2 - 1)$, then ∀ t,u ∈ ℝ, (H(t) ≥ 1 ∧ H(u) ≥ 1) → ϕ(t+u) = ϕ(t) · ϕ(u).
background
The module develops auxiliary functions to classify continuous solutions of d'Alembert's equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1. This equation arises from the Recognition Composition Law applied to the shifted cost H(x) = J(x) + 1, where J is the cost function satisfying J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y). MODULE_DOC states: 'We formalize Branch 1: the cosh case, which is the one relevant to RS (since J-cost grows unboundedly and H = 1 + J achieves values > 1).'
proof idea
The declaration is a definition that directly states the multiplicative Cauchy equation for the auxiliary phi. The accompanying comment sketches the algebraic steps from the d'Alembert identity by isolating square-root branches to obtain the product rule, but the verification of that implication is treated as conditional on this statement.
why it matters
H_PhiMultiplicative supplies the key hypothesis for aczel_classification_conditional, which completes the Aczél classification of d'Alembert solutions into cosh and cos forms. It supports derivation of the hyperbolic-cosine solution for the cost function in Recognition Science, consistent with unbounded J-cost growth. The declaration touches the open question of formalizing the continuous multiplicative Cauchy equation to reach the exponential form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.