CPT_FACTOR_forced_factorization_unique
plain-language theorem explainer
Under certificate and rigidity hypotheses on a ratio cost space, any admissible cost factors uniquely through the canonical J-cost image and is uniquely independent of state on the observation side. CPT and verification authors cite this as the strong uniqueness form of paper Theorem 5.1. The export is a one-line term application of the upstream ForcedFactorization uniqueness lemma.
Claim. Let $R$ be a ratio cost space on states $S$ and observations $O$, and let $C:S\to O\to\mathbb{R}$ satisfy the certificate hypotheses and the rigidity hypotheses relative to $R$. Then there is a unique map $\varphi$ on the realized image of the canonical cost such that $C(s,o)=\varphi(J(\mathrm{ratio}_R(s,o)))$ for all $s,o$, and there is a unique $\psi:O\to\mathbb{R}$ such that $C(s,o)=\psi(o)$ for all $s,o$.
background
The CPT export module is a citation surface for the forced-factorization layer of the paper. All aliases are fully proved (no sorry, no new axioms). The CPT_FACTOR_* family maps to paper Theorem 5.1.
A ratio cost space packages ratio data on pairs $(s,o)$. The canonical cost is $J$ of that ratio, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The cost code is the subtype of reals realized as such canonical values. Certificate hypotheses are the structural assumptions that make $C$ a certified cost relative to $R$; rigidity hypotheses strengthen those assumptions so factorization is unique, not merely existent.
Upstream, the non-export lemma forced_factorization_unique in ForcedFactorization carries the real content; this declaration only renames it for paper citation.
proof idea
One-line term wrapper. The body applies ForcedFactorization.forced_factorization_unique to the ratio cost space $R$, the cost $C$, the certificate bundle, and the rigidity bundle. No local tactics, rewrites, or case splits: both unique-existence claims (cost-image reparametrization $\varphi$ and state-free profile $\psi$) are inherited verbatim from that upstream lemma.
why it matters
This is the strong uniqueness half of paper Theorem 5.1 (forced factorisation), exported under the CPT_FACTOR_* citation family. Sibling exports give existence of a monotone reparametrization and state-independence of the profile; this declaration upgrades both layers to $\exists!$.
In Recognition Science the point is structural: once certificate and rigidity hold, observable costs cannot hide an alternative code. They must factor through the unique $J$-cost on ratio data (T5 $J$-uniqueness in the forcing chain) and must be constant in the state argument. That locks the CPT cost model to the Recognition Composition Law's cost rather than an arbitrary surrogate.
The dependency graph currently lists no downstream users; the declaration is an export endpoint meant for external citation and for composing with the pipeline, optimality, and $\varepsilon$-certification aliases in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.