pith. sign in
theorem

washburn_uniqueness_aczel

proved
show as:
module
IndisputableMonolith.Cost.FunctionalEquation
domain
Cost
line
1076 · github
papers citing
25257 papers (below)

plain-language theorem explainer

Washburn's uniqueness theorem shows that any continuous reciprocal cost on positive reals obeying the Recognition Composition Law, normalization at unity, and unit calibration must equal the J-cost. Researchers citing T5 in the forcing chain or logical derivations of cost invoke this result. The proof converts the composition law to a d'Alembert equation on the shifted H function, applies the Aczél smoothness lemma to identify the cosh solution, and matches it to Jcost via the exponential substitution.

Claim. Let $F : (0,∞) → ℝ$ satisfy $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, the Recognition Composition Law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for all $x,y > 0$, the calibration condition that the second derivative of $t ↦ F(e^t)$ at $t=0$ equals 1, and continuity on $(0,∞)$. Then $F(x) = J(x)$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$.

background

The module supplies lemmas for the T5 cost uniqueness proof in the Recognition Science forcing chain. Reciprocal cost requires $F(x) = F(1/x)$ for $x > 0$; normalized means $F(1) = 0$; the composition law is the Recognition Composition Law (RCL) on positive ratios; calibrated is the condition $G''(0) = 1$ where $G(t) = F(e^t)$. The Aczél smoothness package guarantees that continuous solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2H(t)H(u)$ with $H(0)=1$ are $C^∞$. Upstream, the composition law is equivalent to the cosh-add identity on $G$, and $H$ is the shift $J + 1$ that turns the RCL into standard d'Alembert form.

proof idea

Fix $x > 0$. Reciprocity gives symmetry $F(y) = F(y^{-1})$. The equivalence lemma converts the composition law into CoshAddIdentity on $G_F$. Define $G_F$ and $H_F = G_F + 1$; record $G_F(0) = 0$ and $H_F(0) = 1$ from normalization, obtain continuity of both transforms, derive the direct cosh-add on $G_F$, and obtain the d'Alembert equation on $H_F$. Calibration supplies the second derivative of $H_F$ at zero equal to 1. The d'Alembert_cosh_solution_aczel lemma then forces $H_F(t) = cosh(t)$, so $G_F(t) = cosh(t) - 1$. The change of variables $x = exp(log x)$ matches this to the known expression for Jcost.

why it matters

This supplies the clean T5 uniqueness statement in the forcing chain, feeding directly into cost_algebra_unique_aczel and the logical formalization results J_is_unique_cost_under_logic and RCL_is_unique_functional_form_of_logic. It anchors the derivation of the phi-ladder and alpha band from the single functional equation by internalizing the Aczél axiom and removing extra regularity hypotheses. The result thereby closes the uniqueness argument for the canonical reciprocal cost under the Recognition Composition Law.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 25257)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.