ratioInducedCost
plain-language theorem explainer
Any configuration space equipped with a positive real ratio map inherits the Recognition Science cost J(x)=(x+1/x)/2-1 as an intrinsic cost function. The construction packages that pullback into a CostedSpace, so later reference theorems can treat ratio-embedded objects uniformly. Citation is for anyone building ratio-induced reference or zero-cost characterizations. The body is a two-field structure instance: J is Jcost of the ratio, nonneg is Jcost_nonneg.
Claim. Given a type $C$ and a ratio map $\iota: C\to\mathbb{R}_{>0}$, the ratio-induced costed space equips $C$ with cost $J(c)=\frac{\iota(c)+\iota(c)^{-1}}{2}-1$, which is nonnegative for every $c$.
background
The module formalizes reference as cost-minimizing compression: a symbol points to an object when the connecting ledger entry minimizes J-cost. A CostedSpace is any type with a nonnegative cost $J:C\to\mathbb{R}$. A RatioMap embeds $C$ into the positive reals so the standard RS cost can be applied pointwise.
Upstream, $J_{\mathrm{cost}}(x)=(x+x^{-1})/2-1$ is the unique recognition cost forced by the composition law (T5 J-uniqueness). The lemma $J_{\mathrm{cost}}\ge 0$ on $\mathbb{R}{>0}$ is AM-GM (equivalently a squared form). Pulling $J{\mathrm{cost}}$ back along the ratio map is the canonical way to put an arbitrary configuration space into the Algebra of Aboutness.
proof idea
Definitional construction, not a proof. The CostedSpace fields are filled by $J(c):=J_{\mathrm{cost}}(\iota.{\mathrm{ratio}},c)$ and $\mathrm{nonneg}(c):=J_{\mathrm{cost_nonneg}}(\iota.{\mathrm{pos}},c)$. No further tactics: positivity of the ratio supplies the hypothesis of the AM-GM nonnegativity lemma.
why it matters
This is the bridge from abstract configuration types to the RS cost used throughout the Physics of Reference. Downstream, ratio_induced_zero_iff shows $J(c)=0$ iff the ratio is $1$, and balanced_zero_cost specializes that to balanced configurations. Those facts feed the mathematical-backbone and effectiveness results: zero-cost (balanced) configurations have universal referential capacity, and near-balanced ones can refer to any positive-cost object. The construction is the cost half of ratioReference, the canonical reference structure inherited from $J(x)=\frac12(x+1/x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.