forced_factorization
plain-language theorem explainer
Under explicit certificate and rigidity hypotheses on a ratio-cost scaffold, any cost C factors through the realized canonical-cost image by a reparametrization, and is simultaneously independent of the state (depends only on the observable). CPT factorization arguments cite this as the strongest currently claim-honest Lean packaging of forced factorization. The proof packages monotone reparametrization existence with the state-independence lemma.
Claim. Let $S$ be inhabited and $R$ a ratio-cost space on types $S,O$ (positive real embeddings of states and observables). Let $C:S\to O\to\mathbb{R}$. If $C$ satisfies the certificate hypotheses (equal canonical reciprocal cost implies equal $C$) and the rigidity hypothesis (independence of the state variable), then there exists $\varphi$ on the realized cost image such that $C(s,o)=\varphi(\mathrm{canonicalCost}_R(s,o))$ for all $s,o$, and there exists $\psi:O\to\mathbb{R}$ with $C(s,o)=\psi(o)$ for all $s,o$.
background
This module is the hypothesis-explicit Lean layer for the paper's CPT forced-factorization claims: ratio-induced canonical cost, certificate hypotheses stated openly, reparametrization on the realized cost image, and state-independence only under an explicit rigidity bundle. No hidden assumptions are used.
A ratio-cost space supplies positive embeddings $\iota_S:S\to\mathbb{R}$ and $\iota_O:O\to\mathbb{R}$; the ratio coordinate and the canonical reciprocal cost are built from those embeddings. Certificate hypotheses require that equal ratio (and, more strongly, equal canonical cost) imply equal certificate value $C$. Rigidity is the separate demand that $C$ is independent of the state argument. The cost code is the subtype of reals in the realized cost image, the domain on which reparametrization witnesses live.
Upstream cost language in the monolith (J-cost of recognition events, derived costs of multiplicative recognizers, rung-coarsened recognition sums) supplies the ambient meaning of $C$, but this theorem stays at the abstract scaffold level.
proof idea
Term-mode packaging of two prior lemmas. First, destructure the existence of a monotone reparametrization on the cost image under the certificate bundle: that yields $\varphi$ and the pointwise representation $C(s,o)=\varphi(\langle\mathrm{canonicalCost},s,o,\ldots\rangle)$; monotonicity is discarded. Second, destructure state-independence under the rigidity bundle to obtain $\psi:O\to\mathbb{R}$ with $C(s,o)=\psi(o)$. Return the pair $(\varphi,\psi)$ with both witnesses. No new algebra is proved here.
why it matters
This is the assembled forced-factorization statement at the current maximal claim-honest level: cost-image reparametrization plus optional state-independence under explicit rigidity. It is the strongest bundled theorem the module currently proves, matching the module goal of capturing the paper's factorization claims without smuggling assumptions.
In the Recognition framework it sits in the verification/CPT lane rather than the T0–T8 forcing chain itself. It constrains how admissible costs may depend on ratio data and observables once certificate and rigidity hypotheses are granted, which is the Lean shape needed before stronger uniqueness or physical identification steps. No downstream consumers are wired yet (used_by is empty), so it is a terminal packaging lemma for the present layer, ready for CPT uniqueness or profile-classification arguments to cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.