aczel_classification_conditional
Under the d'Alembert equation with H(0)=1, continuity, H(t)≥1 everywhere, and the two bridge hypotheses on the auxiliary phi, H must be of the form cosh(λ t) for some real λ. Recognition Science derivations of the J-cost from the Recognition Composition Law invoke this to fix the hyperbolic shape of the cost function. The argument first builds the auxiliary phi from H, verifies that phi is continuous, positive, normalized at zero and multiplicative, applies the supplied Cauchy-to-exponential bridge to obtain an exponential representation, and,
claimLet $H:ℝ→ℝ$ be continuous, satisfy $H(0)=1$, the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and $H(t)≥1$ for all $t$. Let $φ(t):=H(t)+√(H(t)^2-1)$. Suppose $φ$ is multiplicative whenever its arguments satisfy the lower bound $H≥1$, and suppose every continuous positive multiplicative function normalized at zero is an exponential. Then there exists $λ∈ℝ$ such that $H(t)=cosh(λ t)$ for all $t$.
background
In the Recognition Science setting the shifted cost $H(x)=J(x)+1$ converts the Recognition Composition Law into the d'Alembert functional equation $H(xy)+H(x/y)=2H(x)H(u)$. The module isolates the cosh branch of Aczél's classification: when $H$ is continuous, $H(0)=1$ and $H≥1$ everywhere, one defines the auxiliary $φ(t)=H(t)+√(H(t)^2-1)$. The referenced definitions supply the two bridge statements: $H_PhiMultiplicative$ asserts that $φ$ is multiplicative under the lower bound, while $H_CauchyToExponential$ asserts that any continuous positive multiplicative function with value 1 at zero is an exponential. Upstream, CostAlgebra.H records the translation $H=J+1$ and FunctionalEquation.H records the same reparametrization for the general functional equation.
proof idea
The tactic proof first constructs the auxiliary $φ$ and records its continuity, positivity, normalization at zero and multiplicativity by direct appeal to the supplied lemmas phi_pos, phi_at_zero and H_PhiMultiplicative. It then invokes the hypothesis H_CauchyToExponential on $φ$ to obtain $φ(t)=exp(λ t)$. The recovery theorem H_from_phi rewrites $H(t)=(φ(t)+φ(t)^{-1})/2$; substituting the exponential and invoking the identity $cosh(x)=(e^x+e^{-x})/2$ yields the claimed form.
why it matters in Recognition Science
This is the full Aczél classification for the unbounded (cosh) branch, the only branch relevant to Recognition Science because the J-cost grows without bound. It closes the identification of the cost function once the Recognition Composition Law has produced the d'Alembert equation and the auxiliary multiplicative property has been verified. The result sits inside the T5 J-uniqueness step of the forcing chain and supplies the explicit hyperbolic solution that later mass-ladder and Berry-threshold arguments rely upon.
scope and limits
- Does not discharge the two bridge hypotheses H_PhiMultiplicative and H_CauchyToExponential.
- Does not treat the bounded (cosine) branch of the Aczél classification.
- Assumes the global lower bound H(t)≥1; does not derive it from the Recognition Composition Law.
- Does not produce an explicit value for the constant λ from first principles.
formal statement (Lean)
120theorem aczel_classification_conditional
121 (H : ℝ → ℝ)
122 (h_one : H 0 = 1)
123 (h_cont : Continuous H)
124 (h_dA : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u)
125 (h_phi_mult : H_PhiMultiplicative H)
126 (h_cauchy : H_CauchyToExponential)
127 (h_ge_one : ∀ t, 1 ≤ H t) :
128 ∃ lam : ℝ, ∀ t, H t = Real.cosh (lam * t) := by
proof body
Tactic-mode proof.
129 have h_phi_cont : Continuous (phi H) := by
130 unfold phi
131 exact h_cont.add ((h_cont.pow 2).sub continuous_const).sqrt
132 have h_phi_pos : ∀ t, 0 < phi H t := fun t => phi_pos H t (h_ge_one t)
133 have h_phi_zero : phi H 0 = 1 := phi_at_zero H h_one
134 have h_phi_cauchy : ∀ t u, phi H (t + u) = phi H t * phi H u :=
135 fun t u => h_phi_mult t u (h_ge_one t) (h_ge_one u)
136 obtain ⟨lam_, hlam⟩ := h_cauchy (phi H) h_phi_cont h_phi_pos h_phi_zero h_phi_cauchy
137 refine ⟨lam_, fun t => ?_⟩
138 have h_phi_exp : phi H t = Real.exp (lam_ * t) := hlam t
139 have h_phi_neg : phi H (-t) = Real.exp (-(lam_ * t)) := by
140 rw [hlam (-t)]; ring_nf
141 have h_H_from_phi := H_from_phi H t (h_ge_one t)
142 rw [h_phi_exp] at h_H_from_phi
143 rw [Real.cosh_eq]
144 convert h_H_from_phi using 1
145 rw [exp_neg]
146
147end
148
149end IndisputableMonolith.Cost.CauchyAuxiliary