existsUnique_state_profile
plain-language theorem explainer
Under an explicit rigidity hypothesis that cost is independent of the state variable, there is a unique state-free profile ψ on observables such that C(s,o)=ψ(o) for every state and observable. Anyone assembling CPT forced-factorization uniqueness cites this. The proof builds ψ from any default state and recovers uniqueness by function extensionality from rigidity.
Claim. Let $S$ be inhabited and let $C:S\to O\to\mathbb{R}$ be a real-valued cost on a ratio-cost space. If rigidity holds, i.e. $C(s_1,o)=C(s_2,o)$ for all states $s_1,s_2$ and observables $o$, then there exists a unique profile $\psi:O\to\mathbb{R}$ such that $C(s,o)=\psi(o)$ for all $s\in S$ and $o\in O$.
background
This module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost scaffold, certificate hypotheses stated openly, existence of a reparametrization on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions are used.
A ratio-cost space packages positive embeddings of states $S$ and observables $O$ into $\mathbb{R}$, supplying the ratio coordinate that feeds the canonical reciprocal cost. The cost $C:S\to O\to\mathbb{R}$ is the object being factorized. Rigidity is the bare Prop bundle asserting $C(s_1,o)=C(s_2,o)$ for all pairs of states and every observable: pure state-independence, nothing more.
Upstream cost notions in the framework (J-cost of a recognition event, derived cost of a multiplicative recognizer, total recognition cost under a ratio weight) motivate why one expects a state-free profile, but this lemma treats rigidity as an explicit hypothesis rather than deriving it.
proof idea
Term-mode existence-and-uniqueness. Existence: take any default state (from Inhabited S) and set $\psi(o):=C(\mathrm{default},o)$. For arbitrary $s,o$, rigidity's independent_of_state equates $C(s,o)$ with $C(\mathrm{default},o)$, so $C$ factors through $\psi$. Uniqueness: if another $\psi'$ agrees with $C$ on all pairs, evaluate at the default state and apply function extensionality on $O$; the two profiles coincide pointwise. No external lemmas beyond the rigidity field and funext.
why it matters
This is the state-independence half of the module's maximal claim-honest factorization package. It feeds directly into forced_factorization_unique, whose doc-comment calls it the strongest bundled statement currently proved: both the cost-image reparametrization and the state-free profile are unique under explicit hypothesis bundles.
In the paper narrative, forced factorization says certificate values determine a unique observable profile once rigidity is granted. Keeping rigidity as a named hypothesis (rather than a silent axiom) is the module's design point: the Lean layer stays claim-honest. The result does not itself touch T5 J-uniqueness or the RCL; it sits in the verification layer that packages those cost structures into CPT-facing uniqueness statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.