CPT_FACTOR_phi_independent_of_state
plain-language theorem explainer
Under an explicit rigidity hypothesis that costs do not depend on the state, the bivariate cost equals a single state-free profile on observables. CPT consumers cite this as the rigidity step of paper Theorem 5.1 (forced factorization). The export is a one-line term wrapper around the core ForcedFactorization lemma.
Claim. Let $S$ be an inhabited type of states and $O$ a type of observables, with a ratio-cost scaffold (positive real embeddings of both). Let $C:S\to O\to\mathbb{R}$. If the rigidity hypotheses hold—in particular $C(s_1,o)=C(s_2,o)$ for all states $s_1,s_2$ and observables $o$—then there exists $\psi:O\to\mathbb{R}$ such that $C(s,o)=\psi(o)$ for every $s$ and $o$.
background
The CPT export surface collects citation-friendly, fully proved aliases for the continuous-parameter theorem layer. Items tagged CPT_FACTOR_* map to paper Theorem 5.1 (forced factorization).
A ratio-cost scaffold supplies positive embeddings of states and observables into $\mathbb{R}$. The rigidity hypothesis bundle packages the assumption that certificate values ignore the state: for all $s_1,s_2$ and $o$, $C(s_1,o)=C(s_2,o)$.
The upstream core result states the same conclusion internally: "if certificate values are state-independent by hypothesis, there exists a single state-free profile $\psi$ representing all $C,s,_$."
proof idea
One-line term wrapper that applies the core ForcedFactorization state-independence theorem. That core proof builds $\psi$ by evaluating $C$ at the default inhabitant of $S$, then uses the rigidity hypothesis to erase dependence on the chosen state.
why it matters
Supplies the rigidity half of paper Theorem 5.1 in the stable CPT export surface, alongside the monotone-reparametrization and assembled forced-factorization uniqueness aliases in the same family. No downstream dependents are recorded yet; the point of the export is a citable name outside the internal ForcedFactorization module. In the Recognition stack this licenses treating costs as pure observable profiles once rigidity is granted, which the neighboring pipeline and optimality exports then compose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.