CostImage
plain-language theorem explainer
The realized image of the canonical reciprocal cost on state–observer pairs: the set of all real values that cost actually attains. CPT factorization and reparametrization witnesses cite it as the ambient set for encoded cost coordinates. The body is a one-line range definition of the canonical cost map on S × O.
Claim. Given a ratio-cost scaffold $R$ on types $S$ and $O$ (positive embeddings of states and observers into $\mathbb{R}$), the cost image is the set $\{ \mathrm{canonical\,cost}_R(s,o) : s\in S,\, o\in O \} \subseteq \mathbb{R}$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, certificate and rigidity hypotheses stated openly, and reparametrization only on the realized cost image, with no hidden assumptions.
A RatioCostSpace packages positive real embeddings $\iota_S:S\to\mathbb{R}{>0}$ and $\iota_O:O\to\mathbb{R}{>0}$. From those embeddings one forms a ratio coordinate and the canonical reciprocal cost on pairs $(s,o)$. Across the monolith, recognition cost is the $J$-cost (or a derived comparator cost) on positive ratios; here the same idea is specialized to the CPT scaffold as a map $S\times O\to\mathbb{R}$.
The cost image is simply the set of real numbers that this canonical cost actually hits. Downstream encodings restrict to that set so reparametrization witnesses stay on realized values rather than the whole line.
proof idea
Definitional, not a proof. The set is declared as the range of the map $(s,o)\mapsto \mathrm{canonicalCost},R,s,o$ on $S\times O$. No lemmas are applied; Mathlib Set.range is the only construction.
why it matters
Forced-factorization claims need a precise ambient set for cost coordinates: existence of a reparametrization is stated on realized costs, not on all of $\mathbb{R}$. This definition supplies that set.
It is consumed immediately by the encoded cost type CostCode, the subtype of reals lying in the cost image, which is the coordinate space for reparametrization witnesses in the same module. That keeps certificate and rigidity hypotheses tied to values the canonical cost can produce under the ratio scaffold.
In the broader Recognition picture, cost is $J$-type (T5 uniqueness of $J$, RCL). Here the role is verification hygiene: pin the image so CPT factorization statements remain hypothesis-explicit and do not smuggle domain assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.