forced_factorization_unique
plain-language theorem explainer
Under explicit certificate and rigidity hypotheses on a ratio-cost scaffold, any cost C factors uniquely through the realized image of the canonical J-cost and, separately, is uniquely a function of the observable alone. CPT verification cites this as the strongest currently proved forced-factorization package. The proof is a two-branch constructor that invokes the unique cost reparametrization and the unique state-free profile lemmas.
Claim. Let $R$ be a ratio-cost scaffold on types $S,O$ (positive embeddings into $\mathbb{R}$) and $C:S\times O\to\mathbb{R}$. Assume certificate hypotheses: $C$ depends only on the ratio coordinate and on the canonical cost $J(\mathrm{ratio})$. Assume rigidity: $C$ is independent of the state $s\in S$. Then there is a unique $\varphi$ on the realized cost image such that $C(s,o)=\varphi(J(\mathrm{ratio}(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
This module is the hypothesis-explicit Lean layer for CPT forced factorization: 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.
A RatioCostSpace supplies positive maps $\iota_S:S\to\mathbb{R}$ and $\iota_O:O\to\mathbb{R}$. The ratio coordinate is their quotient; the canonical cost is $J$ of that ratio, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness). CostCode is the subtype of reals in the image of that canonical cost on $S\times O$.
CertificateHypotheses packages two functional dependences: equal ratios imply equal $C$, and equal canonical costs imply equal $C$. RigidityHypotheses asserts full state-independence: $C(s_1,o)=C(s_2,o)$ for all states. The theorem bundles both layers into one uniqueness statement.
proof idea
Term/tactic hybrid: constructor splits the conjunction. The left conjunct is discharged by existsUnique_cost_reparam R C h, which builds the unique reparametrization $\varphi$ on CostCode from the certificate bundle (ratio and cost dependence). The right conjunct is discharged by existsUnique_state_profile R C hRig, which uses rigidity to produce the unique observable profile $\psi:O\to\mathbb{R}$. No further algebraic work sits in this declaration; it is a thin packaging of the two uniqueness lemmas.
why it matters
This is the strongest bundled forced-factorization statement currently proved in the CPT verification layer: unique cost-image reparametrization plus unique state-free profile under named hypothesis bundles. Downstream, CPT_FACTOR_forced_factorization_unique re-exports it for the CPT export surface, and forced_factorization_unique_of_primitives strengthens the hypotheses to primitive ratio-level assumptions (deriving certificate and rigidity from more basic ratio data).
In the Recognition framework this sits under verification of CPT structure rather than the T0–T8 forcing chain itself, but it uses the canonical $J$-cost (T5) as the ratio-induced scaffold. It makes precise the paper claim that observable costs factor through the reciprocal cost image and become state-free once rigidity is granted, without smuggling assumptions into the Lean context.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.