canonicalCost
plain-language theorem explainer
Canonical ratio-induced cost on a state–observer pair: evaluate the RS J-cost on the positive ratio coordinate of a ratio-cost space. CPT forced-factorization and monotone-reparametrization theorems cite it as the baseline cost against which certificates are compared. The body is a one-line composition of Jcost with the ratio map.
Claim. Given a ratio-cost space $R$ on types $S$ and $O$ (positive embeddings $\iota_S:S\to\mathbb{R}_{>0}$, $\iota_O:O\to\mathbb{R}_{>0}$) and a pair $(s,o)\in S\times O$, the canonical cost is $J\bigl(r_R(s,o)\bigr)$, where $r_R$ is the positive ratio coordinate of $R$ and $J(x)=(x+x^{-1})/2-1$.
background
The module is the hypothesis-explicit Lean layer for CPT forced factorization: ratio-induced canonical cost, explicit certificate hypotheses, existence of a reparametrization on the realized cost image, and state-independence only under an explicit rigidity hypothesis. No hidden assumptions.
A RatioCostSpace on types $S$ (states) and $O$ (observers) supplies positive real embeddings $\iota_S$, $\iota_O$ and a derived ratio coordinate $r_R(s,o)$. The RS recognition cost is the unique T5 functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the reciprocal cost forced by the Recognition Composition Law. Upstream, the same $J$ appears as the recognition cost of a positive ratio and as the derived cost of multiplicative recognizers.
This definition simply feeds that ratio into $J$, producing the baseline cost used throughout the factorization layer.
proof idea
Definition, not a proof. One-line composition: apply Cost.Jcost to the ratio coordinate ratio R s o. No lemmas, tactics, or side conditions.
why it matters
This is the cost scaffold named in the module doc as the first ingredient of the paper's forced-factorization claims (Thm. 5.1). Downstream, CostImage is exactly the range of this map on $S\times O$; CertificateHypotheses and the reparametrization existence theorems compare an arbitrary certificate $C$ against it. Export theorems CPT_FACTOR_exists_monotone_reparam, CPT_FACTOR_forced_factorization, and the uniqueness variants all take a ratio-cost space and route through this canonical cost. In the RS chain it is the concrete T5 $J$ instance used to force factorization of CPT-style certificates into a monotone reparametrization of $J$ on the realized cost image, with state-free uniqueness only under rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.