CPT_FACTOR_forced_factorization
plain-language theorem explainer
Under certificate and rigidity hypotheses on a ratio cost space, any admissible cost C factors two ways at once: as a reparametrization of the canonical cost on the cost-code quotient, and as a purely observation-dependent profile independent of state. Citation target for paper Theorem 5.1 (forced factorization). Proof is a two-line assembly of the monotone-reparam existence lemma and the state-independence lemma.
Claim. Let $R$ be a ratio cost space on states $S$ and observations $O$, and let $C:S\to O\to\mathbb{R}$. If the certificate hypotheses and rigidity hypotheses hold for $(R,C)$, then (i) there exists $\varphi$ on the cost-code of $R$ such that $C(s,o)=\varphi([R.\mathrm{canonicalCost}(s,o)])$ for all $s,o$, and (ii) there exists $\psi:O\to\mathbb{R}$ such that $C(s,o)=\psi(o)$ for all $s,o$ (state-free factorization).
background
This module is the CPT export surface: citation-friendly aliases for the fully proved CPT formalization layer, with no sorry and no new axioms. The CPT_FACTOR_* family maps to paper Theorem 5.1 (forced factorization).
A ratio cost space packages the structural data needed to compare costs on positive ratios between states and observations, including a canonical cost. Certificate hypotheses certify that $C$ is compatible with that structure (so a monotone reparametrization through the cost-code exists). Rigidity hypotheses force the cost to ignore the state coordinate, leaving only an observation profile.
Upstream cost notions in the wider stack (J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen total cost) supply the Recognition-Science meaning of "cost": non-negative functionals built from the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ forced at T5. Here those enter only as ambient vocabulary; the local argument is pure CPT factorization.
proof idea
Term-mode assembly, not a new argument. First, ForcedFactorization.exists_monotone_reparam under the certificate hypotheses yields a cost-code map $\varphi$ and the representation identity $C(s,o)=\varphi([R.\mathrm{canonicalCost}(s,o)])$ (the monotone side-condition is discarded). Second, ForcedFactorization.phi_independent_of_state under the rigidity hypotheses yields $\psi:O\to\mathbb{R}$ with $C(s,o)=\psi(o)$ for all $s,o$. The conclusion is the pair of existential witnesses packaged as a conjunction.
why it matters
Export alias for paper Theorem 5.1, the forced-factorization core of the CPT layer. It sits beside the sibling exports CPT_FACTOR_exists_monotone_reparam, CPT_FACTOR_phi_independent_of_state, and the uniqueness strengthening CPT_FACTOR_forced_factorization_unique, and parallel to the pipeline (CPT_PIPELINE_*), window-identifiability (WINDOW_*), and optimality (CPT_OPT_*) families on the same surface.
In the Recognition framework this is the structural claim that admissible costs cannot carry hidden state dependence once certificate and rigidity hold: they are canonical-cost reparams and pure observation profiles. That is the algebraic backbone for later CPT pipeline soundness and $\varepsilon$-certification. No downstream consumers are recorded on this export itself; it is the citation hook for the paper theorem rather than an internal lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.