RatioMap
plain-language theorem explainer
A ratio map is a positive real embedding of a configuration type C, the data needed to evaluate the RS cost J on abstract configurations. Anyone building reference structures, balanced configurations, or ratio-induced costed spaces cites it. As a structure definition it carries no proof: it packages a map C → ℝ with a positivity witness.
Claim. A ratio map on a type $C$ is a function $\iota : C \to \mathbb{R}$ together with a proof that $\iota(x) > 0$ for every $x \in C$. Equivalently, it is an embedding of configurations into the positive reals $\mathbb{R}_+$.
background
The module formalizes the Physics of Reference: aboutness as cost-minimizing compression. A symbol $S$ refers to an object $O$ when the ledger link between them minimizes $J$-cost. The canonical cost is the RS functional $J(x) = \frac12(x + 1/x) - 1$ (equivalently $\cosh(\log x) - 1$), defined on positive reals and forced unique by the Recognition Composition Law and the T5 step of the forcing chain.
Abstract configuration types need not be reals. A ratio map supplies the missing bridge: it embeds $C$ into $\mathbb{R}_+$ so that $J$ can be evaluated pointwise. Downstream, the induced costed space sets $J_C(c) := J(\iota(c))$, and balance means $\iota(c) = 1$, which is exactly the zero locus of $J$.
Related cost constructions appear elsewhere (observer-event $J$-cost, multiplicative-recognizer derived cost, rung-coarsened multiset cost). All of them ultimately evaluate a positive-ratio weight; the ratio map is the local packaging of that weight on an arbitrary type.
proof idea
No proof body: this is a structure declaration. It records two fields, an embedding ratio : C → ℝ and a positivity certificate pos : ∀ x, 0 < ratio x. Instantiation is by providing both components; consumers project them with the usual structure accessors.
why it matters
Ratio maps are the entry point for every ratio-induced construction in the reference algebra. They feed ratioInducedCost (costed space with $J_C = J \circ \iota$), the characterization ratio_induced_zero_iff ($J_C(c)=0$ iff $\iota(c)=1$), the predicate IsBalanced, and the theorem balanced_zero_cost. They also underwrite ratioReference, the canonical reference structure between two configuration spaces, and the perfect-reference criterion: reference cost vanishes exactly when the two ratios agree.
In the module thesis this is item 3 (ratio-induced reference inherited from $J$). It connects Law of Existence (existence as defect collapse to zero) to concrete configuration types: zero cost means ratio one, the balanced fixed point of $J$. Without a ratio map, abstract types cannot host the RS cost or the forced reference geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.