T5UniqueCert
plain-language theorem explainer
Empty certificate structure marking the T5 packaging step: any F that already equals J on the exponential axis equals Jcost on (0,∞) by exp/log transport. Cite only as the trivial axis-to-ray packaging; the real uniqueness theorem is law_of_logic_forces_jcost. No proof body: pure marker with Repr.
Claim. Certificate type for the packaging claim: if $F:\mathbb{R}\to\mathbb{R}$ satisfies the Jensen sketch (so already $F(e^t)=J(e^t)$ for all real $t$), then $F=J$ on $(0,\infty)$, where $J(x)=(x+x^{-1})/2-1$. The structure itself carries no fields; it is a named marker for that transport step.
background
Recognition cost on positive ratios is $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$). The class JensenSketch extends reciprocal unit normalization by two axis bounds: $F(e^t)\le J(e^t)$ and $J(e^t)\le F(e^t)$ for all real $t$. Those bounds already force $F=J$ on the exponential axis.
This module is the T5 packaging certificate layer. The module doc states explicitly that the certificate is a packaging tautology: hypothesis already equals the conclusion on the axis, and the ray statement is transport along the surjective $\exp/\log$ correspondence. Substantive T5 uniqueness lives elsewhere (functional equation plus Aczél/d'Alembert classification), not here.
proof idea
No proof body. The declaration is an empty structure with deriving Repr, i.e. a named certificate tag rather than a proved theorem. The mathematical content it names is the one-line transport: from $F\circ\exp=J\circ\exp$ on $\mathbb{R}$ and bijectivity of $\exp:\mathbb{R}\to(0,\infty)$, conclude $F=J$ on $(0,\infty)$. Upstream JensenSketch already supplies the axis equality; nothing further is proved in this structure.
why it matters
Sits in the Verification domain as an honesty-corrected packaging marker for the T5 (J-uniqueness) story in the forcing chain. Framework landmark T5 identifies $J(x)=(x+x^{-1})/2-1$ as the unique recognition cost; the real content is the composition law plus calibration and continuity forcing $F=J$ via the Aczél route.
This certificate must not be cited as that uniqueness theorem. The module doc redirects citations to law_of_logic_forces_jcost in the functional-equation development. No downstream consumers are recorded; the structure exists so verification surfaces can point at a stable name for the trivial axis-to-ray step without overselling it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.