ratio_triangle_reverse
plain-language theorem explainer
Under a geometric-mean condition on three positive ratios, the reverse triangle inequality holds for RS reference cost: adjacent costs sum to at most the direct cost. Cite when checking whether J is metric-like, or when chaining ratio-induced reference. The proof reduces to the identity J(r²)=2J(r)(J(r)+2) plus J≥0.
Claim. Let $\iota$ embed a type $X$ into the positive reals. For $a,b,c\in X$ with $\iota(b)^2=\iota(a)\cdot\iota(c)$, the ratio-induced reference costs satisfy $R(a,b)+R(b,c)\le R(a,c)$, where $R(x,y)=J(\iota(x)/\iota(y))$ and $J(t)=\frac{t+t^{-1}}{2}-1$.
background
The module treats reference as cost-minimizing compression: a symbol points to an object when the connecting ledger entry minimizes the Recognition Science cost. A ratio map embeds configurations into $\mathbb{R}_+$, so the canonical cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) applies directly. The induced reference structure charges $J$ of the ratio of the two embeddings.
The ordinary triangle inequality for reference bounds direct cost by a chain: $R(a,c)\le R(a,b)+R(b,c)$. The present result is the opposite direction, but only when the three ratios form a geometric progression. Because $J\ge 0$ with equality solely at $1$, the double-angle identity forces $J(r^2)\ge 2J(r)$, so $J$ fails to be a metric on positive reals (and thus on configurations via ratios).
proof idea
Unfold the ratio-induced cost. Set $r_{ab}=\iota(a)/\iota(b)$, $r_{bc}=\iota(b)/\iota(c)$, $r_{ac}=\iota(a)/\iota(c)$; positivity of the three embeddings gives positivity of these quotients. From $\iota(b)^2=\iota(a)\iota(c)$, field simplification yields $r_{ab}=r_{bc}$, and clearing denominators with nlinarith yields $r_{ac}=r_{ab}^2$. The goal collapses to $2J(r)\le J(r^2)$ for $r>0$.
Establish the closed form $J(x^2)=2J(x)(J(x)+2)$ by unfolding $J$ and expanding (equivalently via $\cosh(2t)=2\cosh^2(t)-1$ as in the doc-comment). Nonnegativity of $J$ finishes the inequality; equality holds only at $r=1$.
why it matters
This is local hygiene inside the Physics of Reference development. Ratio-induced reference is one of the module's main constructions, alongside forced emergence of symbols and the ordinary (forward) triangle inequality for chained reference. The doc-comment records that an earlier claim had the inequality backwards; the corrected direction shows explicitly that $J$-cost does not define a metric.
In the forcing chain, $J$ is the unique cost (T5), $J(x)=\cosh(\log x)-1$. Knowing which metric axioms it satisfies or fails constrains every later use of reference cost, composition of reference structures, and the effectiveness principle for near-balanced configurations. No downstream dependents are recorded yet; the lemma stands as a corrected local fact about reverse chaining under geometric means.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.