ratio
plain-language theorem explainer
Defines the positive real ratio coordinate of a state–observer pair by dividing the two positive embeddings of a ratio-cost scaffold. CPT factorization and reciprocal-cost arguments cite it as the raw multiplicative input to the canonical J-cost. The body is a one-line quotient of the scaffold maps.
Claim. Given a ratio-cost scaffold $R$ on types $S$ and $O$ (positive real embeddings $\iota_S:S\to\mathbb{R}_{>0}$ and $\iota_O:O\to\mathbb{R}_{>0}$), the ratio of a pair $(s,o)$ is the positive real $\iota_S(s)/\iota_O(o)$.
background
The module CPT Forced Factorization packages the paper's forced-factorization claims in hypothesis-explicit Lean form: a ratio-induced canonical cost scaffold, named certificate and rigidity hypotheses, reparametrization on the realized cost image, and state-independence only under explicit rigidity. No hidden assumptions are used.
A RatioCostSpace is the local scaffold: two maps $\iota_S:S\to\mathbb{R}$ and $\iota_O:O\to\mathbb{R}$ that land strictly positive. The ratio coordinate is the multiplicative comparison of those embeddings. Upstream cost constructions (observer J-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient J-cost, rung-coarsened weighted sums) all treat positive ratios as the natural argument of the Recognition Composition Law cost $J$, so this quotient is the interface between abstract state/observer data and that cost.
proof idea
Definitional one-liner: evaluate the two positive embeddings of the scaffold and form their real quotient. No lemmas or tactics; positivity of the result is inherited from the scaffold axioms $\iota_S>0$ and $\iota_O>0$.
why it matters
This is the raw multiplicative input to the canonical ratio-induced cost used throughout CPT factorization. Downstream algebra uses it (or the same ratio idea) for normalization $J(1)=0$, reciprocal symmetry $J(x)=J(1/x)$, and the positive domain of recognition cost systems. Applied modules feed ratios into J-cost for pitch JND bounds, exoplanet eccentricity penalties and moon-mass habitability bands, and mass-to-light derived quantities. In the forcing chain it sits under T5 J-uniqueness and the RCL: once ratios are formed, the unique cost is $J(x)=\cosh(\log x)-1$. It does not itself force factorization; sibling certificate and rigidity hypotheses carry that load.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.