is
plain-language theorem explainer
Any real function meeting the Jensen-sketch bounds equals the standard J-cost on the positive reals. The certificate is always verified: a trivial packaging fact, not the substantive T5 uniqueness theorem. Proof is a short tactic that applies positive-ray transport. Cite this only as exp-axis-to-ray transport; cite the law-of-logic cost theorem for real T5 uniqueness.
Claim. For every packaging witness and every $F:\mathbb{R}\to\mathbb{R}$ satisfying the Jensen-sketch hypotheses (which already force $F=J$ on the exponential axis), and for every $x>0$, one has $F(x)=J(x)$, where $J(x)=(x+x^{-1})/2-1$ is the standard J-cost.
background
Recognition Science forces a unique reciprocal cost $J$ on $(0,\infty)$ as step T5 of the forcing chain. The genuine uniqueness theorem is the law-of-logic cost result in the functional-equation module: reciprocal symmetry, unit normalization, the Recognition Composition Law, calibration, and continuity force $F=J$ via the Aczél/d'Alembert classification, with no caller-supplied regularity parameters.
This module is only a packaging certificate. The module header states the honesty correction explicitly: the Jensen-sketch hypotheses already include both $F(e^t)\le J(e^t)$ and $J(e^t)\le F(e^t)$, so they pin $F=J$ on the exponential axis. Passing from that axis to the positive ray is pure transport along $\exp/\log$ surjectivity. Hypothesis is essentially the conclusion; no independent uniqueness content lives here.
The certificate structure is a unit-like witness. Its verification predicate asserts the transport claim: every Jensen-sketch $F$ agrees with $J$ at every positive real.
proof idea
The verification predicate is the $\forall F$ statement above. The theorem that every certificate satisfies it is a four-step tactic proof: introduce $F$, the Jensen-sketch instance, the point $x$, and the positivity hypothesis $hx$; then close by exact on the positive-ray uniqueness transport lemma applied to $hx$. No algebraic work occurs in this file; the lemma already carries the axis-to-ray step.
why it matters
T5 in the Unified Forcing Chain is J-uniqueness: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, is the unique cost compatible with the Recognition Composition Law and the standard normalizations. Downstream physics (phi fixed point, eight-tick octave, $D=3$, the mass ladder) sits on that uniqueness.
This declaration does not supply that uniqueness. The module doc insists one must cite the law-of-logic cost theorem (and its Aczél proof) for T5 claims, and cite this certificate only as the trivial packaging/transport step. Used-by is empty: nothing downstream should treat this as the crown-jewel uniqueness result. Its place is audit hygiene: a named, simp-friendly witness that the packaging predicate holds, so verification dashboards can mark the T5 certificate slot green without overstating the math.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.