exists_monotone_reparam
plain-language theorem explainer
Under explicit certificate hypotheses on a ratio-cost scaffold, any certificate factors through a monotone map on the realized image of the canonical reciprocal cost. CPT factorization arguments cite this as the existence half of the reparametrization step (paper Thm. 5.1, step 1). The proof builds the map by classical choice of preimages and transfers equality and order via cost-level dependence and cost-monotonicity.
Claim. Let $R$ be a ratio-cost space on types $S,O$ and let $C:S\times O\to\mathbb{R}$ obey the certificate hypotheses (dependence on the ratio and on the canonical reciprocal cost, and monotonicity in that cost). Write $\mathrm{CostCode}(R)$ for the realized image of the canonical cost. Then there exists $\varphi:\mathrm{CostCode}(R)\to\mathbb{R}$ such that $C(s,o)=\varphi(\mathrm{canCost}_R(s,o))$ for all $s,o$, and $\varphi$ is monotone along the canonical-cost order at fixed state $s$.
background
This module is the hypothesis-explicit Lean layer for CPT forced factorization: a ratio-induced canonical cost scaffold, 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 equips states $S$ and observations $O$ with positive real embeddings; the ratio coordinate and the canonical reciprocal cost are built from those embeddings. The certificate $C:S\to O\to\mathbb{R}$ is an arbitrary real-valued profile. CertificateHypotheses packages the working assumptions: equal ratios imply equal $C$, equal canonical costs imply equal $C$, and $C$ is monotone in the canonical cost at fixed state. CostCode is the subtype of reals that actually arise as canonical costs, so reparametrizations are not forced to be defined on all of $\mathbb{R}$.
Upstream cost language in the monolith (J-cost of recognition events, derived costs of multiplicative recognizers, rung-coarsened totals) supplies the physical reading of $C$, but this lemma is purely about factorization of an abstract certificate through the realized cost image.
proof idea
Classical choice defines $\varphi$ on each cost code by picking a witnessing pair $(s,o)$ and evaluating $C$ there. For the representation identity, the chosen pair has the same canonical cost as the input pair; cost-level dependence then equates the two $C$-values, so $C(s,o)=\varphi(\mathrm{canCost}_R(s,o))$.
Monotonicity is the same representation run twice: rewrite both $\varphi$-values as $C(s,o_1)$ and $C(s,o_2)$, apply the certificate's cost-monotonicity hypothesis to the assumed inequality of canonical costs, and transport back. The argument never needs global surjectivity onto $\mathbb{R}$; the subtype CostCode is exactly the domain that choice can hit.
why it matters
This is step 1 of the paper's forced-factorization theorem (Thm. 5.1): existence of a monotone reparametrization on the realized cost image. The export CPT_FACTOR_exists_monotone_reparam is a thin wrapper of this statement; forced_factorization and its export assemble it with the optional rigidity half (state-independence) into the maximal claim-honest package.
Immediately downstream, existsUnique_cost_reparam reuses the existence witness and proves uniqueness of any profile that represents all certificate values on CostCode, so the reparametrization is canonical once it exists. In the broader Recognition stack this sits in the verification layer above the J-cost / RCL forcing chain (T5 J-uniqueness and the composition law), converting abstract certificate data into a monotone function of the canonical reciprocal cost without overclaiming continuum-wide surjectivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.