CostCode
plain-language theorem explainer
The realized-cost coordinate is the subtype of reals lying in the image of the canonical reciprocal cost on state–observable pairs. CPT factorization proofs cite it as the exact domain for monotone reparametrizations, avoiding any claim of global surjectivity onto ℝ. The declaration is a one-line subtype abbreviation of that image set.
Claim. Given a ratio-cost space $R$ on types $S$ and $O$, the encoded realized-cost coordinate is the subtype $\{ t \in \mathbb{R} \mid t \in \mathrm{im}(C_{\mathrm{can}}) \}$, where $C_{\mathrm{can}}$ is the canonical cost on $S \times O$ induced by $R$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate hypotheses stated openly, existence of a reparametrization on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions are used.
A ratio-cost space packages positive real embeddings $\iota_S : S \to \mathbb{R}{>0}$ and $\iota_O : O \to \mathbb{R}{>0}$. From those one forms a ratio coordinate and a canonical reciprocal cost on pairs $(s,o)$. The cost image is the set of all real values attained by that canonical cost as $(s,o)$ ranges over $S \times O$.
The encoded coordinate is simply that image packaged as a subtype of $\mathbb{R}$. Downstream reparametrization statements take maps out of this subtype so they only quantify over values the cost actually hits.
proof idea
Pure definitional abbreviation: the type is the subtype ${ t : \mathbb{R} // t \in \mathrm{CostImage}, R }$. No proof obligations; Mathlib subtype infrastructure supplies membership and coercion.
why it matters
This coordinate is the precise domain for the monotone reparametrization layer of paper Theorem 5.1. Export theorems CPT_FACTOR_exists_monotone_reparam, CPT_FACTOR_forced_factorization, and the uniqueness variants all quantify $\varphi$ as a map out of this subtype, matching the in-module statement that existence is on the realized cost image and does not overclaim global surjectivity onto $\mathbb{R}$.
Local consumers include exists_monotone_reparam, existsUnique_cost_reparam, forced_factorization, and certificate_depends_on_ratio. The construction keeps the factorization scaffold honest: certificate hypotheses force dependence on the ratio, then a monotone reparam on this code recovers the observed cost, with rigidity supplying state-free uniqueness when assumed.
It sits in the verification spine rather than the T0–T8 forcing chain; it does not itself force $J$, $\varphi$, or $D=3$, but it is the typed witness space those CPT claims use once a ratio-cost scaffold is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.