existsUnique_cost_reparam
plain-language theorem explainer
Under explicit certificate hypotheses, any cost profile C on a ratio-cost scaffold admits a unique reparametrization φ on the realized cost codes: C(s,o) equals φ of the canonical cost of (s,o). CPT factorization arguments cite this to pin the cost-image factor once and for all. The proof takes existence from the monotone reparametrization lemma and proves uniqueness by evaluating both candidates on a common code representative.
Claim. Let $R$ be a ratio-cost scaffold on state space $S$ and observable space $O$, and let $C:S\times O\to\mathbb{R}$ satisfy the certificate hypotheses (equal ratio implies equal $C$, and equal canonical cost implies equal $C$). Then there exists a unique map $\varphi$ from the realized cost codes of $R$ into $\mathbb{R}$ such that $C(s,o)=\varphi(\mathrm{canonicalCost}_R(s,o))$ for all $s,o$.
background
This module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate assumptions stated openly, existence of a reparametrization on the realized cost image, and state-independence only under a separate rigidity hypothesis. No hidden assumptions are smuggled in.
A RatioCostSpace supplies positive embeddings $\iota_S:S\to\mathbb{R}$ and $\iota_O:O\to\mathbb{R}$. From these one forms a ratio coordinate and a canonical reciprocal cost; the image of that cost is packaged as CostCode, the subtype of realized cost values. Certificate hypotheses require that $C$ depend only on the ratio (hence only on the canonical cost): equal ratios give equal $C$, and equal canonical costs give equal $C$.
The companion existence result produces a monotone reparametrization on those codes. The present theorem upgrades that existence to uniqueness of any representing profile on the cost codes.
proof idea
Existence is imported in one step: exists_monotone_reparam supplies a witness $\varphi_0$ that represents $C$ on every code (monotonicity is discarded). Uniqueness is pure pointwise comparison. Fix any other representing $\varphi$. For an arbitrary code $t=\langle r,\langle(s,o),hp\rangle\rangle$, subtype extensionality identifies the canonical-code packing of $(s,o)$ with $t$. Transporting both representation equations along that identification yields $C(s,o)=\varphi_0(t)$ and $C(s,o)=\varphi(t)$, so $\varphi(t)=\varphi_0(t)$. funext finishes.
why it matters
Forced factorization in the CPT verification layer needs a single, rigid cost-image factor rather than a family of equivalent rewrites. This uniqueness lemma is the cost-code half of that rigidity: once certificate hypotheses hold, the reparametrization on realized costs is canonical.
The sole downstream consumer is forced_factorization_unique, the strongest bundled statement currently proved in the module: both the cost-image reparametrization and the state-free profile are unique under the explicit certificate and rigidity hypothesis bundles. Together they close the Lean shape of the paper's forced-factorization claim without silent assumptions.
In the broader Recognition stack this sits in verification rather than the T0–T8 forcing chain; it certifies that certificate data factor cleanly through the canonical cost image before any physical identification is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.