RatioCostSpace
plain-language theorem explainer
Packages a state space and an observable space with strictly positive real embeddings, so every pair determines a positive ratio coordinate. CPT factorization theorems cite this as the ambient scaffold on which certificate and rigidity hypotheses are stated. It is a pure data structure: four fields, no proof obligations beyond positivity.
Claim. A ratio-cost space on types $S$ (states) and $O$ (observables) consists of maps $\iota_S:S\to\mathbb{R}$ and $\iota_O:O\to\mathbb{R}$ such that $\iota_S(s)>0$ for all $s\in S$ and $\iota_O(o)>0$ for all $o\in O$. The induced ratio coordinate is the positive quotient formed from these embeddings; the canonical cost is the $J$-cost of that ratio.
background
The module is the hypothesis-explicit Lean layer for the paper's CPT forced-factorization claims. It isolates a ratio-induced canonical cost scaffold, states certificate hypotheses openly, and separates existence of a monotone reparametrization on the realized cost image from state-independence (which needs an explicit rigidity hypothesis). No hidden assumptions are used.
Upstream, recognition cost is the doubled $J$-cost on positive ratios: $J(x)=(x+x^{-1})/2-1$, forced unique by the Recognition Composition Law (T5). Reciprocal events invert the ratio; multiplicative recognizers induce cost via a comparator on positive reals. Cosmological rung coarsening sums a ratio weight over events. The present structure only supplies the positive embeddings that make those ratio coordinates well-defined on abstract $S$ and $O$.
Sibling fields in the same namespace build the ratio coordinate, the canonical cost $J(\mathrm{ratio}(s,o))$, the realized cost image, and the certificate/rigidity hypothesis bundles consumed by the export theorems.
proof idea
No proof. The declaration is a structure with four fields: two real-valued embeddings and two positivity axioms. Downstream definitions (ratio coordinate, canonical $J$-cost) and hypothesis bundles are defined by projection and composition on these fields; nothing is discharged here.
why it matters
This is the ambient type for every CPT factorization export. Paper Thm. 5.1 step 1 (existence of a monotone reparametrization on the cost image), the rigidity step (state-independence of the profile), the assembled forced-factorization theorem, and both uniqueness forms (certificate-level and primitive-level) all take an instance of this structure as their first argument.
It ties the verification layer to the T5 $J$-uniqueness landmark: once ratios are positive, the canonical cost is forced to be $J$, and factorization arguments can ask whether an arbitrary cost $C:S\times O\to\mathbb{R}$ is a monotone reparametrization of that image, and whether the reparametrization can be chosen state-free under rigidity. Without this scaffold the certificate hypotheses have nowhere to live.
The structure itself does not close any open physics claim; it makes the Lean shape of those claims auditable and hypothesis-explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.